Structure-Aware Quantum Circuit Equivalence Checking via Sparse Pauli Propagation

arXiv:2611.15080v1 [cs.SE] 11 Nov 2026

Structure-Aware Quantum Circuit Equivalence Checking via Sparse Pauli Propagation SHANGZHOU XIA∗ , Kyushu University, Japan JUNJIE LUO∗ , RIKEN Center for Quantum Computing, Japan QICHEN WANG, Kyushu University, Japan YASUNARI SUZUKI, RIKEN Center for Quantum Computing, Japan JIANJUN ZHAO† , Kyushu University, Japan Quantum circuit equivalence checking is essential for validating compiler optimizations, but its computational cost can vary substantially with circuit structure. We present a structure-aware equivalence checker for unitary quantum circuits based on sparse Pauli propagation. It combines two complementary verification strategies: generator propagation compares the conjugation actions of the circuits on Pauli generators, while Cut-Miter exploits cancellation between circuit products at selected cut points. A structure-aware verification procedure uses circuit characteristics to select between these strategies while explicitly accounting for numerical and approximation errors. We evaluate our framework against three existing equivalence checkers on two benchmark suites containing circuit pairs with up to 512 qubits. Across 434 scored circuit pairs, our framework produces reference-consistent decisions for 96.3% of the pairs without any incorrect verdicts, while the evaluated baselines achieve at most 68.7% reference-consistent decisions. It also achieves the lowest aggregate runtime among the evaluated tools, reducing total runtime by 48.5%–76.0% relative to these baselines. Ablation studies confirm the benefits of cut-based verification, Pauli-term pruning, and bounded propagation attempts. These results indicate that structure-aware sparse Pauli propagation, combined with complementary verification strategies and explicit error accounting, can provide an effective approach to practical quantum circuit equivalence checking. CCS Concepts: • Software and its engineering → Software verification and validation. Additional Key Words and Phrases: Equivalence Checking, Quantum Software Verification, Pauli Propagation

1

Introduction

Quantum programs typically undergo rewriting and optimization during compilation [32, 37], including decomposing high-level operations, canceling or commuting gates, synthesizing alternative subcircuits, and translating circuits into hardware-supported gate sets. These transformations may substantially alter the syntax and structure of a circuit, but must preserve its semantics. However, several studies [16, 17, 24, 33] have revealed semantic inconsistencies after such transformations in widely used quantum development frameworks. Consequently, semantic regression checking has become an important component of building reliable quantum software systems. To address this problem, existing research has primarily pursued two approaches: testing and verification. Quantum transformation testing typically follows the metamorphic testing paradigm [17, 24]. By executing the original and transformed circuits separately on quantum devices, one can obtain only a finite number of samples from their output distributions. However, matching the observed samples cannot establish equivalence for all possible inputs, and discrepancies may ∗ Both authors contributed equally to this research. † Corresponding author.

Authors’ Contact Information: Shangzhou Xia, Kyushu University, Fukuoka, Japan, xia.shangzhou.218@s.kyushu-u.ac.jp; Junjie Luo, RIKEN Center for Quantum Computing, Wako, Saitama, Japan, junjie.luo@riken.jp; Qichen Wang, Kyushu University, Fukuoka, Japan, wang.qichen.256@s.kyushu-u.ac.jp; Yasunari Suzuki, RIKEN Center for Quantum Computing, Wako, Saitama, Japan, yasunari.suzuki@riken.jp; Jianjun Zhao, Kyushu University, Fukuoka, Japan, zhao@ait.kyushu-u.ac.jp. 2026. ACM XXXX-XXXX/2026/11-ART https://doi.org/10.1145/nnnnnnn.nnnnnnn

, Vol. 1, No. 1, Article . Publication date: November 2026.

2

Shangzhou Xia, Junjie Luo, Qichen Wang, Yasunari Suzuki and Jianjun Zhao

be masked by statistical noise arising from a finite number of shots as well as hardware errors, making it difficult to construct an effective test oracle. Quantum equivalence checkers typically avoid explicit state-vector simulation by leveraging representations such as decision diagrams, ZX diagrams, path sums, weighted model counting, and Pauli propagation [6, 14, 19, 26, 30]. These techniques have enabled the verification of quantum circuits far beyond the scale tractable by dense-matrix comparison. Nevertheless, their performance remains highly dependent on circuit structure. A representation that is compact for one class of circuits may grow exponentially for another. More subtly, even when the final equivalence condition admits a compact representation, establishing that condition may require constructing intermediate states of enormous size. Consequently, relying on a single symbolic representation and a fixed propagation strategy can create a representation bottleneck: even when a sparse representation exists for the same verification problem, a checker may still fail if intermediate representations become dense, leading to memory exhaustion or excessive runtime. Our key observation is that quantum-circuit equivalence exposes two complementary forms of sparsity. The first is action sparsity. For Clifford-dominated circuits, the conjugation of a Pauli generator by the circuit remains compact. Equivalence can therefore be checked by comparing the images of the 2𝑛 generators without constructing either circuit’s complete operator. The second is difference sparsity. Circuits produced by compiler rewrites, or local mutations, frequently share substantial structure, even when each circuit is individually expensive to propagate. By constructing their miter 𝑈 2†𝑈 1 from the two sides in an alternating order, common structure can cancel early, and the remaining difference may stay sparse. Neither form of sparsity dominates universally: Clifford circuits may have simple generator actions even when their Pauli expansions are exponentially large, whereas rotation-dense circuit pairs may admit compact difference operators even when independent propagation is expensive. Based on this observation, we present a structure-aware equivalence checker for unitary quantum circuits. Instead of committing to one representation, our framework organizes these complementary Pauli-propagation engines as a bounded portfolio. Generator backend independently propagates the Pauli generators through both circuits and compares their conjugation actions. Cut-Miter backend searches several circuit cut points and compares partial products at a potentially sparser boundary and incrementally constructs a sparse Pauli representation of 𝑈 2†𝑈 1 , consuming operations from both circuits so that aligned structure is eliminated as early as possible. A lightweight router selects an initial engine using circuit characteristics, including the number and proportion of non-Clifford rotations. Failed fast paths consume only bounded slices of the available resources and fall back to more general verification paths. This portfolio is designed not only for performance but also for dependable use as a software-testing oracle. All engines decide the same semantic property using complete residual 𝐿2 mass rather than individual Pauli coefficients, since a semantic difference may be distributed across many individually small coefficients. Our framework explicitly tracks the errors introduced by Pauli-term pruning and semantic lowering, and uses the resulting error bound to certify Eqivalent or Not-Eqivalent when the residual is sufficiently separated from the tolerance. Otherwise, it returns Undecided rather than treating numerical or resource limitations as evidence of equivalence. We evaluate our framework on 434 scored circuit pairs from two benchmark suites, with circuit widths ranging up to 512 qubits, against three existing equivalence checkers. Our framework returns correct, reference-consistent decisions for 96.3% of the scored pairs with no incorrect verdicts, compared with at most 68.7% correct decisions for the evaluated baselines. It also achieves the lowest aggregate runtime, reducing total runtime by 48.5%–76.0% relative to these tools. The results illustrate the benefit of adapting the verification strategy to circuit structure: cut-miter

, Vol. 1, No. 1, Article . Publication date: November 2026.

Structure-Aware Quantum Circuit Equivalence Checking via Sparse Pauli Propagation

3

comparisons exploit cancellation between related circuits, whereas generator propagation can efficiently handle circuits with substantial Clifford structure. Ablation results further show that both cut-based verification and Pauli-term pruning are important for maintaining decision coverage and controlling computational cost, while bounded generator attempts prevent expensive propagation cases from consuming the entire verification budget. Finally, varying the pruning threshold from 10−12 to 10−14 changes the outcome of only one of 438 evaluated instances and introduces no EQ–NEQ switches, indicating that the observed decisions are stable across the tested range. These results support the effectiveness of a bounded, structure-aware portfolio for practical quantum circuit equivalence checking. The contribution is listed as follows: • A structure-aware equivalence checking method. We combine Pauli-generator propagation with cut-point partial-product comparison to exploit compact circuit actions and cancellation between circuits. The method selects between these strategies according to circuit structure and resource limits. • Numerical decisions with approximation error bounds. We formulate equivalence decisions using residual norms and accumulated errors from pruning and semantic lowering. • An implementation and empirical evaluation. We implement our framework and evaluate it against three existing checkers on two benchmark suites, obtaining more correct decisions and lower aggregate runtime. Ablation and sensitivity studies examine the contributions of individual components and the effect of pruning thresholds. The remainder of this paper is organized as follows. Section 2 provides the necessary background. Section 3 presents our methodology. Section 4 describes the experimental setup and discusses the empirical results. Section 5 discusses the threats to validity, while Section 6 reviews related work. Finally, Section 7 concludes the paper. 2 2.1

Background Quantum Circuits and Unitary Semantics 𝑛

An 𝑛-qubit pure state is represented by a unit vector |𝜓 ⟩ ∈ C2 . A unitary gate acting on 𝑘 qubits is described by a 2𝑘 × 2𝑘 unitary matrix and is embedded into the 𝑛-qubit state space according to the qubits on which it acts. Common single-qubit gates include the Pauli gates 𝑋 , 𝑌 , and 𝑍 , the Hadamard gate 𝐻 , and the rotation gates 𝑅𝜎 (𝜃 ) = exp(−𝑖𝜃𝜎/2),

𝜎 ∈ {𝑋, 𝑌 , 𝑍 }.

(1)

Multi-qubit gates, such as the controlled-NOT gate CX, introduce interactions between qubits. We consider quantum circuits composed of unitary gates. If the gates of a circuit 𝐶 are applied in the order 𝐺 1, 𝐺 2, . . . , 𝐺𝑚 , its unitary semantics is 𝑈𝐶 = 𝐺𝑚𝐺𝑚−1 · · · 𝐺 1 . Thus, for an input state |𝜓 ⟩, the circuit produces 𝑈𝐶 |𝜓 ⟩. Because multiplication order is significant, two circuits may contain similar gates while implementing different unitary transformations. A quantum state can also be described by a density operator 𝜌, a positive semidefinite matrix with trace one. For a pure state, 𝜌 = |𝜓 ⟩ ⟨𝜓 |. A circuit with unitary 𝑈𝐶 transforms it into 𝑈𝐶 𝜌𝑈𝐶† . An 𝑛-qubit Pauli string is a tensor product 𝑃 = 𝑃 1 ⊗ · · · ⊗ 𝑃𝑛 , where each 𝑃 𝑗 belongs to {𝐼, 𝑋, 𝑌 , 𝑍 }. We write P𝑛 for the set of these strings. The strings 𝑋 𝑗 and 𝑍 𝑗 act as 𝑋 and 𝑍 , respectively, on qubit 𝑗 and as 𝐼 on all other qubits. A Clifford gate maps each Pauli string under conjugation to another Pauli string, possibly with a sign change. Common Clifford gates include the Pauli gates, 𝐻 , 𝑆, and CX. Non-Clifford gates, including 𝑇 and generic rotations, can produce a linear combination of Pauli strings. , Vol. 1, No. 1, Article . Publication date: November 2026.

4

Shangzhou Xia, Junjie Luo, Qichen Wang, Yasunari Suzuki and Jianjun Zhao

2.2

Quantum Circuit Equivalence Checking

As quantum computing continues to advance, quantum circuits are increasingly processed by compilation and optimization techniques [18, 21, 23] to improve their execution efficiency and adapt them to the constraints of quantum hardware. These transformations may substantially change the structure of a circuit, producing circuit variants that are syntactically different from the original while being expected to implement the same quantum operation. Therefore, it is essential to verify that such transformations preserve the semantics of the original circuit. Quantum circuit equivalence checking [5, 6, 14, 19, 26, 31, 36] addresses this need by determining whether two quantum circuits implement the same quantum operation, typically up to a global phase. It thus provides a fundamental correctness guarantee for quantum circuit compilation and optimization. Definition 2.1 (Equivalence). Two 𝑛-qubit circuits 𝐶 1 and 𝐶 2 with unitaries 𝑈 1 and 𝑈 2 are equivalent, written 𝐶 1 ≡ 𝐶 2 , if 𝑈 1 = 𝑒 𝑖𝜑 𝑈 2 for some 𝜑 ∈ [0, 2𝜋). The factor 𝑒 𝑖𝜑 is a global phase and does not affect measurement probabilities. Since 𝑈 2†𝑈 2 = 𝐼 , Definition 2.1 is equivalent to 𝑀 = 𝑈 2†𝑈 1 = 𝑒 𝑖𝜑 𝐼 . (2) The composite operator 𝑀 is called a miter. It reduces equivalence checking to determining whether a single operator equals the identity up to a global phase. 2.3

Pauli Propagation

Pauli propagation provides a compact way to represent and analyze quantum operators without explicitly constructing their exponentially large matrix representations. Let P𝑛 = {𝐼, 𝑋, 𝑌 , 𝑍 } ⊗𝑛 denote the 𝑛-qubit Pauli basis. Any 𝑛-qubit operator 𝐴 can be expressed as a linear combination of Pauli strings, ∑︁ 𝐴= 𝛼 𝑃 𝑃, (3) 𝑃 ∈ P𝑛

where 𝛼 𝑃 is the coefficient associated with Pauli string 𝑃. Pauli strings can be efficiently manipulated using the multiplication rules of the single-qubit Pauli operators. For example, 𝑋𝑌 = 𝑖𝑍,

𝑌 𝑍 = 𝑖𝑋,

𝑍𝑋 = 𝑖𝑌 .

(4)

The single-qubit identities 𝑋 2 = 𝑌 2 = 𝑍 2 = 𝐼 further imply that the product of any two Pauli strings is another Pauli string up to a phase in {1, −1, 𝑖, −𝑖}. For example, (𝑋 ⊗ 𝑍 ) (𝑌 ⊗ 𝑋 ) = (𝑋𝑌 ) ⊗ (𝑍𝑋 ) = 𝑖𝑍 ⊗ 𝑖𝑌 = −𝑍 ⊗ 𝑌 .

(5)

These properties allow Pauli strings to be propagated and multiplied without explicitly constructing their matrix representations. In particular, for a quantum gate 𝑈 , Pauli propagation can be formulated through the conjugation of an operator, 𝐴 ↦→ 𝑈 𝐴𝑈 † . For Clifford gates, conjugation maps every Pauli string to a single Pauli string up to a phase. For example, 𝐻𝑋 𝐻 = 𝑍,

𝐻𝑍𝐻 = 𝑋,

𝐻𝑌 𝐻 = −𝑌 ,

𝑆𝑋𝑆 † = 𝑌 ,

𝑆𝑌 𝑆 † = −𝑋,

𝑆𝑍𝑆 † = 𝑍 .

(6)

Consequently, Clifford gates do not introduce additional Pauli terms during propagation. This property allows a Pauli operator to be represented by a single Pauli string throughout a Clifford circuit. A single Pauli string can branch into multiple terms during propagation. General quantum circuits therefore require a weighted Pauli representation. By maintaining these weighted Pauli representations sparsely, Pauli propagation can avoid explicit statevector or unitary-matrix construction while preserving the operator-level semantics of the circuit. This combination of Pauli algebra, Clifford conjugation, and sparse term management provides the basis for Pauli-based quantum circuit analysis and equivalence checking. , Vol. 1, No. 1, Article . Publication date: November 2026.

Structure-Aware Quantum Circuit Equivalence Checking via Sparse Pauli Propagation

Quantum Circuits

Preprocessing

5

Equivalence Checking

Semantic Lowering

Pauli Propagation

Pauli Generators

{𝑅𝑧 𝜃 , 𝑋, 𝑋, 𝐶𝑋}

𝐶𝑈𝐶 † = ෍ 𝛼𝑃 (𝐶𝑃𝐶 † )

{𝑍0 , 𝑍1 … 𝑍𝑛 , 𝑋0 , 𝑋1 … 𝑋𝑛 }

𝑃

Pauli Plans • Information Extraction • Clifford Consolidation

𝑐∨𝑛

Circuit Cut Point

Miter Construction

𝑈1 = 𝐴1 𝐵1 ∥ 𝑈2 = 𝐴2 𝐵2

• 𝐿 = 𝐴†2 → 𝐼 ← 𝐴1 • 𝑅 = [𝐵2 → 𝐼 ← 𝐵1† ]

Result Certification

EQ/NEQ /UND

Fig. 1. The overall workflow of quantum circuit equivalence checking in our framework.

3

Methodology

Figure 1 illustrates the overall workflow of our framework, which consists of two major modules: (1) √ the Preprocessing module first lowers the input quantum circuit to the basis gate set {𝑅𝑧 , √𝑋, 𝑋, 𝐶𝑋 }. Under this representation, all non-Clifford effects are captured by 𝑅𝑧 rotations, while { 𝑋, 𝑋, 𝐶𝑋 } are Clifford gates. This normalization simplifies the subsequent Pauli-string expansion by restricting the non-Clifford operations that need to be handled explicitly. The module then extracts structural information from the normalized circuit and consolidates consecutive Clifford gates into Clifford blocks. Non-Clifford 𝑅𝑧 operations are kept as individual operations. The resulting representation consists of Clifford blocks and individual non-Clifford operations, thereby exposing the circuit structure for subsequent analysis. (2) the Equivalence Checking module selects different checking strategies based on the number of qubits and the non-Clifford ratio of the input circuits. For circuits with a low non-Clifford ratio or a large number of qubits, we employ the Pauli-generator evolution strategy (Section 3.1). A low non-Clifford ratio ensures that the evolution of each Pauli generator remains efficient, while for large circuits, non-equivalence can be efficiently detected by evolving the finite set of 2𝑛 Pauli generators. For other cases, we employ the cut-miter strategy (Section 3.2). The circuits are partitioned into multiple segments, and a miter is constructed at each cut point to analyze the weight of the non-identity Pauli components and determine equivalence. To account for numerical errors and the effects of pruning, the results produced by these strategies are further processed by the Result Certification module (Section 3.3). The certification procedure validates the checking result and ultimately returns the equivalence verdict. 3.1

Generator-Based Verification in the Heisenberg Picture

Our first backend compares the conjugation actions of the two circuits on Pauli generators. This representation is insensitive to global phase and avoids constructing dense unitary matrices or state vectors. Let G𝑛 = {𝑍 1, . . . , 𝑍𝑛 , 𝑋 1, . . . , 𝑋𝑛 } be the canonical generating set of the 𝑛-qubit Pauli group up to phase. We use the following standard characterization, which has also been applied to Clifford-circuit equivalence checking by Thanos et al. [30]. Theorem 3.1 (Generator criterion). For arbitrary 𝑛-qubit unitaries 𝑈 1 and 𝑈 2 , 𝑈1 ≡ 𝑈2

⇐⇒

𝑈 1𝐺𝑈 1† = 𝑈 2𝐺𝑈 2†

for every 𝐺 ∈ G𝑛 .

(7)

Proof sketch. A global phase cancels under conjugation, proving the forward direction. Conversely, every Pauli operator is, up to phase, a product of elements of G𝑛 . Agreement on the ⊗𝑛 generators therefore implies 𝑈 1 𝑃𝑈 1† = 𝑈 2 𝑃𝑈 2† for every Í 𝑃 ∈ P𝑛 , where P𝑛 = {𝐼, 𝑋, 𝑌 , 𝑍 } . Since every density operator admits a Pauli expansion 𝜌 = 𝑃 ∈ P𝑛 𝛼 𝑃 𝑃, linearity gives , Vol. 1, No. 1, Article . Publication date: November 2026.

6

Shangzhou Xia, Junjie Luo, Qichen Wang, Yasunari Suzuki and Jianjun Zhao

𝑈 1 𝜌𝑈 1† =

∑︁

𝛼 𝑃 𝑈 1 𝑃𝑈 1† =

𝑃

∑︁

𝛼 𝑃 𝑈 2 𝑃𝑈 2† = 𝑈 2 𝜌𝑈 2† .

(8)

𝑃

For any density operator 𝜌, 𝑈 1 and 𝑈 2 satisfy the above equation, demonstrating 𝑈 1 ≡ 𝑈 2 .

□

The characterization holds for any complete generating set of the Pauli group up to phase. We choose G𝑛 because it is a minimal set of 2𝑛 local operators. Consequently, equivalence over all quantum inputs is reduced to 2𝑛 operator comparisons, and any generator on which Eq. (7) fails provides an operator-level witness of inequivalence. Sparse propagation. For each 𝐺 ∈ G𝑛 , the backend independently propagates 𝐺 through each of the two input circuits, yielding the two Heisenberg images ∑︁ H𝑖 (𝐺) = 𝑈𝑖 𝐺𝑈𝑖† = 𝛼𝑖,𝐺,𝑃 𝑃, 𝑖 ∈ {1, 2}. (9) 𝑃 ∈ P𝑛

Each Heisenberg image is maintained as a sparse Pauli representation. Terms producing the same Pauli string are merged by summing their coefficients. For a Clifford gate 𝐶, conjugation maps each Pauli string to a single Pauli string up to a sign: 𝐶𝑃𝐶 † = 𝑠𝑃 ′,

𝑃, 𝑃 ′ ∈ P𝑛 ,

𝑠 ∈ {−1, +1}.

(10)

Consequently, Clifford gates preserve the number of Pauli terms and introduce no branching. We exploit this property by grouping maximal consecutive Clifford sequences into single propagation units, which are applied using precomputed conjugation tables. For each non-Clifford gate, we decompose it into a semantically equivalent composition of 𝑅𝑧 (𝜃 ) rotations and Clifford gates. After this transformation, the only non-Clifford operations are 𝑅𝑧 (𝜃 ) rotations with angles that are not integer multiples of 𝜋/2. Its local conjugation action is 𝑅𝑧 (𝜃 )𝐼𝑅𝑧 (𝜃 ) † = 𝐼,

𝑅𝑧 (𝜃 )𝑍𝑅𝑧 (𝜃 ) † = 𝑍,

𝑅𝑧 (𝜃 )𝑋 𝑅𝑧 (𝜃 ) † = cos(𝜃 )𝑋 + sin(𝜃 )𝑌 ,

𝑅𝑧 (𝜃 )𝑌 𝑅𝑧 (𝜃 ) † = cos(𝜃 )𝑌 − sin(𝜃 )𝑋 .

(11)

Hence, an 𝑅𝑧 gate branches only active terms containing 𝑋 or 𝑌 on its target qubit; terms containing 𝐼 or 𝑍 remain unchanged. Identical terms created by different branches are subsequently merged. The generator backend therefore propagates Pauli operators through the conjugation action of non-Clifford gates, rather than explicitly representing or expanding the gate operators. Comparison and scheduling. After propagating 𝐺 through both circuits, we quantify the discrepancy between H1 (𝐺) and H2 (𝐺) using the ℓ2 distance between their coefficient vectors.
𝑟𝐺 = 𝜶 1,𝐺 − 𝜶 2,𝐺 2 , 𝜶 𝑖,𝐺 = 𝛼𝑖,𝐺,𝑃 𝑃 ∈ P𝑛 , 𝑖 ∈ {1, 2}. (12) In exact arithmetic, 𝑟𝐺 = 0 if and only if H1 (𝐺) = H2 (𝐺). Hence, a nonzero residual for any generator is sufficient to witness non-equivalence, while equivalence is established only when all 2𝑛 generator images coincide. Propagation attempts process one or more generators through one circuit under term and time limits. The time limit for an attempt is a fixed fraction of the remaining overall time. If an attempt involving multiple generators exceeds either limit, propagation is retried for individual generators. A generator whose propagation remains incomplete after retries is skipped, leaving time to check other generators. Completed comparisons are evaluated using the certification conditions in Section 3.3. If no verdict is established after these attempts or the overall time limit is reached, the checker returns Undecided. , Vol. 1, No. 1, Article . Publication date: November 2026.

Structure-Aware Quantum Circuit Equivalence Checking via Sparse Pauli Propagation

3.2

7

Miter-Based Verification in the Pauli Representation

The generator backend propagates the two circuits independently and compares their Heisenberg images only after propagation. However, it cannot directly exploit cancellations between corresponding regions of the two circuits. Our second verification backend instead compares the circuits through their composite miter 𝑀 = 𝑈 2†𝑈 1 . By the definition of equivalence up to global phase, 𝑈1 ≡ 𝑈2

∃, 𝜙 ∈ R, 𝑀 = 𝑒 𝑖𝜙 𝐼 .

⇐⇒

(13)

Rather than constructing the 2𝑛 ×2𝑛 unitary matrix 𝑀 explicitly, we characterize the miter condition through its Pauli representation. We expand the miter in the Pauli basis P𝑛 = {𝐼, 𝑋, 𝑌 , 𝑍 } ⊗𝑛 as ∑︁ ∑︁ ∑︁ ∑︁ 1 𝑀 = 𝑈 2†𝑈 1 = ( 𝛼 𝑅 𝑅) ( 𝛼𝑄′ 𝑄) = 𝛼 𝑅 𝛼𝑄′ 𝑅𝑄 = 𝛽𝑃 𝑃, 𝛽𝑃 = 𝑛 Tr(𝑃 † 𝑀). (14) 2 𝑅∈ P 𝑄∈P 𝑅,𝑄 ∈ P 𝑃∈P 𝑛

𝑛

𝑛

𝑛

Specifically, we represent each quantum gate in 𝑈 1 and 𝑈 2† as a linear combination of Pauli strings and construct 𝑀 by performing Pauli-representation multiplication gate by gate. After each multiplication, terms corresponding to the same Pauli string are merged by summing their coefficients, thereby avoiding the explicit construction of its unitary matrix. At this point, the equivalencechecking problem is reduced to checking whether all non-identity Pauli coefficients in the Pauli expansion of 𝑀 are zero. However, this approach cannot guarantee sparsity throughout the computation. When represented in terms of Pauli strings, a quantum gate may contain multiple Pauli terms rather than a single term, causing the number of intermediate terms to grow exponentially. Prior work [6] uses an alternating miter construction to accelerate equivalence checking of quantum circuits. Following this approach, we incrementally construct the miter from the output boundaries of both circuits, forming a structure of the form 𝐺 → 𝐼 ← 𝐺 ′ . By applying gates from the two circuits from opposite sides, inverse operations corresponding to aligned regions can be brought together and canceled early. This cancellation can keep the intermediate Pauli sum small and reduce the number of terms processed by subsequent updates. Cut-Miter Pauli Comparison. However, this alternating construction is most effective when the two circuits remain locally aligned throughout the construction. If the circuits differ substantially around an internal region, the partial miter may grow before the construction reaches equivalent regions on the other side of the difference. To mitigate this limitation, we introduce an internal cut that decomposes each circuit into a prefix and a suffix, and construct two partial products from the two sides of the cut: 𝑈 1 = 𝐴1 𝐵 1 and 𝑈 2 = 𝐴2 𝐵 2 , where 𝐵𝑖 is the prefix before the cut and 𝐴𝑖 is the suffix after it. Rearranging the equivalence condition gives 𝑈 1 = 𝑒 𝑖𝜙 𝑈 2

⇐⇒

𝐴†2 𝐴1 = 𝑒 𝑖𝜙 𝐵 2 𝐵 1† .

(15)

Accordingly, the backend constructs the following structure in the form of a miter: ∑︁ ∑︁ 𝐿 = [𝐴†2 → 𝐼 ← 𝐴1 ] = 𝛽𝐿,𝑃 𝑃, 𝑅 = [𝐵 2 → 𝐼 ← 𝐵 1† ] = 𝛽𝑅,𝑃 𝑃, 𝑃 ∈ P𝑛

(16)

𝑃 ∈ P𝑛

using the alternating procedure described above. Cancellation between corresponding suffixes and prefixes can reduce the intermediate Pauli support of 𝐿 and 𝑅, respectively. Let ℓ = (𝛽𝐿,𝑃 )𝑃 ∈ P𝑛 and 𝒓 = (𝛽𝑅,𝑃 )𝑃 ∈ P𝑛 be the coefficient vectors of 𝐿 and 𝑅. Pauli orthogonality gives Tr(𝑃 †𝑄) = 2𝑛 𝛿𝑃,𝑄 . Since both products are unitary, their coefficient vectors have unit norm: ∥ℓ ∥ 22 =

Tr(𝐿 † 𝐿) = 1, 2𝑛

∥𝒓 ∥ 22 =

Tr(𝑅 †𝑅) = 1. 2𝑛

(17)

, Vol. 1, No. 1, Article . Publication date: November 2026.

8

Shangzhou Xia, Junjie Luo, Qichen Wang, Yasunari Suzuki and Jianjun Zhao

For 𝐿 = 𝐴†2 𝐴1 and 𝑅 = 𝐵 2 𝐵 1† , orthogonality and the cyclicity of the trace give † †

⟨𝒓, ℓ⟩ =

∑︁

𝛽𝑅,𝑃 𝛽𝐿,𝑃 =

𝑃 ∈ P𝑛

Tr(𝑅 † 𝐿) Tr(𝐵 1 𝐵 2 𝐴2 𝐴1 ) Tr(𝑀) = = . 2𝑛 2𝑛 2𝑛

(18)

The inner product is thus independent of the cut position. To account for global phase, we choose  ⟨𝒓, ℓ⟩    , |⟨𝒓, ℓ⟩| > 0, 𝜆 = |⟨𝒓, ℓ⟩|   otherwise.  1, This phase minimizes the coefficient distance, which satisfies 𝑑 = ∥ℓ − 𝜆𝒓 ∥ 2, Í

| 2 = 1 and 𝛽

For unitary 𝑀, 𝑃 |𝛽𝑃 non-identity coefficients:

𝑑 2 = 2 − 2|⟨𝒓, ℓ⟩|.

(19)

(20)

𝑛 𝐼 = Tr(𝑀)/2 . We define the residual as the ℓ2 norm of its

! 1/2 𝑟𝑀 =

∑︁

|𝛽𝑃 |

2

√︁ √︁ = 1 − |⟨𝒓, ℓ⟩| 2 = 𝑑 1 − 𝑑 2 /4.

(21)

𝑃 ≠𝐼

In exact arithmetic, 𝑟 𝑀 = 0 is equivalent to 𝑈 1 ≡ 𝑈 2 . The cost of constructing 𝐿 and 𝑅 can vary with the cut position, so the backend searches over several candidates. Candidate cuts are selected based on the cumulative number of non-Clifford rotations rather than the raw gate count, as non-Clifford rotations are the primary source of Pauli-support growth. The backend first evaluates a balanced cut and then considers asymmetric alternatives. Candidate cuts are initially screened under a small probe budget, and the most promising candidates are subsequently re-evaluated under the full budget. A probe contributes to the final verdict only when the complete coefficient-vector comparison is successfully completed. If a probe exceeds its resource budget before the comparison is completed, it is treated as inconclusive. 3.3

Complexity and Certified Results

Complexity. The resulting operators are propagated in the Pauli basis as sparse Pauli sums. The dominant cost of this propagation comes from the growth of the number of Pauli strings. In particular, a Clifford operation maps each Pauli string to a single Pauli string and therefore does not increase the representation size, whereas a non-Clifford rotation can split one Pauli string into two. Consequently, if a circuit contains 𝑡𝑖 non-Clifford rotations, independently propagating the circuit may generate up to 2𝑡𝑖 Pauli strings. Let quantum circuits 𝐶 1 and 𝐶 2 contain 𝑚 and 𝑚 ′ gates, respectively. As a baseline, independently propagating the two circuits requires 𝑂 (𝑚2𝑡1 + 𝑚 ′ 2𝑡2 ) string operations, where 𝑡𝑖 is the total number of non-Clifford rotations in 𝐶𝑖 . Thus, the baseline cost depends on the global non-Clifford complexity of the circuits. The cut-miter backend exploits structural similarity between the two circuits to avoid this global expansion. Let |𝐷 | be the number of differing rotations and 𝑡𝑐 be the maximum number of common non-Clifford rotations encountered by any partial miter. A differing rotation can introduce at most one additional branching factor of two, while common Clifford operations do not increase the number of Pauli strings. Therefore, by the size bound, each partial miter contains at most 2 |𝐷 |+𝑡𝑐 Pauli strings, yielding a total construction cost of 𝑂 ((𝑚 + 𝑚 ′ )2 |𝐷 |+𝑡𝑐 ). The key point is that non-Clifford rotations outside the difference region do not contribute to the exponential growth of the partial miter. Hence, when the circuits differ only in a small and localized region, (|𝐷 | + 𝑡𝑐 ) can be substantially smaller than the global non-Clifford count, reducing the number of Pauli strings that must be maintained. , Vol. 1, No. 1, Article . Publication date: November 2026.

Structure-Aware Quantum Circuit Equivalence Checking via Sparse Pauli Propagation

9

The generator-based backend exploits locality within each circuit rather than similarity between the two circuits. For a generator 𝐺, let 𝑡𝑖 (𝐺) denote the number of non-Clifford rotations in its light cone in circuit 𝐶𝑖 . Rotations outside this light cone cannot affect the propagation of 𝐺, so propagating 𝐺 requires at most 2𝑡𝑖 (𝐺 ) Pauli strings. Thus, the cost for one generator is 𝑂 (𝑚2𝑡1 (𝐺 ) + 𝑚 ′ 2𝑡2 (𝐺 ) ), Í and the total cost over the 2n generators is 𝑂 ( 𝐺 (𝑚2𝑡1 (𝐺 ) + 𝑚 ′ 2𝑡2 (𝐺 ) )). Although this backend propagates multiple generators, each propagation depends only on the non-Clifford rotations in the corresponding light cone. It can therefore be substantially cheaper than global propagation when these light cones are sufficiently small. Overall, the two backends exploit different sources of locality: the cut-miter backend exploits similarity between the input circuits, while the generator-based backend exploits locality of individual generators. Neither backend is asymptotically superior for all circuits; their benefits arise when the corresponding local complexity is substantially smaller than the global non-Clifford complexity. Certified Results. The underlying equivalence criterion is exact: two circuits are equivalent if and only if their miter residual is zero. In practice, however, Pauli-term pruning and semantic lowering introduce bounded approximation errors that must be accounted for when making numerical decisions. We therefore use a tolerance 𝜖 for decision making while explicitly tracking the error bounds introduced by these approximations. Let 𝐿 denote the accumulated ℓ2 -norm of the coefficients removed by pruning from both compared representations, and let 𝑠 be the combined operator-norm error bound introduced by snapping near-Clifford 𝑅𝑧 rotations in both circuits. We use 𝑏 = 𝐿 + 𝑠 for cut-miter comparison and 𝑏 = 𝐿 + 2𝑠 for generator comparison, since snapping changes both 𝑈 and 𝑈 † in 𝑈 𝐺𝑈 † . In exact arithmetic, a residual 𝑞 computed from the approximate representation satisfies 𝑞 − 𝑏 ≤ 𝑞 exact ≤ 𝑞 + 𝑏. √︁ For the cut comparison, the corresponding miter residual is 𝑟 𝑀 = 𝑑 1 − 𝑑 2 /4. Therefore, if 𝑟 𝑀 +𝑏 ≤ 𝜖, the checker can certify the circuits as Eqivalent. Conversely, if 𝑟 𝑀 −𝑏 > 𝜖, the checker can certify them as Not-Eqivalent. Otherwise, the comparison cannot establish a definitive result under the current error bound. For the generator comparison, let 𝑟𝐺 denote the discrepancy between the propagated images of a Pauli generator 𝐺 in the two circuits. Although the generator backend does not explicitly construct the miter, its certification can be related to the miter residual 𝑟 𝑀 . In exact arithmetic, the discrepancy of each generator satisfies 𝑟𝐺exact ≤ 2𝑟 𝑀 . Thus, a sufficiently large discrepancy for any single generator is sufficient to establish non-equivalence. In particular, if 𝑟𝐺 − 𝑏 > 2𝜖, then 𝑟𝐺exact > 2𝜖, which implies 𝑟 𝑀 > 𝜖. The checker can therefore certify the circuits as Not-Eqivalent. In contrast, certifying equivalence requires a global upper bound on the miter residual, rather than evidence from a single generator. For the complete set of their discrepancies √︃2𝑛 Pauli generators,
Í 2 exact . Taking the approximation collectively provide such an upper bound, since 2𝑟 𝑀 ≤ 𝐺 𝑟𝐺 Í 2 error into account, each exact discrepancy is bounded by 𝑟𝐺 + 𝑏. We therefore use 𝑆 = √ 𝐺 (𝑟𝐺 + 𝑏) as √a conservative upper bound on the squared discrepancies. It follows that 2𝑟 𝑀 ≤ 𝑆. Hence, if 2𝑆 ≤ 𝜖, then 𝑟 𝑀 ≤ 𝜖, and the checker can certify the circuits as Eqivalent. This certificate requires all 2n generators to complete, because the bound relies on their collective discrepancies. 3.4

Algorithm

This section describes how our framework selects an equivalence-checking strategy according to the structural characteristics of the target quantum circuits. Algorithm 1 presents the overall workflow of the proposed structure-aware equivalence-checking approach. Given two quantum circuits 𝐶 1 and 𝐶 2 and a residual tolerance 𝜖, the checker first verifies that the two circuits act on the same number of qubits (lines 1-3). It then performs semantic lowering and , Vol. 1, No. 1, Article . Publication date: November 2026.

10

Shangzhou Xia, Junjie Luo, Qichen Wang, Yasunari Suzuki and Jianjun Zhao

Algorithm 1 : Structure-Aware Quantum Circuit Equivalence Checking Input: Quantum circuits 𝐶 1 , 𝐶 2 and residual tolerance 𝜖 Output: Eqivalent, Not-Eqivalent, or Undecided (Timeout ⇒ Undecided) 1: if 𝐶 1 and 𝐶 2 have different numbers of qubits then 2: return Not-Eqivalent 3: end if 4: Π 1 , Π 2 ← PauliPlans(Lowering(𝐶 1 , 𝐶 2 ), 𝜏𝑠𝑛𝑎𝑝 ) 5: 𝑐 ← max{Π1 .non_clifford, Π 2 .non_clifford} 6: 𝑠 ← Π 1 .snap_err + Π 2 .snap_err 7: if 𝑐 ≥ 𝑐𝑡ℎ𝑟𝑒𝑠ℎ𝑜𝑙𝑑 and 𝑛 ≤ 𝑛𝑡ℎ𝑟𝑒𝑠ℎ𝑜𝑙𝑑 then 8: for all scheduled cut attempts at fractions 𝑓 ∈ 𝐹 cut do 9: 𝐴𝑖 , 𝐵𝑖 ← CutPoint( 𝑓 , Π𝑖 ) for 𝑖 = 1, 2 10: (ℓ, 𝐿ℓ ), (𝒓, 𝐿𝒓 ) ← PauliSum(𝐴†2 𝐴1 , 𝜏𝑝𝑟𝑢𝑛𝑒 ), PauliSum(𝐵 2 𝐵 1† , 𝜏𝑝𝑟𝑢𝑛𝑒 ) 11: if BudgetExceeded then 12: continue 13: end if 14: 𝑏 ← 𝐿ℓ + 𝐿 𝒓 + 𝑠 √︁ 15: 𝜆 ← ⟨𝒓, ℓ ⟩ / | ⟨𝒓, ℓ ⟩ |; 𝑑 ← ∥ℓ − 𝜆𝒓 ∥ 2 ; 𝑟 ← 𝑑 1 − 𝑑 2 /4 16: return Eqivalent if 𝑟 + 𝑏 ≤ 𝜖; Not-Eqivalent if 𝑟 − 𝑏 > 𝜖 17: end for 18: end if 19: 𝑖𝑛𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 ← false; 𝑆 ← 0 20: for all 𝐺 ∈ {𝑍 1 , . . . , 𝑍𝑛 , 𝑋 1 , . . . , 𝑋𝑛 } do 21: 𝜶 1 , 𝜶 2 , 𝐿1 , 𝐿2 ← SparsePropagation(𝐺, Π1 , Π 2 , 𝜏𝑝𝑟𝑢𝑛𝑒 ) 22: if BudgetExceeded then 23: 𝑖𝑛𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 ← true 24: continue 25: end if 26: 𝑏 ← 𝐿1 + 𝐿2 + 2𝑠 27: if ∥𝜶 1 − 𝜶 2 ∥ 2 − 𝑏 > 2𝜖 then 28: return Not-Eqivalent 29: end if 30: 𝑆 ← 𝑆 + ( ∥𝜶 1 − 𝜶 2 ∥ 2 + 𝑏 ) 2 31: end for √ 32: return Undecided if 𝑖𝑛𝑐𝑜𝑚𝑝𝑙𝑒𝑡𝑒 or 𝑆/2 > 𝜖 else Eqivalent

constructs the corresponding Pauli propagation plans Π 1 and Π 2 (line 4). The maximum proportion of non-Clifford operations in the two plans is used as the structural indicator 𝑐 (line 5), while the accumulated operator-norm error 𝑠 introduced by snapping is also obtained (line 6). When the circuits contain a sufficiently large proportion of non-Clifford operations and the number of qubits is within the predefined threshold (line 7), the checker first invokes the cut-based backend. It evaluates a set of candidate cut positions, with the balanced cut considered first and asymmetric cuts subsequently examined (line 8). For each candidate cut, the circuits are decomposed into prefix and suffix parts (line 9), and the two corresponding Pauli-sum representations are constructed. During Pauli-sum construction, we prune coefficients whose magnitudes are below 𝜏𝑝𝑟𝑢𝑛𝑒 and return the accumulated error introduced by the pruning process (line 10). If the construction exceeds the string budget, the current cut is skipped, and the next candidate is considered (line 11-13). Otherwise, the accumulated approximation error is bounded by 𝑏 = 𝐿 + 𝑠 (line 14), where 𝐿 denotes the pruning error and 𝑠 denotes the semantic-lowering error. The coefficient vectors ℓ and 𝒓 are aligned up to a global phase 𝜆, and their√︁cut distance 𝑑 is computed. This distance is converted into the corresponding miter residual 𝑟 = 𝑑 1 − 𝑑 2 /4 (line 15). Accounting for the approximation bound 𝑏, the checker immediately certifies the circuits as Eqivalent when 𝑟 + 𝑏 ≤ 𝜖, or as , Vol. 1, No. 1, Article . Publication date: November 2026.

Structure-Aware Quantum Circuit Equivalence Checking via Sparse Pauli Propagation

11

Not-Eqivalent when 𝑟 −𝑏 > 𝜖 (line 16). If neither condition holds, the current cut is inconclusive, and the checker proceeds to the next candidate. If the cut-based backend is not applicable or cannot establish a definitive result, the checker falls back to the generator-based backend. It propagates each of the 2𝑛 Pauli generators through both circuits and obtains the corresponding coefficient vectors 𝜶 1 , 𝜶 2 and pruning error 𝐿 (line 21). If propagation for a generator exceeds the string budget, the checker marks the analysis as incomplete and continues with the remaining generators (line 22-25). For every successfully propagated generator, the discrepancy 𝑟𝐺 = |𝜶 1 − 𝜶 2 | 2 is computed. If 𝑟𝐺 − 𝑏 > 2𝜖, the generator provides a sufficient witness for non-equivalence (line 27), and the checker immediately returns Not-Eqivalent (line 28). Otherwise, the conservative upper bound (𝑟𝐺 + 𝑏) 2 is accumulated into 𝑆 (line 30). After all generators have been processed, the checker can certify equivalence√only when every generator has been successfully analyzed and the resulting global bound satisfies 𝑆/2 ≤ 𝜖. If some generators were incomplete or this condition is not satisfied, the checker returns Undecided (line 32). Thus, the algorithm exploits an asymmetric certification principle: a single sufficiently large generator discrepancy is sufficient to certify non-equivalence, whereas equivalence requires complete coverage of all generators and a sufficiently small aggregate discrepancy. Implementation. We use 𝜖 = 10−10 as the default residual tolerance. Pauli coefficients with magnitude at most 𝜏prune = 10−14 are removed after merging duplicate terms. This threshold eliminates floating-point cancellation residue while remaining well below 𝜖. During Pauli-plan construction, an 𝑅𝑧 rotation within 𝜏snap = 10−12 of a Clifford angle is snapped to that angle. The actual perturbation introduced by these snaps is accumulated as 𝑠. All verdicts use the certified error band 𝑏. The cut backend is enabled when the larger plan contains at least 𝑐 threshold = 16 non-Clifford rotations and the circuits have at most 𝑛 threshold = 32 qubits. The former is an empirical routing threshold that avoids cut-search overhead on rotation-sparse circuits. The latter follows from the current implementation, which stores the 𝑋 and 𝑍 masks of a Pauli string in one 64-bit word. We try the cut fractions 𝐹 cut = (0.50, 0.35, 0.65, 0.25, 0.75, 0), where 0 represents the input-end one-sided construction, 0.5 is the balanced cut, and the remaining fractions cover asymmetric alignments. If the cut backend cannot certify a verdict within its resource budget, the algorithm falls back to generator propagation. 4

Experimental Evaluation

Our framework is implemented in Python using Qiskit 2.5.1 [15]. We address the following research questions: • RQ1: Effectiveness and Efficiency. How effectively and efficiently does our framework check quantum circuit equivalence compared with existing approaches? • RQ2: Component Effectiveness. How does each component contribute to the overall performance of our approach? • RQ3: Pruning Sensitivity. How sensitive is our approach to the pruning threshold 𝜏prune ? In RQ1, we compare our framework with QCEC, Quokka#, and QuPRS on two benchmark suites. We evaluate their correctness, decision coverage, and runtime under the same timeout limit. In RQ2, we conduct an ablation study of individual components of our framework. We evaluate configurations without cut-miter checking, with only the input-end cut, with the input-end cut evaluated first, without per-attempt time limits, and without Pauli-term pruning. We compare their decision coverage, runtime, and memory consumption with those of the complete configuration. In RQ3, we evaluate our framework with 𝜏prune ∈ {10−14, 10−13, 10−12 }. We study how the threshold affects decision coverage and runtime. , Vol. 1, No. 1, Article . Publication date: November 2026.

12

Shangzhou Xia, Junjie Luo, Qichen Wang, Yasunari Suzuki and Jianjun Zhao

Baselines. MQT QCEC [7] combines decision-diagram-based construction, alternating checking, simulation, and ZX-calculus rewriting. Quokka# [20] reduces Pauli-generator equivalence obligations to weighted model counting. The Quokka# baseline represents the WMC-based equivalence-checking implementation provided by the Quokka# framework, which builds on the line of work introduced by ECMC [19]. QuPRS [14] combines path-sum reduction with a weighted-model-counting fallback. We use QCEC 3.8.0, Quokka# 2.7.5 on Union and the artifact-provided version 2.7.3 on Artifact, and QuPRS 0.13.0 in hybrid mode. QCEC uses its default configuration on Union, while its ZX checker is disabled on Artifact to match the original artifact’s experimental settings [20]. Benchmarks. Our primary benchmark Union contains 350 circuit pairs derived from 70 base circuits. The base circuits cover 14 MQT Bench families, including GHZ, Deutsch–Jozsa, graph-state, W-state, QFT, QPE, QAOA, VQE, amplitude-estimation, quantum-walk, Grover, and QNN circuits, together with random Clifford+𝑇 circuits. Circuit widths range from 4 to 512 qubits. For each base circuit 𝐶, we remove final measurements and obtain 𝐶 opt using Qiskit at optimization level 2, with the gate √ set {id, 𝑅𝑧 , 𝑋, 𝑋, CX} and seed 42. We compare 𝐶 with 𝐶 opt and four variants generated separately from 𝐶 opt by deleting one gate (del), swapping the control and target of one CX gate (flip), or increasing one 𝑅𝑧 angle by 10−4 (shift4) or 10−7 (shift7). This construction yields five pairs (1 equivalent circuit pair classified as EQ and 4 non-equivalent circuit pairs classified as NEQ) per base circuit, with mutation positions selected using a fixed seed for each circuit family and width. Before freezing the resulting QASM files for reuse across experiments, we normalize the final qubit order and translate both sides at optimization level 0. Our framework, QCEC, and QuPRS use the gate set above. Quokka# 2.7.5 uses {𝑅𝑥 , 𝑅𝑧 , 𝐻, CX} because it does not support sx and incorrectly encodes 𝑅 𝑦 rotations. The Artifact benchmark contains 88 circuit pairs distributed with the Quokka# artifact. These include the original optimization, gate-missing, and rotation-perturbation pairs, covering both algorithmic circuits and reversible arithmetic benchmarks. Experimental setup. All experiments were conducted on a machine running NixOS 25.11, equipped with a 14-core Intel Core i9-10940X CPU at 3.30 GHz, with 28 hardware threads and 204 GiB of RAM. We allow 300 seconds per circuit pair for all tools. Our framework uses an equivalence tolerance of 10−10 and a default pruning threshold of 10−14 . Generator propagation attempts are limited to 10% of the remaining time. The corresponding RQ2 variant removes the per-attempt limit while retaining the overall timeout. 4.1

RQ1: Effectiveness and Efficiency

Overall comparison. Our method returns reference-consistent results for 343 of 346 scored Union instances and 76 of 88 Artifact instances, with no incorrect results and the lowest aggregate runtime on both suites (Table 1). Our method and QCEC correctly classify 64 of 66 EQ instances on Union and all seven on Artifact. All additional correct results over QCEC are on NEQ instances. On Union, the 105 additional results resolve 42 misclassifications and 63 inconclusive cases. On Artifact EQ instances, QCEC takes 6.0 s compared with our 24.0 s. The four excluded Union instances are the eq variants of QFT-16, QPEexact-32, QPEinexact-32, and QPEinexact-64. Their reference labels assume that O2 optimization preserves equivalence, while Qiskit applies numerical tolerances even with approximation_degree=1.0 [35]. The resulting differences exceed our circuit tolerance, and both our method and Quokka# return NEQ on these pairs. Structural suitability. Table 2 illustrates how circuit structure affects cost. DJ-64 contains Clifford gates apart from the perturbed rotation, so generator conjugation produces at most two Pauli terms per generator despite its width. Partial-product comparison can also keep intermediate Pauli representations small when common circuit structure cancels. On VQE-2L-10 with shift7, the balanced cut establishes NEQ in 0.067 s, with a recorded peak of 4 112 Pauli terms, while all three , Vol. 1, No. 1, Article . Publication date: November 2026.

Structure-Aware Quantum Circuit Equivalence Checking via Sparse Pauli Propagation

13

Table 1. Comparison with existing equivalence checkers by reference label. Union (346 instances) Tool

Correct

Incorrect

Inconclusive

Artifact (88 instances) Time (s)

Correct

EQ (66 instances) Ours QCEC Quokka# QuPRS

64 64 49 52

0 0 0 0

2 2 17 14

279 174 188 108

0 42 49 108

1 64 43 64

Inconclusive

Time (s)

EQ (7 instances) 572.6 611.2 6 064.8 4 362.1

7 7 6 5

NEQ (280 instances) Ours QCEC Quokka# QuPRS

Incorrect

0 0 0 0

0 0 1 2

24.0 6.0 457.8 756.3

NEQ (81 instances) 1 987.6 8 468.1 15 478.2 19 405.1

69 36 55 10

0 21 4 33

12 24 22 38

5 183.1 7 550.9 7 366.6 11 224.9

Groups and correctness are based on reference labels. Inconclusive denotes no EQ or NEQ result within 300 seconds. Time is summed within each group.

Table 2. Representative instances illustrating complementary strengths. Instance DJ-64, shift7 (U) VQE-2L-10, shift7 (U) QWalk-8, shift4 (A) QPEexact-16, flip (U) QNN-16, eq (U)

Ours

QCEC

Quokka#

QuPRS

NEQ (0.036s) NEQ (0.067s) NEQ (24.118s) NEQ (180.930s) EQ (29.315s)

EQ† (0.194s)

EQ† (1.441s)

T/O T/O T/O EQ (0.048s)

T/O T/O NEQ (0.698s) EQ (0.461s)

EQ† (1.068s) T/O T/O NEQ (0.791s) EQ (3.686s)

U and A denote Union and Artifact. T/O denotes timeout; † marks an incorrect result.

baselines time out. On QWalk-8 with shift4, generator comparison establishes NEQ in 24.118 s using a residual of 1.768 × 10−5 . The baselines can be substantially faster on other circuit structures. QCEC uses decision-diagram methods and simulation. Quokka# encodes Pauli propagation as weighted Boolean constraints, and QuPRS simplifies path-sums before invoking model counting. A large Pauli expansion may still admit efficient reasoning in these representations. On QPEexact-16 with flip, our method requires generator retries and takes 180.930 s, whereas Quokka# and QuPRS both finish below one second. QCEC checks QNN-16 eq in 0.048 s, compared with our 29.315 s. Across the 238 Union instances, both QCEC and our method classify correctly; the median runtime ratio 𝑇QCEC /𝑇ours is 1.22. Numerical sensitivity. On the 70 Union shift7 instances, our method detects all 70, compared with 21 for QCEC, four for Quokka#, and zero for QuPRS. The DJ example illustrates how the comparison quantity affects detection. An affected generator has residual 2| sin(𝛿/2)| ≈ |𝛿 |, whereas Quokka#’s projected coefficient departs from one by 1 − cos 𝛿 ≈ 𝛿 2 /2. For 𝛿 = 10−7 , the latter is approximately 5 × 10−15 , below its configured numerical tolerance of 10−12 . The original ECMC evaluation also considered phase-shift perturbations of 10−4 and 10−7 , and also reports incorrect results for 10−7 cases. The evaluated QuPRS implementation also rounds the base-two logarithm of the WMC magnitude to three decimal places before its tolerance test [13], reducing the resolution of that comparison. Our method compares the computed residual with the circuit tolerance while , Vol. 1, No. 1, Article . Publication date: November 2026.

14

Shangzhou Xia, Junjie Luo, Qichen Wang, Yasunari Suzuki and Jianjun Zhao

Table 3. Ablation study on 350 Union instances. Configuration

Decided

Time (s)

Rel. time

Peak RSS (GiB)

347 344 345 318 347 347

2 643 4 739 3 232 14 884 2 999 3 070

1.00× 1.79× 1.22× 5.63× 1.13× 1.16×

12.25 43.14 32.03 109.21 12.41 12.41

Full method - Without cut stage - Without per-attempt time limits - Without pruning Input-end first Input-end miter

All variants retain generator verification. Input-end first retains all candidate cuts and evaluates 𝑓 = 0 first, while input-end miter uses only 𝑓 = 0. Decided counts EQ or NEQ results returned within 300 s. Time is summed within each group. Peak RSS is the process high-water mark, including execution beyond the deadline.

accounting for errors from pruning and semantic lowering. These results indicate that, for the small phase perturbations considered in our evaluation, residual-based comparison provides a higherresolution discriminative signal, while explicit error bounds allow our framework to retain this numerical sensitivity without overlooking the approximation errors introduced during computation. Answer to RQ1: Our framework correctly decides more instances than the evaluated stateof-the-art equivalence checkers on Union and Artifact, with the lowest aggregate runtime. No incorrect results are observed among the scored instances. 4.2

RQ2: Component Effectiveness

We compare the full method with five variants that separately remove partial-product comparison, restrict the candidate cuts, change their order, disable pruning, or remove per-attempt time limits for generator propagation (Table 3). All other settings remain fixed. Removing the cut stage leaves generator verification alone, loses three EQ results, and increases aggregate runtime by a factor of 1.79. Recorded peak RSS also rises from 12.25 to 43.14 GiB, a factor of 3.52. The input-end miter decides all three pairs and records a peak of 12.41 GiB. Joint construction at the input end therefore already provides the additional decisions and most of the observed memory reduction. Comparing circuit products permits cancellation between the circuits and can establish a result before separate generator expansions are required. The full method reduces aggregate runtime by 11.9% and 13.9% relative to input-end first and input-end miter, respectively, with the same 347 decisions. Internal cuts improve efficiency on this suite without increasing coverage beyond the input-end miter. Input-end first uses the same candidate cuts as the full method, so their order also affects the benefit obtained within the shared cut-stage budget. This benefit is concentrated: the Grover-8 gm, flip, and shift7 instances account for 108.0% of the net time reduction over input-end first. Trying an expensive boundary first can consume the cut-stage budget before an inexpensive comparison is completed. Disabling pruning reduces the number of decided instances from 347 to 318, increases aggregate runtime by a factor of 5.63, and raises recorded peak RSS from 12.25 to 109.21 GiB. Retained terms must be processed at later propagation steps, where non-Clifford rotations can expand them further. Pruning reduces the work and storage required by subsequent updates as well as the size of the current sum. Removing per-attempt time limits reduces the number of decided instances from 347 to 345 and increases aggregate runtime by 22.3%. Both additional decisions are NEQ, for which one generator comparison can suffice. Limiting expensive propagation attempts leaves time for other generators and can improve coverage without increasing the overall timeout. , Vol. 1, No. 1, Article . Publication date: November 2026.

Structure-Aware Quantum Circuit Equivalence Checking via Sparse Pauli Propagation

15

Table 4. Deciding stages of the full configuration on Union benchmark. Stage or outcome

Instances

Cut-miter checking Generator verification Undecided

200 147 3

Total

350

To further understand how the two verification backends contribute to the overall decision coverage, we analyze the 350 Union circuit pairs according to the backend that produces the final decision. This analysis distinguishes pairs decided directly by the cut-miter stage from those decided by generator verification, as well as pairs for which the cut stage is inconclusive. Table 4 reports 200 decisions made directly by cut-miter, 147 decisions made by generator verification, and three undecided pairs. Among the 147 generator-verification decisions, 115 are obtained without any cut attempt, while the remaining 32 follow inconclusive cut attempts. Thus, among the 235 circuit pairs subjected to the cut stage, 200 are decided directly by cut-miter, while the remaining 35 proceed to generator verification; 32 of these are subsequently decided, and three remain undecided. Overall, the two backends are complementary: cut-miter resolves 200 pairs directly, while generator verification resolves an additional 147 pairs. This distribution indicates that generator verification is not merely a fallback when cut-miter cannot reach a decision, but independently contributes a substantial portion of the final decisions. Further analysis by circuit family shows that the 235 pairs subjected to the cut stage include 100 QAOA, QFT, and VQE pairs, all of which are decided by cut-miter, but only 15 of the 35 QPE pairs are decided at this stage. Generator verification decides 17 of the remaining 20 QPE pairs, leaving three undecided. Thus, the current cut fractions are more effective for the tested QAOA, QFT, and VQE pairs than for QPE. Selecting cuts using circuit structure and estimates of intermediate Pauli-term growth may allow more pairs to be decided before generator propagation. Answer to RQ2: The ablation results show that the components of our framework contribute differently to coverage and efficiency. On the Union benchmark, the cut-miter and generator verification backends are complementary, resolving 200 and 147 pairs, respectively. Pruning has the largest impact: disabling it reduces coverage from 347 to 318 and increases runtime by 5.63×. Per-attempt time limits and cut ordering provide additional benefits, while internal cuts primarily improve runtime. 4.3

RQ3: Pruning Sensitivity

Pruning-threshold sensitivity. Our framework relies on numerical thresholds in its Pauli propagation and decision procedure. In particular, the pruning threshold 𝜏prune determines which Pauli coefficients are discarded after merging duplicate terms. A larger threshold discards more coefficients and can therefore increase the accumulated pruning error bound, which may in turn prevent a comparison from establishing EQ or NEQ. At the same time, a larger threshold can reduce the number of Pauli terms retained for subsequent propagation and thus lower the computational cost. We therefore evaluate the sensitivity of our framework to 𝜏prune by comparing three thresholds, 10−12 , 10−13 , and 10−14 , on both Union and Artifact. We keep the circuit-equivalence tolerance fixed and use the full configuration in all runs. We compare both decision outcomes and aggregate runtime to determine whether reducing the pruning threshold affects decision stability or provides additional coverage at a measurable computational cost. , Vol. 1, No. 1, Article . Publication date: November 2026.

16

Shangzhou Xia, Junjie Luo, Qichen Wang, Yasunari Suzuki and Jianjun Zhao

Table 5. Sensitivity to the pruning threshold. Union

Artifact

𝜀 prune

Decided

Time (s)

Decided

Time (s)

10−12

346/350 347/350 347/350

2 627 2 660 2 643

76/88 76/88 76/88

5 200 5 208 5 207

10−13 10−14 (default)

Outcome stability. Across the three threshold settings in Table 5, 437 of 438 instances retain the same output, with no EQ–NEQ switches. The only difference occurs for one instance that is inconclusive at 10−12 but is classified as EQ at both smaller thresholds. Thus, within the tested range, changing the pruning threshold has little effect on the final decision outcomes, and no instance switches directly between EQ and NEQ. Computational trade-off. Reducing the pruning threshold from 10−13 to 10−14 decreases aggregate runtime by 0.6% on Union and by less than 0.1% on Artifact in these runs, with no change in decision coverage. Combined with the much larger performance degradation observed when pruning is completely disabled in RQ2, these results indicate that pruning itself is important for controlling computational cost on these benchmarks, whereas the exact choice of pruning threshold has relatively little impact within the tested range. The default threshold of 10−14 therefore provides stable decision outcomes with similar computational cost to 10−13 . Overall, these results indicate that our framework is relatively insensitive to the pruning threshold within the tested range. Lowering the threshold does not materially change the decision outcomes or improve coverage, while the presence or absence of pruning has a much larger effect on computational performance. This observation supports the use of a small pruning threshold to maintain stable decisions while retaining the computational benefits of pruning. Answer to RQ3: Our framework achieves similar decision coverage and aggregate runtime on Union and Artifact across pruning thresholds from 10−14 to 10−12 . Reducing the threshold from 10−13 to 10−14 preserves the same coverage with similar runtime. 5

Threats to Validity

Internal validity. Implementation errors and finite-precision arithmetic may affect the results. We mitigate these risks through unit tests and numerical matrix comparisons with Qiskit on small circuits. Our framework also accounts for errors introduced by pruning and rotation-angle adjustments when making tolerance-based decisions. External validity. Our evaluation includes both generated circuit pairs and the original Quokka# artifact. These benchmarks cover different circuit families, sizes, and structures, but may not represent all practical quantum programs. In particular, our framework is primarily designed to exploit structural regularities commonly arising in compiler optimizations and circuit transformations. Its effectiveness may therefore be more limited for arbitrary circuit pairs with little structural correspondence. Mutation positions are fixed, and performance may vary with the mutation location or available resources. Construct validity. Our framework checks full unitary equivalence up to global phase and does not support mid-circuit measurements, classical control, or non-trivial initial layouts. Numerical approximations during transpilation may produce inaccurate reference labels. We check four such , Vol. 1, No. 1, Article . Publication date: November 2026.

Structure-Aware Quantum Circuit Equivalence Checking via Sparse Pauli Propagation

17

discrepancies using Quokka# and exclude them from all metrics in the RQ1 comparison. Since exact ground truth is unavailable for some large circuits, further labeling errors may remain. 6

Related Work

In this section, we review existing methods for quantum circuit equivalence checking and verification beyond unitary circuits. We then discuss Pauli-based simulation and verification methods and their relation to the operator propagation used in our framework. 6.1

Quantum Circuit Equivalence Checking

Quantum circuit equivalence checking has been studied using decision diagrams, the ZX-calculus, path sums, and weighted model counting. Burgholzer and Wille [5, 6] proposed a decision-diagrambased approach to quantum circuit equivalence checking, in which quantum circuit matrices are represented using decision diagrams. They further introduced a miter-based construction that interleaves operations from the two circuits, allowing common substructures to cancel early and thereby reducing the number of decision-diagram nodes. Peham et al. [26] proposed a ZXcalculus-based approach that represents quantum circuits as connected graphs and determines equivalence through graph simplification. They also pointed out that this approach does not guarantee completeness. These two approaches have since been integrated into MQT QCEC [7, 34] as complementary equivalence-checking techniques. Mei et al. [19] used the Pauli-generator characterization of unitary equivalence to reduce circuit comparison to weighted model counting (WMC). Huang et al. [14] combined path-sum reductions with WMC, applying model counting to the residual path-sum when simplification does not decide equivalence. Yu et al. [39] used local projections to check equivalence of shallow circuits, with complexity linear in qubit count for fixed depth but exponential in depth for one-dimensional nearest-neighbor circuits. Our framework extends the alternating miter construction used in decision-diagram-based checking with internal cuts, comparing two partial products directly instead of expanding the complete miter. This allows cancellation within both circuit prefixes and suffixes, which can reduce intermediate Pauli-term growth when corresponding regions are aligned. In contrast to WMC-based checking, it computes these products and generator images by direct sparse propagation. 6.2

Equivalence and Verification Beyond Unitary Circuits

Equivalence checking becomes more involved for quantum programs containing mid-circuit measurements, resets, discarded qubits, noise, or measurement-dependent classical control. Such programs are generally described by quantum channels or ensembles of branch operators rather than a single unitary transformation. Burgholzer and Wille [8] proposed transformations for handling non-unitary operations while retaining compatibility with existing unitary equivalence-checking techniques. Hong et al. [11] formalized the semantics of dynamic quantum circuits using ensembles of linear operators and developed tensor-decision-diagram-based algorithms for checking both measurement-output and quantum-output equivalence. For noisy circuits, Hong et al. [12] defined approximate equivalence using the Jamiolkowski fidelity between quantum channels and evaluated it through tensor-network contraction. More recently, Ricciardi et al. [28] combined deferred measurement with separation and projection techniques to extend unitary equivalence checking to a broader class of hybrid circuits, including circuits with discarded subsystems. Beyond circuit-level equivalence, formal verification methods reason about general behavioral properties of quantum programs. Ying et al. [38] modeled quantum programs using superoperators and quantum Markov chains and developed methods for verifying observable properties and termination. Barthe et al. [2] introduced a relational program logic based on quantum couplings, enabling properties relating two program executions to be formally proved. These studies handle non-unitary , Vol. 1, No. 1, Article . Publication date: November 2026.

18

Shangzhou Xia, Junjie Luo, Qichen Wang, Yasunari Suzuki and Jianjun Zhao

behavior or general program properties, while our framework focuses on the computational cost of full unitary equivalence checking up to global phase. 6.3

Pauli-Domain Circuit Verification

Pauli and stabilizer representations provide an efficient foundation for reasoning about quantum circuits with substantial Clifford structure. Gottesman [10] introduced a Heisenberg-picture description in which quantum computation is characterized through the evolution of Pauli operators. Aaronson and Gottesman [1] subsequently developed efficient tableau-based algorithms for stabilizer circuits. These algorithms exploit the fact that conjugation by a Clifford gate maps each Pauli string to a single Pauli string. Gidney developed Stim [9], an efficient stabilizer simulator based on tableau representations and Pauli-frame propagation. Extending stabilizer techniques beyond Clifford circuits generally requires representing the effect of non-Clifford operations using weighted combinations. Bravyi et al. [4] represented quantum states as low-rank sums of stabilizer states, enabling the simulation of circuits containing a moderate number of non-Clifford gates. Pashayan et al. [25] developed complementary algorithms for estimating output probabilities of circuits containing Clifford gates and arbitrary-angle Pauli-𝑍 rotations. In the operator domain, Rall et al. [27] formulated circuit simulation through Pauli propagation, where states or observables are evolved directly in the Pauli basis. More recent approaches propagate Heisenberg observables as sparse weighted sums of Pauli strings and use coefficient- or weight-based truncation to control term growth. Begušić and Chan [3] applied this approach to real-time operator evolution, while Rudolph et al. [29] systematized the underlying algorithms and provided the PauliPropagation.jl framework. For equivalence checking, Thanos et al. [30] compare the conjugation of the canonical Pauli generators 𝑋𝑖 and 𝑍𝑖 using Stim as the stabilizer-simulation backend. Their approach is efficient but restricted to Clifford circuits. Osama et al. [22] subsequently parallelized generator-based Clifford equivalence checking on GPUs. Our framework propagates weighted Pauli sums through nonClifford rotations, while the Clifford generator checkers propagate single Pauli strings. The sparse simulators above compute states or observables, whereas our framework compares a complete set of generator images to establish equivalence over all inputs. 7

Conclusion

We presented a structure-aware equivalence checker for unitary quantum circuits based on sparse Pauli propagation. By combining generator propagation with Cut-Miter comparison, our framework adapts its verification strategy to different circuit structures while using bounded resources and explicitly accounting for numerical and approximation errors. Our evaluation on two benchmark suites with circuits of up to 512 qubits shows that our framework provides correct, referenceconsistent decisions for 96.3% of 434 scored circuit pairs without incorrect verdicts, compared with at most 68.7% for the evaluated baselines. It also achieves the lowest aggregate runtime, reducing total runtime by 48.5%–76.0%. The ablation results further demonstrate that cut-based comparison and Pauli-term pruning are important for maintaining decision coverage and computational efficiency, while bounded propagation attempts improve the use of the available verification budget. Overall, our results show that exploiting complementary forms of sparsity provides a practical way to make Pauli-based equivalence checking more scalable and robust across diverse quantum circuit structures. Our framework therefore offers a useful verification oracle for quantum software testing and compiler validation. These results also suggest several directions for future work, including structure-adaptive cut-point selection, support for circuits with mid-circuit measurements and classical control, and hybrid verification approaches that combine our framework with SATbased reasoning and weighted model counting. , Vol. 1, No. 1, Article . Publication date: November 2026.

Structure-Aware Quantum Circuit Equivalence Checking via Sparse Pauli Propagation

19

References [1] Scott Aaronson and Daniel Gottesman. 2004. Improved simulation of stabilizer circuits. Phys. Rev. A 70 (Nov 2004), 052328. Issue 5. doi:10.1103/PhysRevA.70.052328 [2] Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. 2019. Relational proofs for quantum programs. Proc. ACM Program. Lang. 4, POPL, Article 21 (Dec. 2019), 29 pages. doi:10.1145/3371089 [3] Tomislav Begušić and Garnet Kin-Lic Chan. 2025. Real-Time Operator Evolution in Two and Three Dimensions via Sparse Pauli Dynamics. PRX Quantum 6 (Apr 2025), 020302. Issue 2. doi:10.1103/PRXQuantum.6.020302 [4] Sergey Bravyi, Dan Browne, Padraic Calpin, Earl Campbell, David Gosset, and Mark Howard. 2019. Simulation of quantum circuits by low-rank stabilizer decompositions. Quantum 3 (Sept. 2019), 181. doi:10.22331/q-2019-09-02-181 [5] Lukas Burgholzer and Robert Wille. 2020. Improved DD-based Equivalence Checking of Quantum Circuits. In 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC). 127–132. doi:10.1109/ASP-DAC47756.2020.9045153 [6] Lukas Burgholzer and Robert Wille. 2021. Advanced Equivalence Checking for Quantum Circuits. (2021). [7] Lukas Burgholzer and Robert Wille. 2021. QCEC: A JKQ tool for quantum circuit equivalence checking. Software Impacts 7 (2021), 100051. doi:10.1016/j.simpa.2020.100051 [8] Lukas Burgholzer and Robert Wille. 2022. Handling non-unitaries in quantum circuit equivalence checking. In Proceedings of the 59th ACM/IEEE Design Automation Conference (San Francisco, California) (DAC ’22). Association for Computing Machinery, New York, NY, USA, 529–534. doi:10.1145/3489517.3530482 [9] Craig Gidney. 2021. Stim: a fast stabilizer circuit simulator. Quantum 5 (July 2021), 497. doi:10.22331/q-2021-07-06-497 [10] Daniel Gottesman. 1998. The Heisenberg Representation of Quantum Computers. arXiv:quant-ph/9807006 [quant-ph] https://arxiv.org/abs/quant-ph/9807006 [11] Xin Hong, Yuan Feng, Sanjiang Li, and Mingsheng Ying. 2022. Equivalence Checking of Dynamic Quantum Circuits. In Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design (San Diego, California) (ICCAD ’22). Association for Computing Machinery, New York, NY, USA, Article 127, 8 pages. doi:10.1145/3508352.3549479 [12] Xin Hong, Mingsheng Ying, Yuan Feng, Xiangzhen Zhou, and Sanjiang Li. 2022. Approximate Equivalence Checking of Noisy Quantum Circuits. In Proceedings of the 58th Annual ACM/IEEE Design Automation Conference (San Francisco, California, United States) (DAC ’21). IEEE Press, 637–642. doi:10.1109/DAC18074.2021.9586214 [13] Wei-Jia Huang. 2026. QuPRS: Quantum Path-sum Reduction and Solver. Source code, version 0.13.0. Lines 344–349. Accessed 2026-09-29. https://github.com/PhysicsQoo/QuPRS/blob/d6b9a8cfcf8671f58992aad19551c54d9a074b23/src/ QuPRS/interface/load_qiskit.py#L344-L349 [14] Wei-Jia Huang, Christophe Chareton, Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Alfons Laarman, and Jingyi Mei. 2026. Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting. In Tools and Algorithms for the Construction and Analysis of Systems, Sebastian Junges and Guy Katz (Eds.). Springer Nature Switzerland, Cham, 419–439. [15] IBM. 2022. Qiskit. https://qiskit.org/. [16] Vasileios Klimis, Avner Bensoussan, Elena Chachkarova, Karine Even-Mendoza, Sophie Fortz, and Connor Lenihan. 2025. Shaking Up Quantum Simulators with Fuzzing and Rigour. Proc. ACM Program. Lang. 9, OOPSLA2, Article 322 (Oct. 2025), 29 pages. doi:10.1145/3763100 [17] Junjie Luo, Shangzhou Xia, Fuyuan Zhang, and Jianjun Zhao. 2026. QEMI: A Quantum Software Stacks Testing Framework via Equivalence Modulo Inputs. In Fundamental Approaches to Software Engineering, Elvira Albert and Corina Pasareanu (Eds.). Springer Nature Switzerland, Cham, 149–169. [18] Dmitri Maslov. 2016. Advantages of using relative-phase Toffoli gates with an application to multiple control Toffoli optimization. Phys. Rev. A 93 (Feb 2016), 022311. Issue 2. doi:10.1103/PhysRevA.93.022311 [19] Jingyi Mei, Tim Coopmans, Marcello Bonsangue, and Alfons Laarman. 2024. Equivalence Checking of Quantum Circuits by Model Counting. In Automated Reasoning, Christoph Benzmüller, Marijn J.H. Heule, and Renate A. Schmidt (Eds.). Springer Nature Switzerland, Cham, 401–421. [20] Jingyi Mei, Dekel Zak, Muhammad Osama, Tim Coopmans, and Alfons Laarman. 2026. Quokka#: Quantum Computing with #SAT. In Computer Aided Verification, Eva Darulova, Anthony W. Lin, and Philipp Rümmer (Eds.). Springer Nature Switzerland, Cham, 387–406. [21] Yunseong Nam, Neil J. Ross, Yuan Su, Andrew M. Childs, and Dmitri Maslov. 2018. Automated optimization of large quantum circuits with continuous parameters. npj Quantum Information 4, 1 (10 May 2018), 23. doi:10.1038/s41534018-0072-4 [22] Muhammad Osama, Dimitrios Thanos, and Alfons Laarman. 2025. Parallel Equivalence Checking of Stabilizer Quantum Circuits on GPUs. In Tools and Algorithms for the Construction and Analysis of Systems, Arie Gurfinkel and Marijn Heule (Eds.). Springer Nature Switzerland, Cham, 109–128. [23] Mateusz Ostaszewski, Edward Grant, and Marcello Benedetti. 2021. Structure optimization for parameterized quantum circuits. Quantum 5 (Jan. 2021), 391. doi:10.22331/q-2021-01-28-391

, Vol. 1, No. 1, Article . Publication date: November 2026.

20

Shangzhou Xia, Junjie Luo, Qichen Wang, Yasunari Suzuki and Jianjun Zhao

[24] Matteo Paltenghi and Michael Pradel. 2023. MorphQ: Metamorphic Testing of the Qiskit Quantum Computing Platform. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). 2413–2424. doi:10.1109/ICSE48619. 2023.00202 [25] Hakop Pashayan, Oliver Reardon-Smith, Kamil Korzekwa, and Stephen D. Bartlett. 2022. Fast Estimation of Outcome Probabilities for Quantum Circuits. PRX Quantum 3 (Jun 2022), 020361. Issue 2. doi:10.1103/PRXQuantum.3.020361 [26] Tom Peham, Lukas Burgholzer, and Robert Wille. 2022. Equivalence Checking of Quantum Circuits With the ZXCalculus. IEEE Journal on Emerging and Selected Topics in Circuits and Systems 12, 3 (2022), 662–675. doi:10.1109/ JETCAS.2022.3202204 [27] Patrick Rall, Daniel Liang, Jeremy Cook, and William Kretschmer. 2019. Simulation of qubit quantum circuits via Pauli propagation. Phys. Rev. A 99 (Jun 2019), 062337. Issue 6. doi:10.1103/PhysRevA.99.062337 [28] Jérome Ricciardi, Sébastien Bardin, Christophe Chareton, and Benoît Valiron. 2025. Quantum Circuit Equivalence Checking: A Tractable Bridge From Unitary to Hybrid Circuits. arXiv:2511.22523 [quant-ph] https://arxiv.org/abs/ 2511.22523 [29] Manuel S. Rudolph, Tyson Jones, Yanting Teng, Armando Angrisani, and Zoë Holmes. 2026. Pauli Propagation: A Computational Framework for Simulating Quantum Systems. PRX Quantum 7 (Aug 2026), 032001. Issue 3. doi:10.1103/6vd7-l9bn [30] Dimitrios Thanos, Tim Coopmans, and Alfons Laarman. 2023. Fast Equivalence Checking of Quantum Circuits of Clifford Gates. In Automated Technology for Verification and Analysis: 21st International Symposium, ATVA 2023, Singapore, October 24–27, 2023, Proceedings, Part II (Singapore, Singapore). Springer-Verlag, Berlin, Heidelberg, 199–216. doi:10.1007/978-3-031-45332-8_10 [31] George F. Viamontes, Igor L. Markov, and John P. Hayes. 2007. Checking equivalence of quantum circuits and states. In Proceedings of the 2007 IEEE/ACM International Conference on Computer-Aided Design (San Jose, California) (ICCAD ’07). IEEE Press, 69–74. [32] G. Vidal and C. M. Dawson. 2004. Universal quantum circuit for two-qubit transformations with three controlled-NOT gates. Phys. Rev. A 69 (Jan 2004), 010301(R). Issue 1. doi:10.1103/PhysRevA.69.010301 [33] Jiyuan Wang, Qian Zhang, Guoqing Harry Xu, and Miryung Kim. 2021. QDiff: Differential Testing of Quantum Software Stacks. In 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE). 692–704. doi:10.1109/ASE51524.2021.9678792 [34] Robert Wille, Lucas Berent, Tobias Forster, Jagatheesan Kunasaikaran, Kevin Mato, Tom Peham, Nils Quetschlich, Damian Rovara, Aaron Sander, Ludwig Schmid, Daniel Schönberger, Yannick Stade, and Lukas Burgholzer. 2024. The MQT Handbook : A Summary of Design Automation Tools and Software for Quantum Computing. In 2024 IEEE International Conference on Quantum Software (QSW). IEEE, 1–8. doi:10.1109/qsw62656.2024.00013 [35] WindOctober. 2026. TwoQubitPeepholeOptimization applies a fidelity cutoff with approximation_degree=1.0. GitHub issue #16864, Qiskit/qiskit. Accessed: 2026-09-28. https://github.com/Qiskit/qiskit/issues/16864 [36] Shigeru Yamashita and Igor L. Markov. 2010. Fast equivalence-checking for quantum circuits. In 2010 IEEE/ACM International Symposium on Nanoscale Architectures. 23–28. doi:10.1109/NANOARCH.2010.5510932 [37] Ge Yan, Wenjie Wu, Yuheng Chen, Kaisen Pan, Xudong Lu, Zixiang Zhou, Yuhan Wang, Ruocheng Wang, and Junchi Yan. 2025. Quantum Circuit Synthesis and Compilation Optimization: Overview and Prospects. arXiv:2407.00736 [quant-ph] https://arxiv.org/abs/2407.00736 [38] Mingsheng Ying, Nengkun Yu, Yuan Feng, and Runyao Duan. 2011. Verification of Quantum Programs. arXiv:1106.4063 [cs.LO] https://arxiv.org/abs/1106.4063 [39] Nengkun Yu, Xuan Du Trinh, and Thomas Reps. 2025. Scalable Equivalence Checking and Verification of Shallow Quantum Circuits. Proc. ACM Program. Lang. 9, OOPSLA2, Article 375 (Oct. 2025), 28 pages. doi:10.1145/3763153

, Vol. 1, No. 1, Article . Publication date: November 2026.

Related documents

• Structure-Aware Quantum Circuit Equivalence Checking via Sparse Pauli Propagation#1658412
• Quantum-Inspired Algorithms beyond Unitary Circuits: the Laplace Transform#927218
• Methods for Automated Equivalence Checking of Quantum Error-Correction Codes#1343734
• QROB: Quantifying Realization Overhead in Quantum Compilation via Reverse Construction#984673
• Symmetry-preserving quantum compilation#1188335