Symbolic Execution for Quantum Error Correction Programs
arXiv:2311.11313 · doi:10.1145/3656419
Abstract
We define QSE, a symbolic execution framework for quantum programs by integrating symbolic variables into quantum states and the outcomes of quantum measurements. The soundness of QSE is established through a theorem that ensures the correctness of symbolic execution within operational semantics. We further introduce symbolic stabilizer states, which symbolize the phases of stabilizer generators, for the efficient analysis of quantum error correction (QEC) programs. Within the QSE framework, we can use symbolic expressions to characterize the possible discrete Pauli errors in QEC, providing a significant improvement over existing methods that rely on sampling with simulators. We implement QSE with the support of symbolic stabilizer states in a prototype tool named QuantumSE.jl. Our experiments on representative QEC codes, including quantum repetition codes, Kitaev's toric codes, and quantum Tanner codes, demonstrate the efficiency of QuantumSE.jl for debugging QEC programs with over 1000 qubits. In addition, by substituting concrete values in symbolic expressions of measurement results, QuantumSE.jl is also equipped with a sampling feature for stabilizer circuits. Despite a longer initialization time than the state-of-the-art stabilizer simulator, Google's Stim, QuantumSE.jl offers a quicker sampling rate in the experiments.
41pages, 11 figures. v2: fix inappropriate use of Stim. v3: Extended version of PLDI 2024 publication
References in corpus (20)
- Supplementary information for "Quantum supremacy using a programmable superconducting processor"
- Surface codes: Towards practical large-scale quantum computation
- Strong quantum computational advantage using a superconducting quantum processor
- Suppressing quantum errors by scaling a surface code logical qubit
- Logical quantum processor based on reconfigurable atom arrays
- Exponential suppression of bit or phase flip errors with repetitive error correction
- Stim: a fast stabilizer circuit simulator
- Realization of an Error-Correcting Surface Code with Superconducting Qubits
- Fault-tolerant operation of a logical qubit in a diamond quantum processor
- Fast simulation of stabilizer circuits using a graph state representation
- Statistical Assertions for Validating Patterns and Finding Bugs in Quantum Programs
- Simulation of Qubit Quantum Circuits via Pauli Propagation
- symQV: Automated Symbolic Verification of Quantum Programs
- LIMDD: A Decision Diagram for Simulation of Quantum Computing Including Stabilizer States
- CFLOBDDs: Context-Free-Language Ordered Binary Decision Diagrams
- A SAT Encoding for Optimal Clifford Circuit Synthesis
- Symbolic Execution for Randomized Programs
- Symbolic Execution for Quantum Error Correction Programs
- Gottesman Types for Quantum Programs
- Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond