Source-linked AI summary
Retromorphic Testing of Quantum Compiler Passes
Mushahid Khan, Olivia Di Matteo
TL;DR
Large, deeply entangled quantum circuits make expected-output validation computationally intractable, complicating compiler-pass testing. RetroQ uses retromorphic testing to automate pass verification, and its evaluation reproduced known bugs and uncovered additional defects.
Problem
Expected outputs for large, deeply entangled circuits are computationally intractable, making compiler-pass correctness difficult to validate with manual oracles.
Source: §I · p. 1Method
RetroQ pairs a forward program with its inverse to create an internal verification oracle for compiler passes, avoiding manual expected-output derivation and knowledge of program internals.
Source: A. Retromorphic Testing · p. 2, §VI · p. 9Results
RetroQ reproduced known bugs and uncovered defects including symbolic-reasoning and adjoint-logic failures, incorrect commutation, runtime failures, and controlled-context global-phase sign inversions.
Source: C. Discussions and Summary of Findings · pp. 8–9, §VI · p. 9Takeaways & Limitations
The evaluation supports retromorphic testing as effective in a quantum context, and the authors argue pass-specific testing can support quantum-compiler reliability and correctness.
Source: §VI · p. 9The current evaluation uses small programs.
Source: §VI · p. 9
Abstract
from arXiv · showhide
Quantum compilers play a critical role in transforming high-level quantum programs into optimized, hardware-compatible circuits. However, verifying the correctness of compiler passes remains challenging, as determining the expected output of large, deeply entangled quantum circuits is computationally intractable. This challenge is further amplified when compiler passes modify already complex circuit structures, making manual validation of transformed circuits impractical. In this work, we perform a systematic analysis of unit tests for quantum compiler passes in four quantum programming frameworks (PennyLane, Qiskit, Cirq, and pytket). Our findings indicate validation is dominated by program-content and program-metric assertions, and test circuits are generally small and shallow. Motivated by these observations, we introduce a testing methodology for automated validation of quantum compiler passes based on retromorphic testing and principles from the Hadamard test. This methodology analyzes a compiler pass, test circuit, and expected pass behavior to verify semantic preservation and intended structural modifications. We implement our methods in a framework, RetroQ, and apply it to compiler passes in PennyLane and Qiskit. Experimental evaluation reproduced several existing bugs as well as uncovered previously undetected defects, such as flawed symbolic parameter handling, incorrect commutation logic, failure to recognize self-adjointness of gates, and runtime crashes. These findings highlight the need for compiler-pass-specific testing methodologies to improve the reliability of the evolving quantum software stack.
I. INTRODUCTION
Quantum compiler passes are difficult to validate when large, entangled circuits lack tractable expected outputs. The paper introduces RetroQ, which uses retromorphic testing to check pass behavior without manually deriving those outputs.
I. INTRODUCTION
- Large, deeply entangled circuits make expected-output computation intractable, while manual oracles and formal verification face substantial hurdles.Unit tests may cover simple cases but fail to provide coverage for these circuits.Source: §I · p. 1
- Because quantum operations are unitary and reversible, the methodology can also extend to quantum arithmetic, uncomputation, and quantum-error-correction encoding circuits.The implementation supports PennyLane and Qiskit, while the methodology is described as applicable to transformations in any framework.Source: §I · p. 2
- RetroQ takes compiler passes, a target quantum function, and expected pass behavior as inputs, automating evaluation without manual derivation of expected outputs.The framework combines retromorphic testing, Hadamard-test principles, and knowledge of expected pass behavior.Source: §I · pp. 1–2
- Evaluation reproduced and uncovered pass defects, including runtime crashes, failures with symbolic parameters, incorrect commutation, and limitations recognizing self-adjoint operators.The results also highlight the importance of global phase in a controlled context.Source: §I · p. 2
A. Retromorphic Testing
- Retromorphic testing pairs a forward program with its inverse to check whether the original input is restored, without requiring knowledge of the program’s implementation.It is one of three black-box testing techniques described alongside differential and metamorphic testing.Source: A. Retromorphic Testing · p. 2
B. Quantum Software Testing
The section reviews platform-level and compiler-pass testing, then analyzes assertion practices and test-circuit scale across four quantum frameworks. Existing checks emphasize circuit contents and metrics, while test circuits are generally shallow and small.
B. Quantum Software Testing
- Platform-level testing spans programming languages, compilers, and execution environments, but holistic methods aggregate errors across layers rather than isolate compiler transformations.These methods may report a final measurement or system-wide crash.Source: B. Quantum Software Testing · pp. 2–3
- QDiff compares measurement distributions across transformed programs, MorphQ(++) exercises Qiskit through program transformations, and QITE tests across platforms using crash and equivalence oracles.QDiff uses seven gate-transformation rules; MorphQ(++) identifies faults through unexpected crashes rather than output-relationship comparisons.Source: B. Quantum Software Testing · pp. 2–3
- Formal approaches verify individual transformations, but VOQC requires specialized proof effort and Giallar is restricted by fixed loop templates and incomplete rewrite rules.Manual VOQC proofs can exceed the code size by more than an order of magnitude.Source: B. Quantum Software Testing · p. 3
III. QUANTUM COMPUTING FRAMEWORK UNIT TESTING
- The study extracted assertions from test-file syntax trees, manually classified their intent, and instrumented circuits to record depth and qubit counts across four frameworks.It examined 113 PennyLane, 31 Qiskit, 55 Cirq, and 1 pytket test files, and measured 1,518, 7,559, 1,682, and 119 circuits, respectively.Source: §III · p. 3
- Program-content and program-metric assertions dominate compiler-pass validation, while practices vary by framework; Cirq has comparatively high Matrix Equivalence assertions and PennyLane alone tests Gradient Equivalence.Pytket allocates 50.88% of assertions to Program Metrics; execution details and output-property equivalence appear infrequently.Source: §III · p. 3
- Most circuits are shallow: about 95% of Cirq, PennyLane, and Qiskit circuits and 81.36% of pytket circuits have depth 1-10.Circuits in Cirq, pytket, and PennyLane are concentrated below 50 qubits; Qiskit includes extreme outliers, including nearly 900 qubits.Source: §III · pp. 3–4
IV. RETROMORPHIC QUANTUM COMPILER TESTING (RETROQ)
RetroQ tests compiler passes by comparing original and transformed circuits without requiring manually specified expected outputs. It checks semantic preservation and structural properties through two verification stages.
IV. RETROMORPHIC QUANTUM COMPILER TESTING (RETROQ)
- RetroQ combines retromorphic testing with the Hadamard test to compare original and transformed circuits without manual expected outputs.It generates transformed circuits using a compiler pass, then checks whether semantic behavior and structural properties are preserved.Source: §IV · p. 4
- Circuit equivalence means identical outcomes for all input states, up to numerical tolerance and global phases.RetroQ uses this equivalence as the basis for semantic correctness.Source: §IV · p. 4
- RetroQ models correctness with a semantic-preservation predicate and predicates over structural properties.The semantic predicate is true when the original and transformed circuits are equivalent; structural predicates constrain circuit metrics such as gate count, depth, or qubit count.Source: §IV · pp. 4–5
- RetroQ evaluates whether a transformed circuit satisfies semantic information and structural property predicates through a two-stage verification process: an adjoint identity check followed by a controlled adjoint identity check.Source: §IV · p. 5
A. Stage 1: Adjoint Identity Check
Stage 1 checks compiler-pass behavior by comparing adjoint-based circuit variants with an identity-check baseline. It compares both semantic outcomes and structural properties against the baseline.
A. Stage 1: Adjoint Identity Check
- The baseline prepares qubits with an initialization operator, applies F and then F’s adjoint, and finally applies the initialization operator’s adjoint; every qubit should measure |0⟩.The baseline circuit is shown in Figure 3.Source: A. Stage 1: Adjoint Identity Check · p. 5, Figure 3 · p. 5
- RetroQ tests two variants: applying the pass to F† and applying the pass to F before taking its adjoint.These variants are shown in Figure 4 as ζ(F †) and ζ(F)†.Source: A. Stage 1: Adjoint Identity Check · p. 5, Figure 4 · p. 5
- Adjoint testing matters because adjoints occur in uncomputation and reversible subroutine construction, and their representation can affect pass behavior.The framework currently uses identity as its default initialization, focusing on passes dependent only on operation sequence and structure; other initialization routines could expose state-sensitive behavior.Source: A. Stage 1: Adjoint Identity Check · p. 5
- For each variant, RetroQ compares semantic and structural information against the baseline; deviations indicate that a verification predicate was violated.Semantic information includes whether each qubit returns to |0⟩.Source: A. Stage 1: Adjoint Identity Check · p. 5
- Automatically deriving and checking expected properties provides a test oracle without requiring users to manually calculate expected outputs for large circuits.The authors describe this as enabling more scalable verification of compiler transformations.Source: A. Stage 1: Adjoint Identity Check · p. 5
B. Stage 2: Controlled Adjoint Identity Check
Stage 2 tests whether compiler-pass behavior remains correct inside controlled operations. It embeds transformed variants in a Hadamard-test-like circuit and compares them with a baseline.
B. Stage 2: Controlled Adjoint Identity Check
- The Hadamard test estimates the real or imaginary part of ⟨ψ| U |ψ⟩ using an auxiliary qubit, a controlled-U operation, and measurement.For an identity U, the auxiliary qubit’s expectation value ⟨Z⟩ should be +1.Source: B. Stage 2: Controlled Adjoint… · p. 5
- The Stage 2 baseline resembles a Hadamard-test circuit, with the auxiliary qubit expected to yield an expectation value of +1.The baseline circuit is shown in Figure 5.Source: B. Stage 2: Controlled Adjoint… · p. 5, Figure 5 · p. 5
- RetroQ creates three transformed variants combining control, adjoint, and compiler-pass operations inside the verification circuit.The variants are shown in Figure 6.Source: B. Stage 2: Controlled Adjoint… · p. 5, Figure 6 · p. 6
- For each variant, RetroQ compares the auxiliary-qubit expectation value and structural information with the baseline.A deviation may indicate a pass bug or unintended propagation of the pass’s effects onto the auxiliary qubit, informing how the pass should be applied with controlled operators.Source: B. Stage 2: Controlled Adjoint… · p. 6
C. Example Application of RetroQ
The example applies RetroQ to PennyLane’s cancel-inverses pass on a circuit containing two Hadamard gates. The pass fails the expected gate-count reduction because it does not recognize Hadamard self-adjointness.
C. Example Application of RetroQ
- The example targets two consecutive Hadamard gates with the cancel-inverses pass, which is designed to remove redundant adjoint or self-inverse operations.The user specifies an expectation that gate count decreases; the example describes gate count as RetroQ’s currently supported predicate, with increase, decrease, or unchanged options.Source: C. Example Application of RetroQ · p. 6
- Stage 1’s identity-initialized baseline establishes reference structural properties, including total gate count, and target expectation values.The example baseline circuit is shown in Figure 7.Source: C. Example Application of RetroQ · p. 6, Figure 7 · p. 6
- Stage 1’s gate_count stayed at baseline 4 (actual 4), and Stage 2’s stayed at baseline 6 (actual 6), violating the expected reductions.For the identity initialization example, the expected counts were 2 and 4, respectively.Source: C. Example Application of RetroQ · p. 6
- The pass failed to recognize that consecutive adjoints of Hadamard gates cancel because Hadamard is self-adjoint.The reported limitation also extends to PennyLane’s Pauli X, Y, and Z, identity, CNOT, and Toffoli gates.Source: C. Example Application of RetroQ · pp. 6–7
V. RESULTS
RetroQ identified or reproduced six bugs while evaluating five compiler passes from Qiskit and PennyLane. The evaluation used small target programs to test intended transformations and checked semantic and structural expectations.
V. RESULTS
- The evaluation tested five passes: two from Qiskit and three from PennyLane, each designed to reduce gate count.The passes were selected because RetroQ checks this structural property.Source: §V · p. 7
- Six bugs were identified or reproduced, including a bug described earlier in the paper.For all identified bugs, the tests used the Identity operator as the initialization function.Source: §V · p. 7
- Small target programs exercised intended behaviors such as inverse cancellation, identity removal, gate fusion, and pattern matching.The transformed circuits were checked against user-specified semantic and structural expectations.Source: §V · p. 7
A. Qiskit Evaluation: Replication of Existing Bugs
The Qiskit evaluation reproduced incorrect SWAP cancellation and failure to remove symbolic zero-angle gates. Both findings occurred in tests of the passes’ intended structural behavior.
1) Incorrect Commutation Inverse Cancellation with SWAP and Controlled-RZ Gates
- The commutation pass incorrectly moved a SWAP through Controlled-RZ and canceled both SWAPs, although the operation count should remain unchanged.The circuit isolates the commutation logic; the behavior occurred in both verification stages.Source: 1) Incorrect Commutation Inverse… · p. 7
2) Zero Angled Parameterized Gate Not Removed
- The identity-removal pass did not reduce gate count for ry(d * 0), despite its symbolic parameter expression being equivalent to zero.The same issue affects RZ and RX gates and reflects a limitation in handling symbolic expressions; the experiment was motivated by Qiskit Issue #6468.Source: 2) Zero Angled Parameterized Gate Not… · p. 7
B. PennyLane: Previously-Undetected Issues
The PennyLane evaluation found a runtime crash in inverse cancellation on a general unitary and a global-phase issue when fusion was applied to an adjoint circuit. The latter produced an incorrect expectation value in a controlled context.
1) Crash in Program with Cancel Inverses
- Cancel inverses crashed at runtime on a unitary followed by its adjoint, as inverse detection compared array-valued gate parameters.The pass is intended to remove adjacent inverses even when represented as general unitary matrices.Source: 1) Crash in Program with Cancel Inverses · p. 8
2) Global Phase and Controlled Operator
- Despite Hadamard being excluded from fusion, applying the pass to the adjoint produced a GlobalPhase; under control, the expectation value became −1 rather than +1.The passage notes that such global-phase outputs must be managed or ignored when the transformed circuit is nested within a control context.Source: 2) Global Phase and Controlled Operator · p. 8
3) Adjoint of Quantum Operation Not Considered in Pattern Matching Optimization
Pattern matching failed to recognize the adjoint of a self-adjoint gate sequence as the defined pattern, so the expected gate-count reduction did not occur.
3) Adjoint of Quantum Operation Not Considered in Pattern Matching Optimization
- In both stages, pattern matching missed H†Z†H† as a match for HZH, despite the gates being self-adjoint, and gate counts did not decrease.The test expected fewer gates for this pattern-matching optimization.Source: 3) Adjoint of Quantum Operation Not… · p. 8
C. Discussions and Summary of Findings
RetroQ reproduced known compiler bugs and uncovered new defect types, while the unit-test analysis found generally small, shallow test circuits. The evaluation also has boundaries: manual circuit selection may miss edge cases, and identity-only initialization may leave some defects undetected.
C. Discussions and Summary of Findings
- Stage 1 exposed symbolic zero-angle gates, incomplete Pauli identity recognition, and PennyLane runtime crashes; Stage 2 showed controlled global phases can invert expectation signs.The reported incorrect expectation value was −1 instead of +1.Source: C. Discussions and Summary of Findings · p. 8
- The PennyLane team confirmed one reported bug, received a feature request for optional phase preservation, and identified qp.simplify as a resolution for another issue.The confirmed bug was reported on GitHub; qp.simplify reduces arithmetic depth or rotation parameters.Source: C. Discussions and Summary of Findings · p. 8
- The study identifies five error categories, with symbolic-reasoning, abstraction-gap, and structural-logic errors caught across Stages 1 and 2, and phase-management and adjoint failures in Stages 1a and 2a.The categories include incorrect commuting of non-commuting gates and failure to recognize inverted sequences equivalent to defined patterns.Source: C. Discussions and Summary of Findings · pp. 8–9
- Manual circuit selection may miss edge cases, tested circuits are small, and identity-only initialization may leave some defects undetected.The paper's example shows that two Hadamard gates could expose a faulty Swap–Swap–Controlled-RZ sequence that identity initialization misses.Source: C. Discussions and Summary of Findings · p. 9
VI. CONCLUSION
- Across four frameworks, unit-test validation was dominated by program-content and program-metric assertions, while most test circuits had depth 1–10.The authors suggest reliance on simple circuits may leave bugs that more complex circuits could expose undetected.Source: §VI · p. 9
- RetroQ uses a forward program paired with its inverse as an internal oracle, avoiding manual expected-output derivation and knowledge of internal program structure.It combines retromorphic testing, Hadamard-test principles, and expected pass behavior.Source: §VI · p. 9
- RetroQ reproduced known bugs and uncovered new defects, including abstraction-gap and adjoint-logic failures and controlled-operation expectation-sign inversions.The evaluation used small programs, though the verification procedure can generalize to larger ones by constructing program inverses.Source: §VI · p. 9
- Future work includes suitable initial-state strategies, test-program generation, automated structural expectations, and support for Cirq and pytket.Source: §VI · p. 9