Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2603.24717

Phased outcome-complete simulation

Vadym Kliuchnikov, Adam Paetznick, Marcus P. da Silva

quant-phSubmitted Mar 25, 2026• Announced Mar 27, 2026• 0 citations
arXivHTMLPDF

Abstract

We generalize the polynomial-time outcome-complete simulation algorithm for stabilizer circuits in arXiv:2309.08676 to track global phases exactly, yielding what we call phased outcome-complete simulation. The original algorithm enabled equivalence checking of stabilizer circuits with intermediate measurements and conditional Pauli corrections for all input states and all measurement outcomes simultaneously, but it tracked quantum states only up to a global phase. Our generalization removes this limitation and enables equivalence checking for an important family of non-stabilizer circuits: stabilizer circuits augmented with single-qubit rotations $\exp(iαZ)$ by symbolic angles. Two such circuits are equivalent if they implement the same quantum channel for all values of the symbolic angles and all measurement outcomes, given a one-to-one correspondence between rotation angles in the two circuits and a mapping between measurement outcomes. This model enables testing of compilation algorithms that transform the Clifford portions of a computation while preserving rotation angles. Examples include Pauli-based computation, edge-disjoint path compilation for surface codes, and custom compilation strategies for reversible circuits such as adders, multipliers, and table lookups. Our efficient classical verification methods extend naturally to circuits with outcome-parity-conditional Pauli gates and intermediate measurements, features that are ubiquitous in fault-tolerant quantum computing but are rarely addressed by existing equivalence-checking approaches.

Comments
13 pages, no figures

Related papers

Stabilizer circuit verification

Vadym Kliuchnikov, Michael E. Beverland, Adam Paetznick

The ubiquity of stabilizer circuits in the design and operation of quantum computers makes techniques to verify their correctness essential. The simulation of stabilizer circuits, which aims to replicate their behavior using a classical computer, is known to be efficient and provides a means of testing correctness. However, simulation is limited in its ability to examine the exponentially large space of possible measurement outcomes. We propose a comprehensive set of efficient classical algorithms to fully characterize and exhaustively verify stabilizer circuits with Pauli unitaries conditioned on parities of measurements. We introduce, as a practical characterization, a general form for such circuits and provide an algorithm to find a general form of any stabilizer circuit. We then provide an algorithm for checking the equivalence of stabilizer circuits. When circuits are not equivalent our algorithm suggests modifications for reconciliation. Next, we provide an algorithm that characterizes the logical action of a (physical) stabilizer circuit on an encoded input. All of our algorithms provide relations of measurement outcomes among corresponding circuit representations. Finally, we provide an analytic description of the logical action induced by measuring a stabilizer group, with application in correctness proofs of code-deformation protocols including lattice surgery and code switching.

arXiv:2309.08676•Sep 15, 2023•1 citation

SyQMA: A memory-efficient, symbolic and exact universal simulator for quantum error correction

George Umbrarescu, David Amaro

The classical simulation of universal quantum circuits is crucial both fundamentally and practically for quantum computation. We propose SyQMA, a simulator with several convenient features, particularly suited for quantum error correction (QEC). SyQMA simulates universal quantum circuits with incoherent Pauli noise and computes exact expectation values and measurement probabilities as symbolic functions of circuit parameters: rotation angles, measurement outcomes, and noise rates. This simulator can sample measurement outcomes, enabling the simulation of dynamic quantum programs where circuit composition depends on prior measurement outputs. For QEC, it performs circuit-level maximum-likelihood decoding, provides exact symbolic expressions for logical error rates, and verifies the fault distance of fault-tolerant (FT) stabiliser and magic state preparation protocols. These features are enabled by an intuitive extension of stabiliser simulators, where each non-Clifford Pauli rotation and incoherent Pauli channel is compactly represented via auxiliary qubits and a modified trace. Representing the state requires only polynomial memory and time, while computing expectation values and measurement probabilities takes exponential time in the number of non-Clifford rotations and deterministic measurements, but only polynomial memory. The FT preparation of stabiliser and magic states, including the first stage of magic state cultivation, is analysed without approximations. We also exactly convert the disjoint error probabilities of a general multi-qubit Pauli channel to independent ones, a key step for creating and sampling from detector error models. The code is publicly available and open-source.

quant-pharXiv:2604.15043•Apr 17, 2026•0 citations

Polynomial-time simulation of non-Clifford quantum error correction

Serban Cercelescu, Mark Koch, Arthur Pesah

We show that every intermediate state of a broad class of non-Clifford quantum error-correction circuits is a third-order phase-polynomial state, even under stochastic Pauli noise. The class includes magic state distillation and cultivation, code switching and gauge fixing, transversal non-Clifford gates with syndrome extraction, and injection of diagonal magic states. Third-order phase-polynomial states strictly generalize stabilizer states, and we prove that they are exactly the stabilizer states of the diagonal-Clifford-and-Pauli (DCP) stabilizer formalism that we introduce. We characterize these states and show that their representations can be updated in polynomial time. This yields an exact polynomial-time simulation algorithm for these circuits and, more broadly, a framework for reasoning about their internal states and about magic states in general. We provide an open-source implementation, \texttt{merlin}, and benchmark it against existing non-Clifford simulators on distillation, cultivation, and code switching circuits. The benchmarks demonstrate improved runtime and memory scaling as the number of logical outputs grows in Bravyi-Haah distillation, and simulation of a code switching circuit beyond the reach of all other tested simulators.

quant-pharXiv:2610.06811•Oct 6, 2026•0 citations

A Simple Method for Compiling Quantum Stabilizer Circuits

Brendan Reid

Stabilizer circuits play an important role in quantum error correction protocols, and will be vital for ensuring fault tolerance in future quantum hardware. While stabilizer circuits are defined on the Clifford generating set,$\{H, S, CX\}$, not all of these gates are native to quantum hardware. As such they must be compiled into the native gateset, with the key difference across hardware archetypes being the native two-qubit gate. Here we introduce an intuitive and accessible method for Clifford gate compilation. While multiple open source solutions exist for quantum circuit compilation, these operate on arbitrary quantum gates. By restricting ourselves to Clifford gates, the compilation process becomes almost trivial and even large circuits can be compiled manually. The core idea is well known: if two Clifford circuits conjugate Paulis identically, they are equivalent. Compilation is then reduced to ensuring that the instantaneous Pauli conjugation is correct for each qubit at every timestep. This is Tableaux Manipulation, so called as we directly interrogate stabilizer tableaux to ensure correct Pauli conjugation. We provide a brief explanation of the process along with a worked example to build intuition; we finally show some comparisons for compiling large circuits to open source software, and highlight that this method ensures a minimal number of quantum gates are employed.

arXiv:2404.19408•IEEE International Conference on Quantum Computing and Engineering (QCE)•Sep 15, 2024•0 citations

Verified Pauli-Product Measurement Compilation for Fault-Tolerant Quantum Computation

John Zhuoyang Ye, Jens Palsberg

Fault-tolerant quantum compilers implement gates through Pauli-product measurements and classical feedback. Verifying such a compiler requires reasoning about the quantum state and the recorded outcomes together: a correction reads an outcome, a gate's internal outcomes must be hidden from its caller, and an application's outcomes must survive optimization. We introduce QPPM, a language for Pauli-product measurement programs, with a weakest-precondition semantics over store-indexed matrix assertions, following quantum Hoare logic with classical variables. Every program terminates, so the Hoare logic is a syntactic presentation of weakest preconditions whose soundness and relative completeness are immediate. Its value is that component specifications compose. All results are mechanized in Lean. We verify lowering of Clifford+$T$ circuits to QPPM with private outcomes and supplied magic states, and an optimizer that eliminates measurements, fuses and reorders rotations, and schedules logical rounds while preserving every outcome that subsequent code can read. A compositional approximation relation bounds the effect of synthesis error on specifications and on output trace distance, and a certificate-checked pipeline selects, among synthesized circuits that meet the user's error limit, the one with the lowest certified depth bound. On QASMBench, verified fusion and scheduling reduce logical measurement depth by a median of 17.9\%, and complete source-to-QPPM allowances are certified for all 35 valid selected small-suite inputs.

quant-pharXiv:2610.31694•Oct 22, 2026•0 citations

Exact efficient simulation of noisy logical magic states using Clifford stabilizers

Yugo Takada, Stephen D. Bartlett, Dominic J. Williamson

The preparation of high-fidelity logical magic states is a crucial subroutine for universal fault-tolerant quantum computation (FTQC). Predicting the performance of FTQC and developing improved protocols rely on numerical methods to classically simulate logical magic state preparation in the presence of noise. Clifford logic on Pauli-stabilizer codes with circuit-level Pauli errors can be efficiently simulated using Pauli-stabilizer formalism, but the non-Clifford operations required to prepare logical magic states render generic simulation inefficient. We introduce Clifford-stabilizer simulation, an exact and efficient algorithm based on updating a Clifford-stabilizer group to simulate noisy preparation protocols for a broad class of logical magic states used to implement non-Clifford gates in the third level of the Clifford hierarchy under circuit-level Pauli errors. Clifford-stabilizer simulation applies to a range of operations that commonly appear in preparation protocols for such logical magic states, including Pauli-stabilizer measurements, logical Clifford measurements, and transversal non-Clifford gates. Our algorithm for Clifford-stabilizer simulation maps a non-Clifford circuit with sampled circuit-level Pauli errors to a Clifford circuit that exactly reproduces its measurement outcome distribution, achieving time and space complexities polynomial in relevant protocol parameters. We perform exact simulation of magic state cultivation up to fault distance 7 by Clifford-stabilizer simulation. Our method provides a route to perform exact benchmarking of large-scale logical magic state preparation protocols required for useful FTQC.

quant-pharXiv:2609.16929•Sep 16, 2026•0 citations
We generalize the polynomial-time outcome-complete simulation algorithm for stabilizer circuits in arXiv:2309.08676 to track global phases exactly, yielding what we call phased outcome-complete simulation. The original algorithm enabled equivalence checking of stabilizer circuits with intermediate measurements and conditional Pauli corrections for all input states and all measurement outcomes simultaneously, but it tracked quantum states only up to a global phase. Our generalization removes this limitation and enables equivalence checking for an important family of non-stabilizer circuits: stabilizer circuits augmented with single-qubit rotations exp⁡(iαZ)\exp(iαZ)exp(iαZ) by symbolic angles. Two such circuits are equivalent if they implement the same quantum channel for all values of the symbolic angles and all measurement outcomes, given a one-to-one correspondence between rotation angles in the two circuits and a mapping between measurement outcomes. This model enables testing of compilation algorithms that transform the Clifford portions of a computation while preserving rotation angles. Examples include Pauli-based computation, edge-disjoint path compilation for surface codes, and custom compilation strategies for reversible circuits such as adders, multipliers, and table lookups. Our efficient classical verification methods extend naturally to circuits with outcome-parity-conditional Pauli gates and intermediate measurements, features that are ubiquitous in fault-tolerant quantum computing but are rarely addressed by existing equivalence-checking approaches.
The ubiquity of stabilizer circuits in the design and operation of quantum computers makes techniques to verify their correctness essential. The simulation of stabilizer circuits, which aims to replicate their behavior using a classical computer, is known to be efficient and provides a means of testing correctness. However, simulation is limited in its ability to examine the exponentially large space of possible measurement outcomes. We propose a comprehensive set of efficient classical algorithms to fully characterize and exhaustively verify stabilizer circuits with Pauli unitaries conditioned on parities of measurements. We introduce, as a practical characterization, a general form for such circuits and provide an algorithm to find a general form of any stabilizer circuit. We then provide an algorithm for checking the equivalence of stabilizer circuits. When circuits are not equivalent our algorithm suggests modifications for reconciliation. Next, we provide an algorithm that characterizes the logical action of a (physical) stabilizer circuit on an encoded input. All of our algorithms provide relations of measurement outcomes among corresponding circuit representations. Finally, we provide an analytic description of the logical action induced by measuring a stabilizer group, with application in correctness proofs of code-deformation protocols including lattice surgery and code switching.
The classical simulation of universal quantum circuits is crucial both fundamentally and practically for quantum computation. We propose SyQMA, a simulator with several convenient features, particularly suited for quantum error correction (QEC). SyQMA simulates universal quantum circuits with incoherent Pauli noise and computes exact expectation values and measurement probabilities as symbolic functions of circuit parameters: rotation angles, measurement outcomes, and noise rates. This simulator can sample measurement outcomes, enabling the simulation of dynamic quantum programs where circuit composition depends on prior measurement outputs. For QEC, it performs circuit-level maximum-likelihood decoding, provides exact symbolic expressions for logical error rates, and verifies the fault distance of fault-tolerant (FT) stabiliser and magic state preparation protocols. These features are enabled by an intuitive extension of stabiliser simulators, where each non-Clifford Pauli rotation and incoherent Pauli channel is compactly represented via auxiliary qubits and a modified trace. Representing the state requires only polynomial memory and time, while computing expectation values and measurement probabilities takes exponential time in the number of non-Clifford rotations and deterministic measurements, but only polynomial memory. The FT preparation of stabiliser and magic states, including the first stage of magic state cultivation, is analysed without approximations. We also exactly convert the disjoint error probabilities of a general multi-qubit Pauli channel to independent ones, a key step for creating and sampling from detector error models. The code is publicly available and open-source.
We show that every intermediate state of a broad class of non-Clifford quantum error-correction circuits is a third-order phase-polynomial state, even under stochastic Pauli noise. The class includes magic state distillation and cultivation, code switching and gauge fixing, transversal non-Clifford gates with syndrome extraction, and injection of diagonal magic states. Third-order phase-polynomial states strictly generalize stabilizer states, and we prove that they are exactly the stabilizer states of the diagonal-Clifford-and-Pauli (DCP) stabilizer formalism that we introduce. We characterize these states and show that their representations can be updated in polynomial time. This yields an exact polynomial-time simulation algorithm for these circuits and, more broadly, a framework for reasoning about their internal states and about magic states in general. We provide an open-source implementation, \texttt{merlin}, and benchmark it against existing non-Clifford simulators on distillation, cultivation, and code switching circuits. The benchmarks demonstrate improved runtime and memory scaling as the number of logical outputs grows in Bravyi-Haah distillation, and simulation of a code switching circuit beyond the reach of all other tested simulators.
Stabilizer circuits play an important role in quantum error correction protocols, and will be vital for ensuring fault tolerance in future quantum hardware. While stabilizer circuits are defined on the Clifford generating set,{H,S,CX}\{H, S, CX\}{H,S,CX}, not all of these gates are native to quantum hardware. As such they must be compiled into the native gateset, with the key difference across hardware archetypes being the native two-qubit gate. Here we introduce an intuitive and accessible method for Clifford gate compilation. While multiple open source solutions exist for quantum circuit compilation, these operate on arbitrary quantum gates. By restricting ourselves to Clifford gates, the compilation process becomes almost trivial and even large circuits can be compiled manually. The core idea is well known: if two Clifford circuits conjugate Paulis identically, they are equivalent. Compilation is then reduced to ensuring that the instantaneous Pauli conjugation is correct for each qubit at every timestep. This is Tableaux Manipulation, so called as we directly interrogate stabilizer tableaux to ensure correct Pauli conjugation. We provide a brief explanation of the process along with a worked example to build intuition; we finally show some comparisons for compiling large circuits to open source software, and highlight that this method ensures a minimal number of quantum gates are employed.
Fault-tolerant quantum compilers implement gates through Pauli-product measurements and classical feedback. Verifying such a compiler requires reasoning about the quantum state and the recorded outcomes together: a correction reads an outcome, a gate's internal outcomes must be hidden from its caller, and an application's outcomes must survive optimization. We introduce QPPM, a language for Pauli-product measurement programs, with a weakest-precondition semantics over store-indexed matrix assertions, following quantum Hoare logic with classical variables. Every program terminates, so the Hoare logic is a syntactic presentation of weakest preconditions whose soundness and relative completeness are immediate. Its value is that component specifications compose. All results are mechanized in Lean. We verify lowering of Clifford+TTT circuits to QPPM with private outcomes and supplied magic states, and an optimizer that eliminates measurements, fuses and reorders rotations, and schedules logical rounds while preserving every outcome that subsequent code can read. A compositional approximation relation bounds the effect of synthesis error on specifications and on output trace distance, and a certificate-checked pipeline selects, among synthesized circuits that meet the user's error limit, the one with the lowest certified depth bound. On QASMBench, verified fusion and scheduling reduce logical measurement depth by a median of 17.9\%, and complete source-to-QPPM allowances are certified for all 35 valid selected small-suite inputs.
The preparation of high-fidelity logical magic states is a crucial subroutine for universal fault-tolerant quantum computation (FTQC). Predicting the performance of FTQC and developing improved protocols rely on numerical methods to classically simulate logical magic state preparation in the presence of noise. Clifford logic on Pauli-stabilizer codes with circuit-level Pauli errors can be efficiently simulated using Pauli-stabilizer formalism, but the non-Clifford operations required to prepare logical magic states render generic simulation inefficient. We introduce Clifford-stabilizer simulation, an exact and efficient algorithm based on updating a Clifford-stabilizer group to simulate noisy preparation protocols for a broad class of logical magic states used to implement non-Clifford gates in the third level of the Clifford hierarchy under circuit-level Pauli errors. Clifford-stabilizer simulation applies to a range of operations that commonly appear in preparation protocols for such logical magic states, including Pauli-stabilizer measurements, logical Clifford measurements, and transversal non-Clifford gates. Our algorithm for Clifford-stabilizer simulation maps a non-Clifford circuit with sampled circuit-level Pauli errors to a Clifford circuit that exactly reproduces its measurement outcome distribution, achieving time and space complexities polynomial in relevant protocol parameters. We perform exact simulation of magic state cultivation up to fault distance 7 by Clifford-stabilizer simulation. Our method provides a route to perform exact benchmarking of large-scale logical magic state preparation protocols required for useful FTQC.