arXiv subjects

Mingsheng Ying

Publications and source records attributed to Mingsheng Ying.

At least 37 records · Page 2Linked to original sources

arXiv2025

LimTDD: A Compact Decision Diagram Integrating Tensor and Local Invertible Map Representations

Tensor networks serve as a powerful tool for efficiently representing and manipulating high-dimensional data in applications such as quantum physics, machine learning, and data compression. Tensor Decision Diagrams (TDDs) offer an efficient framework for tensor representation by leveraging decision diagram techniques. However, the current implementation of TDDs and other decision diagrams fail to exploit tensor isomorphisms, limiting their compression potential. This paper introduces Local Invertible Map Tensor Decision Diagrams (LimTDDs), an extension of TDDs that incorporates local invertible maps (LIMs) to achieve more compact representations. Unlike LIMDD, which uses Pauli operators for quantum states, LimTDD employs the $XP$-stabilizer group, enabling broader applicability across tensor-based tasks. We present efficient algorithms for normalization, slicing, addition, and contraction, critical for tensor network applications. Theoretical analysis demonstrates that LimTDDs achieve greater compactness than TDDs and, in best-case scenarios and for quantum state representations, offer exponential compression advantages over both TDDs and LIMDDs. Experimental results in quantum circuit tensor computation and simulation confirm LimTDD's superior efficiency. Open-source code is available at https://github.com/Veriqc/LimTDD.

cs.DS↗

arXiv2025

Laws of Quantum Programming

In this paper, we investigate the fundamental laws of quantum programming. We extend a comprehensive set of Hoare et al.'s basic laws of classical programming to the quantum setting. These laws characterise the algebraic properties of quantum programs, such as the distributivity of sequential composition over (quantum) if-statements and the unfolding of nested (quantum) if-statements. At the same time, we clarify some subtle differences between certain laws of classical programming and their quantum counterparts. Additionally, we derive a fixpoint characterisation of quantum while-loops and a loop-based realisation of tail recursion in quantum programming. Furthermore, we establish two normal form theorems: one for quantum circuits and one for finite quantum programs. The theory in which these laws are established is formalised in the Coq proof assistant, and all of these laws are mechanically verified. As an application case of our laws, we present a formal derivation of the principle of deferred measurements in dynamic quantum circuits. We expect that these laws can be utilised in correctness-preserving transformation, compilation, and automatic code optimisation in quantum programming. In particular, because these laws are formally verified in Coq, they can be confidently applied in quantum program development.

cs.PL↗

arXiv2025

Borrowing Dirty Qubits in Quantum Programs

Dirty qubits are ancillary qubits that can be borrowed from idle parts of a computation, enabling qubit reuse and reducing the demand for fresh, clean qubits-a resource that is typically scarce in practice. For such reuse to be valid, the initial states of the dirty qubits must not affect the functionality of the quantum circuits in which they are employed. Moreover, their original states, including any entanglement they possess, must be fully restored after use-a requirement commonly known as safe uncomputation. In this paper, we formally define the semantics of dirty-qubit borrowing as a feature in quantum programming languages, and introduce a notion of safe uncomputation for dirty qubits in quantum programs. We also present an efficient algorithm, along with experimental results, for verifying safe uncomputation of dirty qubits in certain quantum circuits.

quant-ph↗

arXiv2025

Advancing Quantum State Preparation Using Decision Diagram with Local Invertible Maps

Quantum state preparation (QSP) is a fundamental task in quantum computing and quantum information processing. It is critical to the execution of many quantum algorithms, including those in quantum machine learning. In this paper, we propose a family of efficient QSP algorithms tailored to different numbers of available ancilla qubits - ranging from no ancilla qubits, to a single ancilla qubit, to a sufficiently large number of ancilla qubits. Our approach exploits the power of Local Invertible Map Tensor Decision Diagrams (LimTDDs) - a highly compact representation of quantum states that combines tensor networks and decision diagrams to reduce quantum circuit complexity. Extensive experiments demonstrate that our methods significantly outperform existing approaches and exhibit better scalability for large-scale quantum states, both in terms of runtime and gate complexity. Furthermore, our method shows exponential improvement in best-case scenarios.

cs.DS↗

arXiv2025

Quantum State Preparation Based on LimTDD

Quantum state preparation is a fundamental task in quantum computing and quantum information processing. With the rapid advancement of quantum technologies, efficient quantum state preparation has become increasingly important. This paper proposes a novel approach for quantum state preparation based on the Local Invertible Map Tensor Decision Diagram (LimTDD). LimTDD combines the advantages of tensor networks and decision diagrams, enabling efficient representation and manipulation of quantum states. Compared with the state-of-the-art quantum state preparation method, LimTDD demonstrates substantial improvements in efficiency when dealing with complex quantum states, while also reducing the complexity of quantum circuits. Examples indicate that, in the best-case scenario, our method can achieve exponential efficiency gains over existing methods. This study not only highlights the potential of LimTDD in quantum state preparation but also provides a robust theoretical and practical foundation for the future development of quantum computing technologies.

quant-ph↗

arXiv2025

A Tensor Network based Decision Diagram for Representation of Quantum Circuits

Tensor networks have been successfully applied in simulation of quantum physical systems for decades. Recently, they have also been employed in classical simulation of quantum computing, in particular, random quantum circuits. This paper proposes a decision diagram style data structure, called TDD (Tensor Decision Diagram), for more principled and convenient applications of tensor networks. This new data structure provides a compact and canonical representation for quantum circuits. By exploiting circuit partition, the TDD of a quantum circuit can be computed efficiently. Furthermore, we show that the operations of tensor networks essential in their applications (e.g., addition and contraction), can also be implemented efficiently in TDDs. A proof-of-concept implementation of TDDs is presented and its efficiency is evaluated on a set of benchmark quantum circuits. It is expected that TDDs will play an important role in various design automation tasks related to quantum circuits, including but not limited to equivalence checking, error detection, synthesis, simulation, and verification.

quant-ph↗

arXiv2025

Access Control Threatened by Quantum Entanglement

Access control is a cornerstone of computer security that prevents unauthorised access to resources. In this paper, we study access control in quantum computer systems. We present the first explicit scenario of a security breach when a classically secure access control system is straightforwardly adapted to the quantum setting. The breach is ultimately due to that quantum mechanics allows the phenomenon of entanglement and violates Mermin inequality, a multi-party variant of the celebrated Bell inequality. This reveals a threat from quantum entanglement to access control if existing computer systems integrate with quantum computing. To protect against such threat, we propose several new models of quantum access control, and rigorously analyse their security, flexibility and efficiency.

quant-ph↗

arXiv2025

Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs

Quantum recursive programming has been recently introduced for describing sophisticated and complicated quantum algorithms in a compact and elegant way. However, implementation of quantum recursion involves intricate interplay between quantum control flow and recursive procedure calls. In this paper, we aim at resolving this fundamental challenge and develop a series of techniques to efficiently implement quantum recursive programs. Our main contributions include: 1. We propose a notion of quantum register machine, the first quantum architecture (including an instruction set) that provides instruction-level support for quantum control flow and recursive procedure calls at the same time. 2. Based on quantum register machine, we describe the first comprehensive implementation process of quantum recursive programs, including the compilation, the partial evaluation of quantum control flow, and the execution on the quantum register machine. 3. As a bonus, our efficient implementation of quantum recursive programs also offers automatic parallelisation of quantum algorithms. For implementing certain quantum algorithmic subroutine, like the widely used quantum multiplexor, we can even obtain exponential parallel speed-up (over the straightforward implementation) from this automatic parallelisation. This demonstrates that quantum recursive programming can be win-win for both modularity of programs and efficiency of their implementation.

quant-ph↗

arXiv2025

Quantum Speedup for Hypergraph Sparsification

Graph sparsification serves as a foundation for many algorithms, such as approximation algorithms for graph cuts and Laplacian system solvers. As its natural generalization, hypergraph sparsification has recently gained increasing attention, with broad applications in graph machine learning and other areas. In this work, we propose the first quantum algorithm for hypergraph sparsification, addressing an open problem proposed by Apers and de Wolf (FOCS'20). For a weighted hypergraph with $n$ vertices, $m$ hyperedges, and rank $r$, our algorithm outputs a near-linear size $\varepsilon$-spectral sparsifier in time $\widetilde O(r\sqrt{mn}/\varepsilon)$. This algorithm matches the quantum lower bound for constant $r$ and demonstrates quantum speedup when compared with the state-of-the-art $\widetilde O(mr)$-time classical algorithm. As applications, our algorithm implies quantum speedups for computing hypergraph cut sparsifiers, approximating hypergraph mincuts and hypergraph $s$-$t$ mincuts.

quant-ph↗

arXiv2025

Image Computation for Quantum Transition Systems

With the rapid progress in quantum hardware and software, the need for verification of quantum systems becomes increasingly crucial. While model checking is a dominant and very successful technique for verifying classical systems, its application to quantum systems is still an underdeveloped research area. This paper advances the development of model checking quantum systems by providing efficient image computation algorithms for quantum transition systems, which play a fundamental role in model checking. In our approach, we represent quantum circuits as tensor networks and design algorithms by leveraging the properties of tensor networks and tensor decision diagrams. Our experiments demonstrate that our contraction partition-based algorithm can greatly improve the efficiency of image computation for quantum transition systems.

cs.DS↗

arXiv2024

Control Flow Adaption: An Efficient Simulation Method For Noisy Quantum Networks

Quantum network research at both the software stack and hardware implementation level has become an exciting area of quantum information science. Although demonstrations of small-scale quantum networks have emerged in the past decade, quantum communication and computation hardware remain scarce resources today. As a result, the evaluation and validation of quantum network protocols primarily rely on classical simulators rather than real quantum networks. This paper introduces a novel quantum network simulation method called control flow adaptation, which enhances standard tensor network simulations. This method enables accurate and efficient simulations of many important quantum network protocols by carefully leveraging the control flow structures of them. Furthermore, we have developed a prototype quantum network simulator, qns-3, as a module for ns-3. This new module implements the control flow adaptation technique and applies it to a wide range of protocols. All related code is open-sourced. We believe the development of the control flow adaptation method and the qns-3 simulator represents a step forward in quantum network research, offering a versatile and scalable platform for testing and verifying quantum network protocols on classical computers.

quant-ph↗

arXiv2024

Verification of Recursively Defined Quantum Circuits

Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and economically programmed. In this paper, we present a proof system for formal verification of the correctness of recursively defined quantum circuits. The soundness and (relative) completeness of the proof system are established. To demonstrating its effectiveness, a series of application examples of the proof system are given, including (multi-qubit) controlled gates, a quantum circuit generating (multi-qubit) GHZ (Greenberger-Horne-Zeilinger) states, recursive definition of quantum Fourier transform, quantum state preparation, and quantum random-access memories (QRAM).

quant-ph↗

arXiv2024

Automatic Test Pattern Generation for Robust Quantum Circuit Testing

Quantum circuit testing is essential for detecting potential faults in realistic quantum devices, while the testing process itself also suffers from the inexactness and unreliability of quantum operations. This paper alleviates the issue by proposing a novel framework of automatic test pattern generation (ATPG) for robust testing of logical quantum circuits. We introduce the stabilizer projector decomposition (SPD) for representing the quantum test pattern, and construct the test application (i.e., state preparation and measurement) using Clifford-only circuits, which are rather robust and efficient as evidenced in the fault-tolerant quantum computation. However, it is generally hard to generate SPDs due to the exponentially growing number of the stabilizer projectors. To circumvent this difficulty, we develop an SPD generation algorithm, as well as several acceleration techniques which can exploit both locality and sparsity in generating SPDs. The effectiveness of our algorithms are validated by 1) theoretical guarantees under reasonable conditions, 2) experimental results on commonly used benchmark circuits, such as Quantum Fourier Transform (QFT), Quantum Volume (QV) and Bernstein-Vazirani (BV) in IBM Qiskit.

quant-ph↗

arXiv2024

Quantum Büchi Automata

Quantum finite automata (QFAs) have been extensively studied in the literature. In this paper, we define and systematically study quantum Büchi automata (QBAs) over infinite words to model the long-term behavior of quantum systems, which extend QFAs. We introduce the classes of $ω$-languages recognized by QBAs in probable, almost sure, strict and non-strict threshold semantics. Several pumping lemmas and closure properties for QBAs are proved. Some decision problems for QBAs are investigated. In particular, we show that there are surprisingly only at most four substantially different classes of $ω$-languages recognized by QBAs (out of uncountably infinite). The relationship between classical $ω$-languages and QBAs is clarified using our pumping lemmas. We also find an $ω$-language recognized by QBAs under the almost sure semantics, which is not $ω$-context-free.

cs.LO↗

arXiv2024

VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models

Adversarial noise attacks present a significant threat to quantum machine learning (QML) models, similar to their classical counterparts. This is especially true in the current Noisy Intermediate-Scale Quantum era, where noise is unavoidable. Therefore, it is essential to ensure the robustness of QML models before their deployment. To address this challenge, we introduce \textit{VeriQR}, the first tool designed specifically for formally verifying and improving the robustness of QML models, to the best of our knowledge. This tool mimics real-world quantum hardware's noisy impacts by incorporating random noise to formally validate a QML model's robustness. \textit{VeriQR} supports exact (sound and complete) algorithms for both local and global robustness verification. For enhanced efficiency, it implements an under-approximate (complete) algorithm and a tensor network-based algorithm to verify local and global robustness, respectively. As a formal verification tool, \textit{VeriQR} can detect adversarial examples and utilize them for further analysis and to enhance the local robustness through adversarial training, as demonstrated by experiments on real-world quantum machine learning models. Moreover, it permits users to incorporate customized noise. Based on this feature, we assess \textit{VeriQR} using various real-world examples, and experimental outcomes confirm that the addition of specific quantum noise can enhance the global robustness of QML models. These processes are made accessible through a user-friendly graphical interface provided by \textit{VeriQR}, catering to general users without requiring a deep understanding of the counter-intuitive probabilistic nature of quantum computing.

quant-ph↗

arXiv2024

New Quantum Algorithms for Computing Quantum Entropies and Distances

We propose a series of quantum algorithms for computing a wide range of quantum entropies and distances, including the von Neumann entropy, quantum Rényi entropy, trace distance, and fidelity. The proposed algorithms significantly outperform the prior best (and even quantum) ones in the low-rank case, some of which achieve exponential speedups. In particular, for $N$-dimensional quantum states of rank $r$, our proposed quantum algorithms for computing the von Neumann entropy, trace distance and fidelity within additive error $\varepsilon$ have time complexity of $\tilde O(r/\varepsilon^2)$, $\tilde O(r^5/\varepsilon^6)$ and $\tilde O(r^{6.5}/\varepsilon^{7.5})$, respectively. By contrast, prior quantum algorithms for the von Neumann entropy and trace distance usually have time complexity $Ω(N)$, and the prior best one for fidelity has time complexity $\tilde O(r^{12.5}/\varepsilon^{13.5})$. The key idea of our quantum algorithms is to extend block-encoding from unitary operators in previous work to quantum states (i.e., density operators). It is realized by developing several convenient techniques to manipulate quantum states and extract information from them. The advantage of our techniques over the existing methods is that no restrictions on density operators are required; in sharp contrast, the previous methods usually require a lower bound on the minimal non-zero eigenvalue of density operators.

quant-ph↗

arXiv2024

Measurement-based Verification of Quantum Markov Chains

Model-checking techniques have been extended to analyze quantum programs and communication protocols represented as quantum Markov chains, an extension of classical Markov chains. To specify qualitative temporal properties, a subspace-based quantum temporal logic is used, which is built on Birkhoff-von Neumann atomic propositions. These propositions determine whether a quantum state is within a subspace of the entire state space. In this paper, we propose the measurement-based linear-time temporal logic MLTL to check quantitative properties. MLTL builds upon classical linear-time temporal logic (LTL) but introduces quantum atomic propositions that reason about the probability distribution after measuring a quantum state. To facilitate verification, we extend the symbolic dynamics-based techniques for stochastic matrices described by Agrawal et al. (JACM 2015) to handle more general quantum linear operators (super-operators) through eigenvalue analysis. This extension enables the development of an efficient algorithm for approximately model checking a quantum Markov chain against an MLTL formula. To demonstrate the utility of our model-checking algorithm, we use it to simultaneously verify linear-time properties of both quantum and classical random walks. Through this verification, we confirm the previously established advantages discovered by Ambainis et al. (STOC 2001) of quantum walks over classical random walks and discover new phenomena unique to quantum walks.

quant-ph↗

arXiv2024

Equivalence Checking of Parameterised Quantum Circuits

Parameterised quantum circuits (PQCs) hold great promise for demonstrating quantum advantages in practical applications of quantum computation. Examples of successful applications include the variational quantum eigensolver, the quantum approximate optimisation algorithm, and quantum machine learning. However, before executing PQCs on real quantum devices, they undergo compilation and optimisation procedures. Given the inherent error-proneness of these processes, it becomes crucial to verify the equivalence between the original PQC and its compiled or optimised version. Unfortunately, most existing quantum circuit verifiers cannot directly handle parameterised quantum circuits; instead, they require parameter substitution to perform verification. In this paper, we address the critical challenge of equivalence checking for PQCs. We propose a novel compact representation for PQCs based on tensor decision diagrams. Leveraging this representation, we present an algorithm for verifying PQC equivalence without the need for instantiation. Our approach ensures both effectiveness and efficiency, as confirmed by experimental evaluations. The decision-diagram representations offer a powerful tool for analysing and verifying parameterised quantum circuits, bridging the gap between theoretical models and practical implementations.

quant-ph↗