The ubiquity of stabilizer circuits in the design and operation of quantum computers makes techniques to verify their correctness essential. The simulation of stabilizer circuits, which aims to replicate their behavior using a classical computer, is known to be efficient and provides a means of testing correctness. However, simulation is limited in its ability to examine the exponentially large space of possible measurement outcomes. We propose a comprehensive set of efficient classical algorithms to fully characterize and exhaustively verify stabilizer circuits with Pauli unitaries conditioned on parities of measurements. We introduce, as a practical characterization, a general form for such circuits and provide an algorithm to find a general form of any stabilizer circuit. We then provide an algorithm for checking the equivalence of stabilizer circuits. When circuits are not equivalent our algorithm suggests modifications for reconciliation. Next, we provide an algorithm that characterizes the logical action of a (physical) stabilizer circuit on an encoded input. All of our algorithms provide relations of measurement outcomes among corresponding circuit representations. Finally, we provide an analytic description of the logical action induced by measuring a stabilizer group, with application in correctness proofs of code-deformation protocols including lattice surgery and code switching.
The ubiquity of stabilizer circuits in the design and operation of quantum computers makes techniques to verify their correctness essential. The simulation of stabilizer circuits, which aims to replicate their behavior using a classical computer, is known to be efficient and provides a means of testing correctness. However, simulation is limited in its ability to examine the exponentially large space of possible measurement outcomes. We propose a comprehensive set of efficient classical algorithms to fully characterize and exhaustively verify stabilizer circuits with Pauli unitaries conditioned on parities of measurements. We introduce, as a practical characterization, a general form for such circuits and provide an algorithm to find a general form of any stabilizer circuit. We then provide an algorithm for checking the equivalence of stabilizer circuits. When circuits are not equivalent our algorithm suggests modifications for reconciliation. Next, we provide an algorithm that characterizes the logical action of a (physical) stabilizer circuit on an encoded input. All of our algorithms provide relations of measurement outcomes among corresponding circuit representations. Finally, we provide an analytic description of the logical action induced by measuring a stabilizer group, with application in correctness proofs of code-deformation protocols including lattice surgery and code switching.
We generalize the polynomial-time outcome-complete simulation algorithm for stabilizer circuits in arXiv:2309.08676 to track global phases exactly, yielding what we call phased outcome-complete simulation. The original algorithm enabled equivalence checking of stabilizer circuits with intermediate measurements and conditional Pauli corrections for all input states and all measurement outcomes simultaneously, but it tracked quantum states only up to a global phase. Our generalization removes this limitation and enables equivalence checking for an important family of non-stabilizer circuits: stabilizer circuits augmented with single-qubit rotations exp(iαZ) by symbolic angles. Two such circuits are equivalent if they implement the same quantum channel for all values of the symbolic angles and all measurement outcomes, given a one-to-one correspondence between rotation angles in the two circuits and a mapping between measurement outcomes. This model enables testing of compilation algorithms that transform the Clifford portions of a computation while preserving rotation angles. Examples include Pauli-based computation, edge-disjoint path compilation for surface codes, and custom compilation strategies for reversible circuits such as adders, multipliers, and table lookups. Our efficient classical verification methods extend naturally to circuits with outcome-parity-conditional Pauli gates and intermediate measurements, features that are ubiquitous in fault-tolerant quantum computing but are rarely addressed by existing equivalence-checking approaches.
Abstract Equivalence checking plays a crucial role in quantum circuit compilation, optimization, and verification. Stabilizer circuits can be simulated classically by tracking the so-called stabilizer operators in linear time. But the simulation of large stabilizer circuits with thousands of qubits and gates, arising e.g. in the study of novel quantum error-correction protocols, still poses a challenge. In this work, we propose a GPU-based deterministic algorithm for equivalence checking of stabilizer circuits using the stabilizer tableau formalism. We explore various design choices and implement the most efficient version. Our algorithm significantly outperforms the state-of-the-art CCEC checker (which relies on the Stim simulator) in terms of time, memory, and energy. Our approach demonstrates up to two orders of magnitude speedup over existing methods. Notably, previous attempts at GPU acceleration in this area were unsuccessful, making this the first effective implementation.
This research paper provides an in-depth examination of verification and testing approaches for quantum circuits, focusing on methodologies essential for ensuring the correctness, reliability and operational efficiency of quantum computing systems. Since quantum circuits function on the fundamental principles of superposition and entanglement, they present verification challenges that cannot be effectively addressed using conventional classical testing techniques. As a result, the development of specialized quantum-specific verification strategies has become critically important. The study highlights simulation-based verification as a foundational technique, wherein the outcomes of quantum circuit simulations are systematically compared with results obtained from physical quantum hardware. This process enables the identification of functional inconsistencies and supports iterative refinement of circuit designs. In addition, randomized benchmarking is examined as a key evaluation method for estimating circuit fidelity and quantifying error rates through the application of random gate sequences and performance comparisons against established benchmarks. To further improve system robustness, the research investigates fault-tolerant mechanisms, particularly quantum error correction codes, which play a vital role in minimizing the effects of noise, decoherence and hardware imperfections. The integration of advanced quantum metrology and characterization techniques is also explored, enabling precise measurement and detailed analysis of quantum system behavior. These techniques provide deeper insights into circuit performance and contribute significantly to validation processes. By combining simulation-based verification, randomized benchmarking, fault-tolerant protocols and quantum metrology, this study proposes a comprehensive and reliable framework for quantum circuit verification and testing. The findings contribute to the advancement of dependable quantum technologies and support their growing applications in areas such as cryptography, materials science and other emerging domains.
To implement quantum algorithms on a quantum computer, we must overcome the twin problems of fault-tolerance -- how can we realize a relatively noiseless computation by cleverly combining noisy components? -- and compilation -- how can we realize an arbitrary quantum algorithm given the basic operations available on the quantum device at hand? We show how treating the former problem via error-correcting codes enables greater flexibility in resolving the latter. Specifically, we explicitly leverage the fact that error-correcting codes introduce redundancy which renders physically distinct operators logically indistinguishable. In terms of computation, it suffices to implement any operator logically equivalent to some target, yet from a compilation perspective, certain choices may be preferable to others. Our novel contribution is making this intuition precise in the general setting of the special unitary group. In particular, we describe how to reduce the problem of making a compilation-ideal choice to a least squares problem and provide a closed form solution thereof. Using our framework, it is possible to circumvent inserting costly swaps to adhere to hardware connectivity; instead, we could realize the logical target through a distinct physical Hamiltonian that is natively accessible. We elucidate our approach using the [[4,2,2]] code. We discuss connections to compressed sensing that may pave the way to efficient compilation leveraging physical degrees of freedom.
Large-scale quantum computation is likely to require massive quantum error correction (QEC). QEC codes and circuits are described via the stabilizer formalism, which represents stabilizer states by keeping track of the operators that preserve them. Such states are obtained by stabilizer circuits (consisting of CNOT, Hadamard and Phase only) and can be represented compactly on conventional computers using Omega(n^2) bits, where n is the number of qubits. Although techniques for the efficient simulation of stabilizer circuits have been studied extensively, techniques for efficient manipulation of stabilizer states are not currently available. To this end, we design new algorithms for: (i) obtaining canonical generators for stabilizer states, (ii) obtaining canonical stabilizer circuits, and (iii) computing the inner product between stabilizer states. Our inner-product algorithm takes O(n^3) time in general, but observes quadratic behavior for many practical instances relevant to QECC (e.g., GHZ states). We prove that each n-qubit stabilizer state has exactly 4(2^n - 1) nearest-neighbor stabilizer states, and verify this claim experimentally using our algorithms. We design techniques for representing arbitrary quantum states using stabilizer frames and generalize our algorithms to compute the inner product between two such frames.
Quantum technologies have progressed beyond the laboratory setting and are beginning to make an impact on industrial development. The construction of practical, general purpose quantum computers has been challenging, to say the least. But quantum cryptographic and communication devices have been available in the commercial marketplace for a few years. Quantum networks have been built in various cities around the world, and plans are afoot to launch a dedicated satellite for quantum communication. Such new technologies demand rigorous analysis and verification before they can be trusted in safety and security-critical applications. In this thesis we investigate the theory and practice of equivalence checking of quantum information systems. We present a tool, Quantum Equivalence Checker (QEC), which uses a concurrent language for describing quantum systems, and performs verification by checking equivalence between specification and implementation. For our process algebraic language CCSq, we define an operational semantics and a superoperator semantics. While in general, simulation of quantum systems using current computing technology is infeasible, we restrict ourselves to the stabilizer formalism, in which there are efficient simulation algorithms and representation of quantum states. By using the stabilizer representation of quantum states we introduce various algorithms for testing equality of stabilizer states. In this thesis, we consider concurrent quantum protocols that behave functionally in the sense of computing a deterministic input-output relation for all interleavings of a concurrent system. Crucially, these input-output relations can be abstracted by superoperators, enabling us to take advantage of linearity. This allows us to analyse the behaviour of protocols with arbitrary input, by simulating their operation on a finite basis set consisting of stabilizer states. We present algorithms for the checking of functionality and equivalence of quantum protocols. Despite the limitations of the stabilizer formalism and also the range of protocols that can be analysed using equivalence checking, QEC is applied to specify and verify a variety of interesting and practical quantum protocols from quantum communication and quantum cryptography to quantum error correction and quantum fault tolerant computation, where for each protocol different sequential and concurrent model are defined in CCSq. We also explain the implementation details of the QEC tool and report on the experimental results produced by using it on the verification of a number of case studies.