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.
This paper presents a novel approach to automated theorem proving specifically tailored for quantum circuit verification. The core idea is to construct a formal system that leverages logical reasoning and proof techniques to rigorously analyze quantum circuit designs. This system aims to identify errors and inconsistencies within the circuit, ensuring compliance with the fundamental principles of quantum mechanics. The proposed method moves beyond traditional circuit simulation, offering a mathematically sound guarantee of correctness. We detail the architecture of the theorem prover, focusing on the representation of quantum circuits and the application of proof strategies. The system utilizes a combination of techniques including logical deduction, model checking, and constraint solving, adapted for the unique characteristics of quantum computation. The paper outlines the key components of this system and highlights its potential to significantly improve the trustworthiness and reliability of quantum computing technologies. The central aim is to establish a robust framework for automated verification, reducing the risk of errors and accelerating the development of quantum software.