Quasilinear Equivalence Checking for Detector Error Models
2026-06-12 • Logic in Computer Science
Logic in Computer ScienceProgramming LanguagesSoftware Engineering
AI summaryⓘ
The authors study a way to represent errors in quantum circuits called Detector Error Models (DEMs). They create a formal mathematical system that helps analyze and simplify these error models in a reliable and efficient manner. Their method can uniquely identify when two error models are essentially the same and can decide this quickly, even for complex quantum error correction setups. This work can aid in checking and improving quantum computing processes by ensuring errors are correctly understood and managed.
Quantum circuitsDetector Error ModelQuantum error correctionEquational theorySymmetric monoidal theoryGiry monadRewriting systemTanner graphsQuantum compilerDecoder equivalence
Authors
Mathys Rennela
Abstract
A Detector Error Model (DEM) is a structured representation of error mechanisms in quantum circuits, which has gained popularity in quantum compilation pipelines for its ability to capture fault-tolerance at a circuit level. It lists error mechanisms as instructions targeting detectors and observables, specifying for each physical fault channel the probability that the fault fires, the detectors it triggers, and the observables it flips. In this paper, we develop an equational theory for DEMs, with its associated categorical semantics. We present a sound, terminating, confluent rewriting system for DEM terms, formulating it as a symmetric monoidal theory (a PROP) over the Giry monad. We prove that every DEM term has a unique normal form, which can be computed efficiently in quasilinear time $O(k|E|\log|E|)$, where $|E|$ is the number of instructions and $k$ bounds the size of a target set. This provides a complete set of invariants (via Tanner graphs) for structural DEM equivalence. We provide the first static decision procedure for DEM equivalence, with rigorous correctness guarantees. It is complete (decides full decoder-equivalence exactly) for non-adaptive quantum error correction (QEC) pipelines, and scales to a sound and applicable decision procedure for partially-adaptive circuits (lattice surgery, distributed QEC, ...) without suffering exponential overhead. We discuss its application to the verification and optimisation of quantum compilers.