Efficient Formal Verification of Quantum Error Correcting Programs

• URL: http://arxiv.org/abs/2504.07732v1
• Date: Thu, 10 Apr 2025 13:28:49 GMT
• Title: Efficient Formal Verification of Quantum Error Correcting Programs
• Authors: Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying,
• Abstract summary: We propose an efficient verification framework for Quantum error correction (QEC) programs.<n>We formalize the proposed program logic in Coq proof assistant, making it a verified QEC verifier.<n>We present a benchmark of 14 verified stabilizer codes.
• Score: 4.936399271348611
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Quantum error correction (QEC) is fundamental for suppressing noise in quantum hardware and enabling fault-tolerant quantum computation. In this paper, we propose an efficient verification framework for QEC programs. We define an assertion logic and a program logic specifically crafted for QEC programs and establish a sound proof system. We then develop an efficient method for handling verification conditions (VCs) of QEC programs: for Pauli errors, the VCs are reduced to classical assertions that can be solved by SMT solvers, and for non-Pauli errors, we provide a heuristic algorithm. We formalize the proposed program logic in Coq proof assistant, making it a verified QEC verifier. Additionally, we implement an automated QEC verifier, Veri-QEC, for verifying various fault-tolerant scenarios. We demonstrate the efficiency and broad functionality of the framework by performing different verification tasks across various scenarios. Finally, we present a benchmark of 14 verified stabilizer codes.

Related papers

• Verifying Fault-Tolerance of Quantum Error Correction Codes [7.796308340803447]
  Large-scale fault-tolerant quantum computing still relies on quantum error correction code (QECC) to suppress noise. This paper formalizes the fault-tolerance of QECC implementations within the language of quantum programs.
  arXiv  Detail & Related papers  (2025-01-24T10:28:24Z)
• Fault-tolerant quantum architectures based on erasure qubits [49.227671756557946]
  We exploit the idea of erasure qubits, relying on an efficient conversion of the dominant noise into erasures at known locations. We propose and optimize QEC schemes based on erasure qubits and the recently-introduced Floquet codes. Our results demonstrate that, despite being slightly more complex, QEC schemes based on erasure qubits can significantly outperform standard approaches.
  arXiv  Detail & Related papers  (2023-12-21T17:40:18Z)
• Demonstration of fault-tolerant Steane quantum error correction [0.7174990929661688]
  This study presents the implementation of multiple rounds of fault-tolerant Steane QEC on a trapped-ion quantum computer. Various QEC codes are employed, and the results are compared to a previous experimental approach utilizing flag qubits.
  arXiv  Detail & Related papers  (2023-12-15T12:32:49Z)
• Testing the Accuracy of Surface Code Decoders [55.616364225463066]
  Large-scale, fault-tolerant quantum computations will be enabled by quantum error-correcting codes (QECC) This work presents the first systematic technique to test the accuracy and effectiveness of different QECC decoding schemes.
  arXiv  Detail & Related papers  (2023-11-21T10:22:08Z)
• Single-shot decoding of good quantum LDPC codes [38.12919328528587]
  We prove that quantum Tanner codes facilitate single-shot quantum error correction (QEC) of adversarial noise. We show that in order to suppress errors over multiple repeated rounds of QEC, it suffices to run the parallel decoding algorithm for constant time in each round.
  arXiv  Detail & Related papers  (2023-06-21T18:00:01Z)
• Enabling Full-Stack Quantum Computing with Changeable Error-Corrected Qubits [14.770636234849444]
  We propose CECQ to explore the large design space for FTQC based on changeable logical qubits. Experiments on various quantum programs demonstrate the effectiveness of CECQ.
  arXiv  Detail & Related papers  (2023-05-11T18:14:49Z)
• Deep Quantum Error Correction [73.54643419792453]
  Quantum error correction codes (QECC) are a key component for realizing the potential of quantum computing. In this work, we efficiently train novel emphend-to-end deep quantum error decoders. The proposed method demonstrates the power of neural decoders for QECC by achieving state-of-the-art accuracy.
  arXiv  Detail & Related papers  (2023-01-27T08:16:26Z)
• Qafny: A Quantum-Program Verifier [39.47005122712576]
  We present Qafny, an automated proof system for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations. We show how Qafny can efficiently verify important quantum algorithms, including quantum-walk algorithms, Grover's algorithm, and Shor's algorithm.
  arXiv  Detail & Related papers  (2022-11-11T18:50:52Z)
• Measurement based estimator scheme for continuous quantum error correction [52.77024349608834]
  Canonical discrete quantum error correction (DQEC) schemes use projective von Neumann measurements on stabilizers to discretize the error syndromes into a finite set. Quantum error correction (QEC) based on continuous measurement, known as continuous quantum error correction (CQEC), can be executed faster than DQEC and can also be resource efficient. We show that by constructing a measurement-based estimator (MBE) of the logical qubit to be protected, it is possible to accurately track the errors occurring on the physical qubits in real time.
  arXiv  Detail & Related papers  (2022-03-25T09:07:18Z)
• Measuring NISQ Gate-Based Qubit Stability Using a 1+1 Field Theory and Cycle Benchmarking [50.8020641352841]
  We study coherent errors on a quantum hardware platform using a transverse field Ising model Hamiltonian as a sample user application. We identify inter-day and intra-day qubit calibration drift and the impacts of quantum circuit placement on groups of qubits in different physical locations on the processor. This paper also discusses how these measurements can provide a better understanding of these types of errors and how they may improve efforts to validate the accuracy of quantum computations.
  arXiv  Detail & Related papers  (2022-01-08T23:12:55Z)
• QECV: Quantum Error Correction Verification [15.05397810840915]
  We propose QECV, a verification framework that can efficiently verify the formal correctness of stabilizer codes. We derive a sound quantum Hoare logic proof system with a set of inference rules for QECV to efficiently reason about the correctness of QEC programs.
  arXiv  Detail & Related papers  (2021-11-26T19:40:53Z)
• Using Quantum Metrological Bounds in Quantum Error Correction: A Simple Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
  We present a proof of the approximate Eastin-Knill theorem, which connects the quality of a quantum error-correcting code with its ability to achieve a universal set of logical gates. Our derivation employs powerful bounds on the quantum Fisher information in generic quantum metrological protocols.
  arXiv  Detail & Related papers  (2020-04-24T17:58:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.