Verifying Fault-Tolerance of Quantum Error Correction Codes
arXiv:2501.14380 · doi:10.1007/978-3-031-98685-7_1
Abstract
Quantum computers have advanced rapidly in qubit count and gate fidelity. However, large-scale fault-tolerant quantum computing still relies on quantum error correction code (QECC) to suppress noise. Manually or experimentally verifying the fault-tolerance property of complex QECC implementation is impractical due to the vast error combinations. This paper formalizes the fault-tolerance of QECC implementations within the language of quantum programs. By incorporating the techniques of quantum symbolic execution, we provide an automatic verification tool for quantum fault-tolerance. We evaluate and demonstrate the effectiveness of our tool on a universal set of logical operations across different QECCs.
54 pages, 8 figures, extended version of the paper accepted by CAV 2025
References in corpus (16)
- Improved Simulation of Stabilizer Circuits
- Universal Quantum Computation with ideal Clifford gates and noisy ancillas
- Suppressing quantum errors by scaling a surface code logical qubit
- Logical quantum processor based on reconfigurable atom arrays
- Topological Quantum Distillation
- Surface code quantum computing by lattice surgery
- Quantum Low-Density Parity-Check Codes
- Optimal Resources for Topological 2D Stabilizer Codes: Comparative Study
- Understanding the effects of leakage in superconducting quantum error detection circuits
- Equivalence Checking of Quantum Circuits with the ZX-Calculus
- Universality of single qudit gates
- symQV: Automated Symbolic Verification of Quantum Programs
- Quantitative Robustness Analysis of Quantum Programs (Extended Version)
- Equivalence Checking of Parameterized Quantum Circuits: Verifying the Compilation of Variational Quantum Algorithms
- Symbolic Execution for Quantum Error Correction Programs
- Automatic Test Pattern Generation for Robust Quantum Circuit Testing