💻 computer science

Parametric Proof-Carrying Compilation for Quantum Error-Correction

This paper introduces PC-QEC, a Lean 4-mechanized proof-carrying compilation framework that generates distance-independent symbolic certificates to formally verify circuit-level distance guarantees for five quantum code families across four syndrome-extraction schemes.

Original author: John Zhuoyang Ye, Jens Palsberg

Published 2026-11-11

📖 6 min read🧠 Deep dive

CC BY 4.0

Original author: John Zhuoyang Ye, Jens Palsberg

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the author. For technical accuracy, refer to the original paper. Read full disclaimer

Quantum computers promise to solve problems that would take ordinary machines thousands of years, but they are incredibly fragile. The tiny particles that carry information, called qubits, are easily disturbed by heat, vibration, or stray electromagnetic fields. A single mistake can corrupt the entire calculation. To build a machine that works, scientists must protect these fragile bits using a technique called quantum error correction. This method does not stop errors from happening; instead, it spreads the information across many physical particles so that if one fails, the system can detect the mistake and fix it without losing the data. The system works by constantly checking the state of the particles using special helper particles, a process known as syndrome extraction. If the checks reveal a problem, a classical computer calculates the necessary correction. However, the very act of checking can sometimes introduce new errors, creating a complex web where a single glitch in a helper particle can spread to several data particles, potentially causing a catastrophic failure.

The central challenge for engineers is to prove that a specific design for checking and correcting errors is actually strong enough to work. They need to know the "distance" of the code, which is a measure of how many independent errors the system can tolerate before it fails. If the distance is too low, the machine will break down before it can finish a long calculation. Calculating this distance for a single, small circuit is difficult, but calculating it for a whole family of circuits that can grow to any size is nearly impossible with traditional methods. Usually, proving the safety of a larger system requires checking every single component individually, a task that grows so large it becomes unmanageable. Without a way to prove these distances for any size, designers cannot be sure their quantum computers will scale up to handle real-world problems.

A team of researchers at the University of California, Los Angeles, has developed a new method to solve this problem. They created a system called PC-QEC, which acts like a rigorous inspector for quantum error-correction designs. Instead of checking one specific size at a time, their method produces a single, finite proof that guarantees safety for an entire family of circuits, regardless of how large they grow. This proof is "parametric," meaning it works for any code distance the user chooses, from the smallest possible size to the largest imaginable. The researchers demonstrated that this proof holds true for five different types of quantum codes and works with four distinct ways of performing the error checks.

The core of their discovery relies on a clever way of tracking how errors move through the system. When a helper particle makes a mistake, it can create a "hook error," where the fault spreads to multiple data particles. The researchers found that while these hook errors look dangerous, they cross a specific set of invisible boundaries in the circuit in a predictable way. In contrast, a true logical error—one that destroys the data—must cross all of these boundaries. By proving that a single fault can only cross a limited number of these boundaries, they showed that a small number of faults can never add up to a total system failure. This insight allows them to separate the mathematical properties of the code from the specific details of the hardware, creating a certificate that proves the system is safe.

The researchers tested their method on the rotated Surface code, a leading candidate for building real quantum computers. They generated a single proof that guarantees a specific level of safety for every odd-numbered code distance starting from three. This proof is compact and does not grow larger as the circuit gets bigger. When they checked this proof against a specific circuit, the verification process took about 214 seconds on average. This is a significant improvement over previous methods, which would require exponentially more time and effort as the circuit size increased. The team also verified that their method works for other complex codes, including hypergraph-product codes and Toric codes, proving that the safety guarantees hold across different geometric arrangements of qubits.

To ensure their results were not just theoretical, the researchers also showed that their safety guarantees are exact. They constructed a specific scenario where exactly the number of faults predicted by their distance measure would cause a failure, proving that the system cannot be any more robust than their proof claims. This matching of the lower bound (the minimum safety) and the upper bound (the point of failure) confirms that their method provides a precise and reliable measure of circuit strength. The work also highlights how the specific order in which the system checks for errors matters; changing the sequence of operations can either preserve the safety or weaken it, and their proof captures these nuances automatically.

The implications of this work extend beyond just one type of quantum computer. The researchers built their system to be flexible, allowing it to check different designs and different error models without starting from scratch. They showed that the same underlying logic can be applied to various extraction schemes, including the Standard, Flag, Shor, and Knill methods. This flexibility means that as engineers experiment with new ways to build quantum hardware, they can use this tool to instantly verify if their new design is safe. The ability to generate a single, reusable proof for an entire family of circuits removes a major bottleneck in the development of fault-tolerant quantum computers.

The researchers used a formal verification tool called Lean 4 to mechanize the logic behind their proofs, ensuring that every step of their reasoning is mathematically sound. This means that the results are not based on simulations or approximations, but on rigorous mathematical deduction. By separating the high-level logic of the code from the low-level details of the gates and wires, they created a framework where the safety of the system can be trusted even as the hardware evolves. This approach mirrors the way software engineers use certificates to verify code, but adapted for the unique challenges of quantum physics.

In the end, this research provides a foundational tool for the future of quantum computing. It answers the critical question of how to be sure that a quantum error-correction scheme will work as it scales up. By providing a method to prove safety for any size, the researchers have given engineers a way to design larger, more reliable quantum computers with confidence. The work demonstrates that it is possible to tame the complexity of quantum errors with a structured, provable approach, paving the way for machines that can perform the long, complex calculations that were previously thought impossible.

Technical Summary: Parametric Proof-Carrying Compilation for Quantum Error-Correction

Problem Statement

Long-duration quantum computations, such as Shor's factoring algorithm, require reliable logical qubits despite noisy physical operations. Quantum Error Correction (QEC) encodes logical information across physical qubits to detect and correct errors. However, the syndrome extraction circuits used to measure stabilizers can themselves introduce errors. A single fault on an ancilla qubit can propagate to multiple data qubits, creating "hook errors" that may mimic logical errors or cancel evidence of data errors.

The central challenge addressed is establishing circuit-level code distance ( $d_{circ}$ ), defined as the minimum number of injected Pauli faults required to produce a logical data error without triggering any detector. Computing this distance is generally NP-hard. Furthermore, QEC codes exist as families (e.g., Surface codes with varying distances $d$ ), where increasing $d$ changes the number of qubits, stabilizers, and gates. Traditional verification methods often require re-proving properties for each specific instance, leading to proofs that grow with $d$ . The authors seek a finite, parametric proof that guarantees circuit-level distance for an entire family of codes, independent of the specific code distance $d$ , while accounting for different syndrome extraction schemes (Standard, Flag, Shor, and Knill).

Methodology: PC-QEC Framework

The authors present PC-QEC (Parametric Proof-Carrying Quantum Error Correction), a framework that compiles a symbolic proof alongside the extraction circuit. The approach separates the high-level code algebra from the implementation details of fault propagation.

1. Three-Layer Architecture

The framework operates across three distinct layers:

CodeML (Source): A parametric language that describes code families using ordered Pauli factors. It defines stabilizers and their coupling orders (e.g., $Z_0 Z_3 Z_1 Z_4$ ) symbolically. It supplies algebraic premises regarding code well-formedness and the geometric properties of logical errors.
QStab (Intermediate Representation): An IR that tracks the residual data error, readout offsets, and fault budget at stabilizer-measurement boundaries. It establishes a program invariant relating the number of faults ( $\ell$ ) to the "cut signatures" of the residual error.
QClifford (Target): The emitted Clifford circuit (Hadamard, CNOT, measurements) with explicit fault sites. It uses fault-aware Hoare logic to verify that the gate-level implementation preserves the invariants established in QStab.

2. The Core Mechanism: Cut Signatures

The key innovation is the use of parity probes (cuts) to distinguish logical errors from hook errors.

Logical Errors: In the Surface code, a logical error (e.g., a row of $Z$ errors) crosses all $d$ cuts in a specific collection (e.g., all columns).
Hook Errors: A hook error caused by a single ancilla fault crosses at most one cut in each collection. This is achieved by carefully ordering the coupling of data qubits to the ancilla (e.g., pairing qubits in the same column) so that their contributions cancel out in the cut signature, leaving at most one uncanceled contribution.

The proof relies on two main properties:

Code Algebra: Every logical error must cross at least $d$ cuts in some collection.
Program Invariant: With $\ell < d$ faults, the residual error can cross at most $\ell$ cuts in any collection.

Since $\ell < d$ , the invariant ensures the residual cannot satisfy the condition for a logical error.

3. Proof-Carrying Compilation

The system generates a finite symbolic certificate whose size is independent of $d$ .

Induction: Instead of enumerating gates for a specific $d$ , the proof uses induction on the code distance and the number of stabilizer measurements.
Symbolic Bounds: The proof tracks symbolic expressions for cut signatures and fault counts.
Translation: The compiler translates the source invariant (QStab) into a target Hoare proof (QClifford) by verifying that each gate and fault site preserves the cut bounds, accounting for "pending" contributions from ancilla qubits that have not yet been fully propagated.

Key Contributions

Parametric Proof-Carrying Compilation: PC-QEC is the first framework to provide a finite, symbolic proof of circuit-level code distance for entire families of QEC codes, valid for every legal code distance $d$ .
Universal Scheme Support: The framework covers four major syndrome extraction schemes (Standard, Flag, Shor, and Knill) and demonstrates that the same high-level proof structure can be adapted to different backend implementations.
Circuit-Level Distance Guarantees: The system proves that for the Rotated Surface code, the circuit-level distance $d_{circ}$ is exactly $d$ for all odd $d \ge 3$ under the Standard Scheme. It also provides lower bounds for other families (Hypergraph-Product, Toric, Triangular Color codes).
Mechanized Metatheory: The soundness and exactness of the approach are mechanized in Lean 4 for canonical Surface, HGP, and Toric code families.
Efficient Verification: The authors demonstrate that checking a symbolic certificate for a family (e.g., all odd $d \ge 3$ for Rotated Surface code) takes a finite amount of time (average 214 seconds) and does not require re-running the proof for each specific $d$ .

Results

The evaluation covers five code families and multiple extraction schemes:

Rotated Surface Code: Proves $d_{circ} = d$ for all odd $d \ge 3$ under the Standard Scheme. The symbolic certificate checks in an average of 214 seconds.
Other Families:
- Unrotated Surface Code & Toric Code: Proves $d_{circ} = d$ .
- Cartesian LP Code: Proves $d_{circ} = 4t$ (where $t$ is a parameter).
- Triangular Color Code: Proves a lower bound of $\lceil d/3 \rceil$ due to reduced-weight invariants.
Finite Instances: The system successfully verified finite circuits for codes like the 5-qubit, Steane, and Shor codes, showing how extraction choices (e.g., coupling order) directly impact the certified distance. For instance, changing the coupling order in a Shor code from block to interleaved restored the distance from 1 to 3.
Performance: Checking times for finite target circuits ranged from 0.2 to 0.5 seconds. The most complex symbolic checks (Cartesian LP and Color codes) took several thousand seconds, reflecting the complexity of the algebraic premises rather than the circuit size.

Significance and Claims

The paper claims that PC-QEC bridges the gap between high-level code algebra and low-level circuit fault tolerance. By separating the geometric proof of logical error properties from the implementation-specific proof of fault propagation, the framework enables scalable testing and formal verification of QEC circuits.

The authors emphasize that their approach provides a finite symbolic certificate that justifies the distance premise for scalable testing tools (like ScaLER) without needing to re-prove the distance for every new code size. The work demonstrates that it is possible to verify the circuit-level distance of an entire infinite family of codes with a proof of fixed size, provided the code family and extraction scheme adhere to specific algebraic and ordering contracts. The paper does not claim to optimize the logical error rate numerically but rather to provide a rigorous, machine-checked guarantee that the circuit-level distance meets the theoretical code distance under declared fault and readout contracts.