Quasilinear Equivalence Checking for Detector Error Models

This paper introduces a sound, terminating, and confluent rewriting system for Detector Error Models (DEMs) that computes unique normal forms in quasilinear time, providing the first complete static decision procedure for verifying decoder equivalence in non-adaptive quantum error correction pipelines and a scalable approach for partially-adaptive circuits.

The Gist

Imagine you are trying to fix a very complex, delicate machine made of quantum parts. Because these parts are so sensitive, they occasionally glitch. To fix them, you need a "decoder"—a smart computer program that looks at the symptoms of the glitches and guesses exactly what went wrong so it can apply the right fix.

To teach this decoder, engineers use a special instruction manual called a Detector Error Model (DEM). Think of a DEM as a recipe card. It lists every possible way the machine can break, how likely each break is, and exactly which "alarm lights" (detectors) will flash and which "score counters" (logical observables) will change when that break happens.

The Problem: Two Manuals, One Truth

Sometimes, engineers rewrite the machine's code to make it faster or smaller. They might change the order of steps or combine two small steps into one big step. If they do this correctly, the machine should behave exactly the same way.

However, the instruction manual (the DEM) generated after the rewrite might look completely different on paper than the one before the rewrite.

• Old Manual: "Step A breaks 10% of the time. Step B breaks 20% of the time."
• New Manual: "Step C breaks 26% of the time."

Even though the math says these are the same outcome, a computer checking them might get confused. Usually, to check if two manuals are the same, engineers have to run millions of simulations (like rolling dice billions of times) to see if the results match. This is slow, expensive, and never 100% certain.

The Solution: A New Way to Compare

This paper introduces a new, super-fast mathematical method to check if two DEM instruction manuals are actually describing the exact same reality, without needing to run any simulations.

The authors treat these manuals like Lego sets or sentence structures. They created a set of simple rules (a "rewriting system") that allow you to simplify any manual down to its most basic, unique form.

Here is how their method works, using everyday analogies:

1. The "Cancel Out" Rule (XOR Semantics)

Imagine you have a light switch. If you flip it once, the light turns on. If you flip it twice, it turns off.
In these manuals, if an error triggers the same alarm light twice, they cancel each other out (like flipping the switch twice). The authors' rules automatically spot these duplicates and remove them, simplifying the list.

2. The "Merge" Rule

Imagine you have two separate notes saying:

• "There is a 10% chance the engine sputters."
• "There is a 20% chance the engine sputters."

If these happen independently, you can combine them into one note: "There is a 26% chance the engine sputters." The authors' system automatically finds all instructions that affect the exact same parts and merges them into a single, clean instruction.

3. The "Order Doesn't Matter" Rule

If you have a list of errors, the order you write them in doesn't change the outcome. It's like a grocery list: "Milk, Eggs, Bread" is the same list as "Bread, Milk, Eggs." The system ignores the order and just looks at the content.

The Result: The "Normal Form"

By applying these rules, the system takes any messy, complex manual and turns it into a Unique Normal Form.

• Think of this like a fingerprint. No matter how you write the manual (long, short, shuffled, or messy), if it describes the same machine behavior, it will always reduce to the exact same fingerprint.
• If two manuals reduce to the same fingerprint, they are equivalent. If they are different, they are not.

Why This is a Big Deal

• Speed: The paper proves this method is incredibly fast. It can check massive manuals in a time that grows almost linearly with the size of the manual (quasilinear time). It's like sorting a deck of cards instantly, whereas the old simulation method was like trying to guess the order by shuffling the deck a million times.
• Certainty: Unlike simulations which only give a "probably," this method gives a 100% mathematical guarantee.
• Scope: It works perfectly for standard quantum error correction (where the machine follows a fixed schedule). For more complex, "adaptive" machines (where the machine changes its plan based on what it sees), the method still works very well, though it has to be slightly more careful.

The Bottom Line

The authors have built a "spell-checker" for quantum error models. Instead of running expensive simulations to see if two versions of a quantum circuit are safe, engineers can now use this algebraic tool to instantly verify that the safety instructions are identical. This ensures that when quantum computers are optimized or compiled, their ability to fix their own errors remains intact.

Technical Summary

Technical Summary: Quasilinear Equivalence Checking for Detector Error Models

Problem Statement

In quantum error correction (QEC), Detector Error Models (DEMs) serve as a structured representation of error mechanisms, bridging noisy quantum circuits and classical decoding algorithms. Generated by tools like Stim, DEMs list physical fault channels, their probabilities, the detectors they trigger, and the logical observables they flip.

A critical challenge in quantum compilation pipelines is verifying that circuit transformations (e.g., optimizations or stitching of lattice surgery patches) preserve the underlying fault model. Two DEMs are considered equivalent if they are decoder-equivalent, meaning they induce the same joint probability distribution over detector and observable outcomes. Currently, verifying this equivalence relies on statistical sampling (Monte Carlo methods), which suffers from exponential sample complexity in the presence of rare events and provides only probabilistic guarantees. There is a lack of a static, deterministic decision procedure for DEM equivalence that scales efficiently.

Methodology

The paper proposes a formal categorical abstraction for DEMs, moving from raw file semantics to an equational theory.

1. Term Language and Semantics

The authors define a term language for DEMs where instructions are composed sequentially and grouped within REPEAT blocks.

• Categorical Framework: DEMs are modeled as morphisms in a discrete symmetric monoidal category (a PROP) over the Giry monad, capturing the probabilistic composition of error events.
• Scope-Local Equivalence: A key insight is that equivalence should be defined locally within each "scope" (the top level or the body of a repeat block). Instructions in different repeat iterations refer to distinct time steps and are not necessarily independent; thus, rewriting across scope boundaries is restricted.
• XOR Semantics: Targets (detectors and observables) carry XOR semantics; an even number of occurrences cancels out. Probabilities combine via the XOR-fold operation ($p \oplus q = p + q - 2pq$).

2. Rewriting System

A sound, terminating, and confluent rewriting system $\mathcal{R}$ is presented to normalize DEM terms. The rules include:

• Fusion (R1): Merging instructions with identical target sets by XORing their probabilities.
• Cancellation (R2, R3): Removing zero-probability instructions, empty targets, and duplicate targets within a single instruction.
• Commutativity (R4): Reordering instructions within the same scope, as error events are independent.
• Congruence (R5): Allowing rewriting within the body of a REPEAT block without altering the block's structure.

3. Decision Procedure

The system proves that every DEM term has a unique normal form (up to permutation of instructions within a scope). This normal form is computed by:

1. Resolving relative detector indices to absolute ones.
2. Applying rewriting rules to cancel duplicates and fuse probabilities.
3. Sorting instructions by their effective target sets.

The equivalence of two DEMs is decided by comparing their normal forms.

Key Contributions and Results

1. Quasilinear Decision Procedure

The paper establishes a decision procedure for scope-local equivalence with a time complexity of $O(k|E| \log |E|)$, where $|E|$ is the number of instructions and $k$ is the maximum size of a target set. This is a significant improvement over simulation-based approaches.

• Invariants: The normal form corresponds to a unique Tanner graph (a bipartite graph of targets and error instructions with probability labels), which serves as a complete set of invariants for the equational theory.

2. Completeness for Non-Adaptive QEC

The authors prove that for non-adaptive QEC pipelines (where logical measurements occur at fixed schedule points), scope-local equivalence is equivalent to full decoder-equivalence.

• Observable-Separation: In standard pipelines (e.g., surface codes), logical observables appear in at most one scope. Under this condition, the static decision procedure decides full decoder-equivalence exactly, regardless of circuit depth or repeat block nesting.

3. Soundness for Adaptive QEC

For partially-adaptive circuits (e.g., lattice surgery, distributed QEC with mid-circuit measurements), the strict observable-separation property may be violated.

• Hybrid Approach: The paper introduces observable-coherence classes to partition scopes based on shared logical observables.
• Result: The procedure remains sound (if the normal forms match, the DEMs are decoder-equivalent) for adaptive protocols. While it may not be complete (it might fail to detect equivalence in some complex adaptive cases), it avoids the exponential overhead of global unrolling by performing local unrolling only within overlapping coherence classes.

Significance and Claims

The paper claims to provide the first static decision procedure for DEM equivalence with rigorous correctness guarantees. Its significance lies in:

• Verification: Enabling the verification that quantum compilation passes preserve fault tolerance without relying on expensive statistical sampling.
• Optimization: Providing a foundation for optimizing DEMs while preserving their semantics.
• Compiler Regression Testing: Offering a tool to ensure that different versions of a compiler generate semantics-equivalent DEMs.
• Theoretical Foundation: Establishing a categorical semantics for error models using the Giry monad and symmetric monoidal theories, connecting QEC formalisms to broader concepts in categorical probability and diagrammatic languages.

The authors note that while a completeness result for all adaptive protocols remains an open theoretical challenge, the proposed hybrid procedure is sufficient for practical compiler regression testing, where the false negative rate is expected to be negligible. The work also lays the groundwork for future integration with proof assistants and the development of tools like emlint for static analysis.