End-to-End Formalization of Quantum Error Correction

• URL: http://arxiv.org/abs/2605.16523v1
• Date: Fri, 15 May 2026 18:17:55 GMT
• Title: End-to-End Formalization of Quantum Error Correction
• Abstract summary: Quantum error-correcting codes (QECCs) sit between noisy quantum hardware and reliable computation, so the code parameters used in practice must be trustworthy.<n>We present Lean-QEC, the first Lean 4 formalization of stabilizer-code theory that delivers machine-checked distance certificates at industrial code sizes.
• Score: 6.320988144551776
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Quantum error-correcting codes (QECCs) sit between noisy quantum hardware and reliable computation, so the code parameters used in practice must be trustworthy. The single number that summarizes a code's strength is its distance, yet certifying a distance lower bound is NP-hard in general, placing it beyond the reach of pen-and-paper proofs as well as direct proof-assistant scripting. As a result, distance values in the literature come either from non-scaling hand proofs, or from unverified solvers that leave a trust gap exactly where the code is supposed to provide a guarantee. We present Lean-QEC, the first Lean 4 formalization of stabilizer-code theory that delivers end-to-end, machine-checked distance certificates at industrial code sizes. Lean-QEC formalizes the linear algebra of qubit states, the Pauli group, stabilizer codes, the binary symplectic representation, classical coding theory, and the CSS and Bivariate Bicycle families. To break the combinatorial barrier, Lean-QEC translates the distance condition into a Boolean satisfiability formula through a verified reduction. The pipeline scales through a BitVec-flattened encoding that replaces Lean's Matrix representation, and an error-location encoding that reduces the variable count from $n$ to $k\lceil \log_2 n\rceil$. With these, we obtain automatically-generated Lean-checked distance proofs for a large range of industrially viable qLDPC codes within the Bivariate Bicycle and Generalized Bicycle families, including [[90, 8, 10]] and [[70, 6, 9]] BB codes, with the formulation scaling up to 144 qubits when performed outside the Lean kernel. The resulting library is reusable and is designed to plug into broader Lean-based efforts toward end-to-end verification of fault-tolerant quantum computation.

Related papers

• Probabilistic Error Cancellation for Single-Mode Gottesman-Kitaev-Preskill Codes [45.91504150103373]
  We study a quantum error mitigation method known as probabilistic error cancellation in the context of the Gottesman-Kitaev-Preskill code.<n>We employ the stabilizer subsystem decomposition for GKP codes to obtain an effective logical channel for noisy operations.
  arXiv  Detail & Related papers  (2026-09-15T12:29:45Z)
• Theory of approximate quantum error correction and the error-set model [53.73800998389749]
  We develop a theory of approximate quantum error correction based on the error-set model.<n>Code correcting a given error set automatically protects against every channel whose Kraus operators lie in their linear span.<n>This linearity gives rise to code distance, the equivalence between erasures and general errors, and a theory ofally good codes.
  arXiv  Detail & Related papers  (2026-07-25T02:15:33Z)
• Error Correction of Beamsplitter-Generated Entangled GKP States [56.80803785296797]
  A promising bosonic code is the Gottesman-Kitaev-Preskill (GKP) code.<n>We generate entangled states of GKP qubits by interfering two qunaught states, which have a grid structure but carry no logical information, on a beamsplitter.<n>We generate all four Bell states with an average fidelity of 69%, and demonstrate an extension of the entangled state lifetime through the use of quantum error correction.
  arXiv  Detail & Related papers  (2026-05-08T17:01:19Z)
• Self-dual Stacked Quantum Low-Density Parity-Check Codes [9.268855474673822]
  We introduce a method for constructing self-dual qLDPC codes by stacking non-self-dual qLDPC codes.<n>We conduct numerical calculations to assess the performance of these codes as quantum memory under the circuit-level noise model.
  arXiv  Detail & Related papers  (2026-02-17T05:55:48Z)
• Single-Shot and Few-Shot Decoding via Stabilizer Redundancy in Bivariate Bicycle Codes [5.685589351789461]
  We prove that $g(z)$ dictates the code's stabilizer redundancy and the structure of the classical emphsyndrome codes required for single-shot decoding.<n>Within the coprime BB ansatz, high quantum rate imposes an upper bound on syndrome distance, limiting single-shot performance.
  arXiv  Detail & Related papers  (2026-01-03T09:49:58Z)
• Toward Uncertainty-Aware and Generalizable Neural Decoding for Quantum LDPC Codes [0.9453554184019106]
  Quantum error correction (QEC) is essential for scalable quantum computing.<n>We propose textbfQuBA, a Bayesian graph neural decoder that integrates attention to both dot-product and multi-head.<n>We further develop textbfSAGU textbf(Sequential Aggregate Generalization under Uncertainty), a multi-code training framework with enhanced cross-domain robustness.
  arXiv  Detail & Related papers  (2025-10-05T01:08:39Z)
• Romanesco codes: Bias-tailored qLDPC codes from fractal codes [0.0]
  We introduce and analyze a family of Clifford-deformed bicycle codes that are tailored for biased noise.<n>Our qLDPC codes are defined on a bipartite hexagonal lattice with limited-range gates and low-weight stabilizers.<n>We find small examples with high encoding rate that perform well for a large range of bias.
  arXiv  Detail & Related papers  (2025-05-30T18:06:24Z)
• Existence and Characterisation of Bivariate Bicycle Codes [0.0]
  We show that BB codes provide compact quantum memory with low overhead and enhanced error correcting capabilities.<n>We explore these codes by leveraging their ring structure and predict their dimension as well as conditions on their existence.
  arXiv  Detail & Related papers  (2025-02-24T11:04:15Z)
• 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)
• 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)
• Neural Belief Propagation Decoding of Quantum LDPC Codes Using Overcomplete Check Matrices [60.02503434201552]
  We propose to decode QLDPC codes based on a check matrix with redundant rows, generated from linear combinations of the rows in the original check matrix. This approach yields a significant improvement in decoding performance with the additional advantage of very low decoding latency.
  arXiv  Detail & Related papers  (2022-12-20T13:41:27Z)
• Finding the disjointness of stabilizer codes is NP-complete [77.34726150561087]
  We show that the problem of calculating the $c-disjointness, or even approximating it to within a constant multiplicative factor, is NP-complete. We provide bounds on the disjointness for various code families, including the CSS codes,$d codes and hypergraph codes. Our results indicate that finding fault-tolerant logical gates for generic quantum error-correcting codes is a computationally challenging task.
  arXiv  Detail & Related papers  (2021-08-10T15:00:20Z)

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.