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

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2610.11195

Retromorphic Testing of Quantum Compiler Passes

Mushahid Khan, Olivia Di Matteo

quant-phcs.SESubmitted Oct 8, 2026• Announced Oct 9, 2026• 0 citations
arXivHTMLPDF

Abstract

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.

Related papers

Concolic Testing for Quantum Compilers

Navnil Choudhury, Ameya Bhave, Kanad Basu

Quantum circuit transpilation is central to the execution of programs on noisy intermediate-scale quantum (NISQ) devices, yet it introduces reliability risks due to heuristic optimizations, parameter thresholds, and layout heuristics. Small perturbations at these decision points can silently alter program semantics, undermine optimization effectiveness, or increase hardware error susceptibility. In this work, we present a concolic testing framework for quantum compilers that systematically uncovers such vulnerabilities by combining concrete execution with symbolic reasoning. We identify and recover decision points in gate-level, parameter-sensitive, and circuit-level transpiler passes, and construct symbolic guards to drive targeted perturbations near boundary conditions. Our evaluation on representative QASMBench circuits demonstrates complete decision-point and boundary coverage of 100%, and high outcome coverage of 78%, uncovering both missed optimizations and semantic deviations in widely used Qiskit passes. These results establish that concolic testing can be applied as a practical methodology for systematically evaluating compiler robustness in the NISQ era.

IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD)•Nov 10, 2025•0 citations

Are We Testing the Wrong Quantum Bugs? A Study of Fault Representation Gaps in Quantum Software Testing

Asif Mohammed Saad, Ahsanul Ameen Sabit, Jonah Brandenburgh +3 more

Quantum software relies on compilers, intermediate representations, and execution frameworks that transform programs before execution. Faults in these components can change the behavior of otherwise correct quantum programs. Yet quantum testing techniques are often evaluated using mutation-generated faults and curated bug benchmarks. We investigate how well the faults represented by these artifacts reflect those encountered in modern quantum software. We audit four quantum mutation-testing tools and three curated bug benchmarks, and collect 410 verified bugs from ten quantum software repositories over two years. We classify faults from all three sources into a common taxonomy of 56 bug families and compare their representation across mutation operators, curated benchmarks, and recent real-world bugs. The mutation tools support 20 bug families, and curated benchmarks add 15 more. Yet only 56 of the 410 real-world bugs (13.7%) belong to families represented by either source; the remaining 354 (86.3%) belong to families absent from both. The largest unrepresented families concern compiler transformations (66 bugs), type handling (53), and input validation (47). Unlike local gate or statement changes, these faults often depend on intermediate representations, compiler pipelines, input types, or dependency versions. Existing mutation operators primarily modify circuits and program constructs, whereas many real-world faults arise in the compilers, representations, and framework interfaces that process them. Addressing this gap requires looking beyond circuit-level faults toward testing semantic preservation across compiler transformations, correctness at representation boundaries, and interactions between software components. Our study provides empirical evidence to guide fault models and benchmarks that capture these mechanisms and preserve the contexts needed to reproduce them.

arXiv:2610.22089•Oct 15, 2026•0 citations

CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler

Yunong Shi, Runzhou Tao, Li, Xupeng +4 more

We present CertiQ, a verification framework for writing and verifying compiler passes of Qiskit, the most widely-used quantum compiler. To our knowledge, CertiQ is the first effort enabling the verification of real-world quantum compiler passes in a mostly-automated manner. Compiler passes written in the CertiQ interface with annotations can be used to generate verification conditions, as well as the executable code that can be integrated into Qiskit. CertiQ introduces the quantum circuit calculus to enable the efficient checking of equivalence of quantum circuits by encoding such a checking procedure into an SMT problem. CertiQ also provides a verified library of widely-used data structures, transformation functions for circuits, and conversion functions for different quantum data representations. This verified library not only enables modular verification but also sheds light on future quantum compiler design. We have re-implemented and verified 26 (out of 30) Qiskit compiler passes in CertiQ, during which three bugs are detected in the Qiskit implementation. Our verified compiler pass implementations passed all of Qiskit's regression tests without showing noticeable performance loss.

arXiv:1908.08963•Aug 23, 2019•10 citations

QDiff: Differential Testing of Quantum Software Stacks

Jiyuan Wang, Qian Zhang, Guoqing Harry Xu +1 more

Over the past few years, several quantum software stacks (QSS) have been developed in response to rapid hardware advances in quantum computing. A QSS includes a quantum programming language, an optimizing compiler that translates a quantum algorithm written in a high-level language into quantum gate instructions, a quantum simulator that emulates these instructions on a classical device, and a software controller that sends analog signals to a very expensive quantum hardware based on quantum circuits. In comparison to traditional compilers and architecture simulators, QSSes are difficult to tests due to the probabilistic nature of results, the lack of clear hardware specifications, and quantum programming complexity.This work devises a novel differential testing approach for QSSes, named QDiff with three major innovations: (1) We generate input programs to be tested via semantics-preserving, source to source transformation to explore program variants. (2) We speed up differential testing by filtering out quantum circuits that are not worthwhile to execute on quantum hardware by analyzing static characteristics such as a circuit depth, 2-gate operations, gate error rates, and T1 relaxation time. (3) We design an extensible equivalence checking mechanism via distribution comparison functions such as Kolmogorov–Smirnov test and cross entropy.We evaluate QDiff with three widely-used open source QSSes: Qiskit from IBM, Cirq from Google, and Pyquil from Rigetti. By running QDiff on both real hardware and quantum simulators, we found several critical bugs revealing potential instabilities in these platforms. QDiff’s source transformation is effective in producing semantically equivalent yet not-identical circuits (i.e., 34% of trials), and its filtering mechanism can speed up differential testing by 66%.

IEEE/ACM International Conference on Automated Software Engineering (ASE)•Nov 1, 2021•60 citations

QITE: Assembly-Level, Cross-Platform Testing of Quantum Computing Platforms

Matteo Paltenghi, Michael Pradel

Quantum computing platforms are susceptible to quantum-specific bugs (e.g., incorrect ordering of qubits or incorrect implementation of quantum abstractions), which are difficult to detect and require specialized expertise. The field faces challenges due to a fragmented landscape of platforms and rapid development cycles that often prioritize features over the development of robust platform testing frameworks, severely hindering the reliability of quantum software. To address these challenges, we present QITE, the first cross-platform testing framework for quantum computing platforms, which leverages QASM, an assembly-level representation, to ensure consistency across different platforms. QITE introduces the novel ITE process to generate equivalent quantum programs by iteratively (I)mporting assembly into platform representations, (T)ransforming via platform optimization and gate conversion, and (E)xporting back to assembly. It uses a crash oracle to detect failures during cross-platform transformations and an equivalence oracle to validate the semantic consistency of the final sets of assembly programs, which are expected to be equivalent by construction. We evaluate QITE on four widely-used quantum computing platforms: Qiskit, PennyLane, Pytket, and BQSKit, revealing 17 bugs, 14 of which are already confirmed or even fixed. Our results demonstrate QITE's effectiveness, its complementarity to existing quantum fuzzers in terms of code coverage, and its ability to expose bugs that have been out of reach for existing testing techniques.

arXiv:2503.17322•Mar 21, 2025•0 citations

QTUNER: A Feature-Guided Adaptive Framework for Quantum-Compiler Optimization Pass Tuning

Ming Zhong, Xiangyu Ren, Jinglei Cheng +2 more

Quantum compiler optimization is important for improving the execution fidelity of quantum circuits. In practice, this optimization is often formulated as reducing circuit-level metrics. In classical compilers, pass tuning has been well-established through various methods. However, these methods cannot be directly applied to quantum compilers, because quantum programs exhibit quantum-specific features. Existing quantum compiler tuning studies have attempted to incorporate quantum circuit features with compiler tuning techniques, but they still suffer from two key limitations. First, they tune only a limited subset of optimization passes, leaving the global effectiveness of the full optimization pass space underexplored. Second, the quantum features they use are mainly static features, such as structure and DAG features, which are not directly tied to the optimization characteristics of quantum circuits. In this paper, we propose QTuner, a feature-guided framework for quantum compiler pass tuning. We first construct an optimization dataset by performing Bayesian Optimization and recording their optimized pass sequences. Based on this dataset, QTuner represents each circuit with two types of features: static circuit features and optimization-aware pass embeddings. Finally, QTuner trains two models offline, which are used to efficiently retrieve and rank promising pass sequences for a new circuit. We evaluate QTuner on two benchmarks across Qiskit and PyTKET compilers. On Qiskit, QTuner achieves up to a 10.6-percentage-point improvement in 2Q gate reduction over the strongest baseline while reducing tuning time by 73.59%. On PyTKET, QTuner achieves up to a 9.4-percentage-point improvement in 2Q gate reduction and reduces tuning time by 64.49%. These results demonstrate that QTuner enables efficient pass tuning across quantum compilers.

quant-pharXiv:2607.04586•Jul 7, 2026•0 citations
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.
Quantum circuit transpilation is central to the execution of programs on noisy intermediate-scale quantum (NISQ) devices, yet it introduces reliability risks due to heuristic optimizations, parameter thresholds, and layout heuristics. Small perturbations at these decision points can silently alter program semantics, undermine optimization effectiveness, or increase hardware error susceptibility. In this work, we present a concolic testing framework for quantum compilers that systematically uncovers such vulnerabilities by combining concrete execution with symbolic reasoning. We identify and recover decision points in gate-level, parameter-sensitive, and circuit-level transpiler passes, and construct symbolic guards to drive targeted perturbations near boundary conditions. Our evaluation on representative QASMBench circuits demonstrates complete decision-point and boundary coverage of 100%, and high outcome coverage of 78%, uncovering both missed optimizations and semantic deviations in widely used Qiskit passes. These results establish that concolic testing can be applied as a practical methodology for systematically evaluating compiler robustness in the NISQ era.
Quantum software relies on compilers, intermediate representations, and execution frameworks that transform programs before execution. Faults in these components can change the behavior of otherwise correct quantum programs. Yet quantum testing techniques are often evaluated using mutation-generated faults and curated bug benchmarks. We investigate how well the faults represented by these artifacts reflect those encountered in modern quantum software. We audit four quantum mutation-testing tools and three curated bug benchmarks, and collect 410 verified bugs from ten quantum software repositories over two years. We classify faults from all three sources into a common taxonomy of 56 bug families and compare their representation across mutation operators, curated benchmarks, and recent real-world bugs. The mutation tools support 20 bug families, and curated benchmarks add 15 more. Yet only 56 of the 410 real-world bugs (13.7%) belong to families represented by either source; the remaining 354 (86.3%) belong to families absent from both. The largest unrepresented families concern compiler transformations (66 bugs), type handling (53), and input validation (47). Unlike local gate or statement changes, these faults often depend on intermediate representations, compiler pipelines, input types, or dependency versions. Existing mutation operators primarily modify circuits and program constructs, whereas many real-world faults arise in the compilers, representations, and framework interfaces that process them. Addressing this gap requires looking beyond circuit-level faults toward testing semantic preservation across compiler transformations, correctness at representation boundaries, and interactions between software components. Our study provides empirical evidence to guide fault models and benchmarks that capture these mechanisms and preserve the contexts needed to reproduce them.
We present CertiQ, a verification framework for writing and verifying compiler passes of Qiskit, the most widely-used quantum compiler. To our knowledge, CertiQ is the first effort enabling the verification of real-world quantum compiler passes in a mostly-automated manner. Compiler passes written in the CertiQ interface with annotations can be used to generate verification conditions, as well as the executable code that can be integrated into Qiskit. CertiQ introduces the quantum circuit calculus to enable the efficient checking of equivalence of quantum circuits by encoding such a checking procedure into an SMT problem. CertiQ also provides a verified library of widely-used data structures, transformation functions for circuits, and conversion functions for different quantum data representations. This verified library not only enables modular verification but also sheds light on future quantum compiler design. We have re-implemented and verified 26 (out of 30) Qiskit compiler passes in CertiQ, during which three bugs are detected in the Qiskit implementation. Our verified compiler pass implementations passed all of Qiskit's regression tests without showing noticeable performance loss.
Over the past few years, several quantum software stacks (QSS) have been developed in response to rapid hardware advances in quantum computing. A QSS includes a quantum programming language, an optimizing compiler that translates a quantum algorithm written in a high-level language into quantum gate instructions, a quantum simulator that emulates these instructions on a classical device, and a software controller that sends analog signals to a very expensive quantum hardware based on quantum circuits. In comparison to traditional compilers and architecture simulators, QSSes are difficult to tests due to the probabilistic nature of results, the lack of clear hardware specifications, and quantum programming complexity.This work devises a novel differential testing approach for QSSes, named QDiff with three major innovations: (1) We generate input programs to be tested via semantics-preserving, source to source transformation to explore program variants. (2) We speed up differential testing by filtering out quantum circuits that are not worthwhile to execute on quantum hardware by analyzing static characteristics such as a circuit depth, 2-gate operations, gate error rates, and T1 relaxation time. (3) We design an extensible equivalence checking mechanism via distribution comparison functions such as Kolmogorov–Smirnov test and cross entropy.We evaluate QDiff with three widely-used open source QSSes: Qiskit from IBM, Cirq from Google, and Pyquil from Rigetti. By running QDiff on both real hardware and quantum simulators, we found several critical bugs revealing potential instabilities in these platforms. QDiff’s source transformation is effective in producing semantically equivalent yet not-identical circuits (i.e., 34% of trials), and its filtering mechanism can speed up differential testing by 66%.
Quantum computing platforms are susceptible to quantum-specific bugs (e.g., incorrect ordering of qubits or incorrect implementation of quantum abstractions), which are difficult to detect and require specialized expertise. The field faces challenges due to a fragmented landscape of platforms and rapid development cycles that often prioritize features over the development of robust platform testing frameworks, severely hindering the reliability of quantum software. To address these challenges, we present QITE, the first cross-platform testing framework for quantum computing platforms, which leverages QASM, an assembly-level representation, to ensure consistency across different platforms. QITE introduces the novel ITE process to generate equivalent quantum programs by iteratively (I)mporting assembly into platform representations, (T)ransforming via platform optimization and gate conversion, and (E)xporting back to assembly. It uses a crash oracle to detect failures during cross-platform transformations and an equivalence oracle to validate the semantic consistency of the final sets of assembly programs, which are expected to be equivalent by construction. We evaluate QITE on four widely-used quantum computing platforms: Qiskit, PennyLane, Pytket, and BQSKit, revealing 17 bugs, 14 of which are already confirmed or even fixed. Our results demonstrate QITE's effectiveness, its complementarity to existing quantum fuzzers in terms of code coverage, and its ability to expose bugs that have been out of reach for existing testing techniques.
Quantum compiler optimization is important for improving the execution fidelity of quantum circuits. In practice, this optimization is often formulated as reducing circuit-level metrics. In classical compilers, pass tuning has been well-established through various methods. However, these methods cannot be directly applied to quantum compilers, because quantum programs exhibit quantum-specific features. Existing quantum compiler tuning studies have attempted to incorporate quantum circuit features with compiler tuning techniques, but they still suffer from two key limitations. First, they tune only a limited subset of optimization passes, leaving the global effectiveness of the full optimization pass space underexplored. Second, the quantum features they use are mainly static features, such as structure and DAG features, which are not directly tied to the optimization characteristics of quantum circuits. In this paper, we propose QTuner, a feature-guided framework for quantum compiler pass tuning. We first construct an optimization dataset by performing Bayesian Optimization and recording their optimized pass sequences. Based on this dataset, QTuner represents each circuit with two types of features: static circuit features and optimization-aware pass embeddings. Finally, QTuner trains two models offline, which are used to efficiently retrieve and rank promising pass sequences for a new circuit. We evaluate QTuner on two benchmarks across Qiskit and PyTKET compilers. On Qiskit, QTuner achieves up to a 10.6-percentage-point improvement in 2Q gate reduction over the strongest baseline while reducing tuning time by 73.59%. On PyTKET, QTuner achieves up to a 9.4-percentage-point improvement in 2Q gate reduction and reduces tuning time by 64.49%. These results demonstrate that QTuner enables efficient pass tuning across quantum compilers.