Equivalence checking is essential for validating compiler transformations of hybrid quantum programs, which combine quantum operations, measurements, and classical control. Measurement-dependent control limits unitary reasoning, while dependencies between classical outcomes and quantum operations can enlarge intermediate symbolic states. We present Irene, an equivalence-checking framework for bounded hybrid quantum programs based on structure-preserving symbolic reduction. The framework progressively simplifies equivalence obligations through three levels of reasoning. At the gate level, algebraic identities simplify unitary regions. At the hybrid path-sum (HPS) level, reduced symbolic execution states are represented as typed graphs, whose isomorphism certifies equivalence. Remaining obligations are handled by density kernels that characterize transformations of input density operators into observable outputs, allowing comparison even when internal measurement histories differ. Residual coefficient differences are encoded as SMT queries. A common set of symbolic reductions supports HPS and density-kernel reasoning by preserving factored Boolean and arithmetic expressions, eliminating reducible dependencies before expanding residual sums. We evaluate Irene against five equivalence checkers on 1,982 program pairs from seven benchmark suites. Irene solves 1,584 pairs (79.92%), compared with 57.52% for MQT QCEC, the baseline with the highest aggregate coverage, with a mean end-to-end time of 3.93 seconds per solved pair. Applied as an equivalence-checking oracle, Irene also identifies 15 previously unknown bugs in quantum compilers, including Qiskit, Cirq, and PennyLane.
Equivalence checking is essential for validating compiler transformations of hybrid quantum programs, which combine quantum operations, measurements, and classical control. Measurement-dependent control limits unitary reasoning, while dependencies between classical outcomes and quantum operations can enlarge intermediate symbolic states. We present Irene, an equivalence-checking framework for bounded hybrid quantum programs based on structure-preserving symbolic reduction. The framework progressively simplifies equivalence obligations through three levels of reasoning. At the gate level, algebraic identities simplify unitary regions. At the hybrid path-sum (HPS) level, reduced symbolic execution states are represented as typed graphs, whose isomorphism certifies equivalence. Remaining obligations are handled by density kernels that characterize transformations of input density operators into observable outputs, allowing comparison even when internal measurement histories differ. Residual coefficient differences are encoded as SMT queries. A common set of symbolic reductions supports HPS and density-kernel reasoning by preserving factored Boolean and arithmetic expressions, eliminating reducible dependencies before expanding residual sums. We evaluate Irene against five equivalence checkers on 1,982 program pairs from seven benchmark suites. Irene solves 1,584 pairs (79.92%), compared with 57.52% for MQT QCEC, the baseline with the highest aggregate coverage, with a mean end-to-end time of 3.93 seconds per solved pair. Applied as an equivalence-checking oracle, Irene also identifies 15 previously unknown bugs in quantum compilers, including Qiskit, Cirq, and PennyLane.
As quantum computing becomes an emerging reality, designing efficient quantum programming capabilities is becoming more and more important. Particularly, the debugging and validation of quantum programs is of paramount importance, as these programs are by definition hard to test. Static analysis and formal verification methods for quantum programs started to emerge a few years now, yet they often miss hybrid quantum/classical reasoning facilities with, e.g., generic quantum control, classical control and classical computation instructions. In this paper, we lay out the foundations of a framework for the automated formal verification of (full) hybrid quantum programs featuring both classical and quantum control, measurement and hybrid data structures. In particular, we propose: (1) a novel symbolic representation for describing and manipulating sets of hybrid quantum/classical states called Hybrid Path-Sums (HPS); (2) a set of rewriting rules providing a rich mechanism for simplifying and reasoning on these symbolic hybrid states, and (3) a core assertion language to specify equivalence of hybrid quantum programs, the satisfaction of properties on (parts of) hybrid states, and the extraction of probabilistic statements about the program behavior. We prove the correctness of the novel symbolic representation, of its rewriting system and of the specification system. Finally, we propose a full implementation of this framework as a dedicated symbolic execution engine for hybrid programs. We present an evaluation of a set of representative hybrid case-studies from the literature, showcasing the advantage of our approach and its efficiency compared to state-of-the-art solutions.
Equivalence checking of hybrid quantum circuits is of primary importance, given that quantum circuit transformations are omnipresent along the quantum compiler chain. While some approaches exist for automating this task, most focus on the simple case of unitary circuits. At the same time, real quantum computing requires hybrid circuits equipped with measurement operators. Moreover, the few approaches targeting the hybrid case are limited to a restricted class of problems. We propose tackling the Quantum Hybrid Circuit Equivalence Checking problem through lifting unitary circuit verification using a transformation known as deferred measurement. We show that this approach alone significantly outperforms prior work, and that, with the addition of specific unitary-level techniques we call separation and projection, it can handle much larger classes of hybrid circuit equivalence problems. We have implemented and evaluated our method over standard circuit transformations such as teleportation, one-way measurement, or the IBM Qiskit compiler, demonstrating its promises. As a side finding, we have identified and reported several unexpected behaviours with the Qiskit compiler.
Hybrid quantum-classical compilation relates ideal operations and measurement outcomes to control pulses and device instructions. Existing formats each describe part of this process, and their preservation checks are often specific to one tool rather than to a common intermediate representation (IR). I present Qaiji-IR, an eight-layer IR family organized by a five-axis semantic contract for data, semantics, lowering, runtime, and verification. Its implementation provides typed circuits, an operation-semantics layer (L4) that records operation structure and checks a bounded set of equivalence rules, and a native-scheduling layer (L2) with separate validation. Nine circuit pairs are compared with ideal reference calculations. An aggregate baseline, which compares operation categories and measurement counts, accepts four behavior-changing transformations: gate reordering and changes of rotation angle, operand, or measurement destination. The L4 checker passes none of them. It distinguishes strict equality from equality up to global phase and returns unsupported when its rules cannot decide, as for valid rotation fusion. L2 validation checks native schedules against their source circuits, decomposition rules, local matrices, and configured timing. A single-qubit active-reset program is compiled through the Qaiji-IR frontend, a syntax adapter, and the EmuPlat backend into pulses and device instructions for a virtual pulse processing unit (VPPU). Injected binary outcomes select the conditional drive. Backend predicate tests reveal incorrect execution for equality to zero and for a nonbinary feedback value. This backend path does not use the validated L2 schedule. Physical measurement feedback, calibrated pulse fidelity, and feedback latency require further work.
Compiling quantum programs for fault-tolerant execution requires transforming high-level operations through multiple abstraction layers: from logical gates to error-corrected encodings to hardware-native instructions. A key challenge is that quantum error correction turns purely quantum programs into hybrid quantum-classical programs, where classical feedback from syndrome measurements drives quantum corrections at runtime. Existing compilation frameworks handle these quantum and classical components separately, requiring manual adaptation of classical logic at each compilation stage, all while preserving program semantics. We present qstack, a compiler framework built around a purely quantum intermediate representation in which classical logic is accessed only through opaque callbacks, written in any classical language. The framework's central mechanism, callback wrapping, enables compositional compilation: each compiler pass automatically adapts both quantum operations and their associated classical callbacks, and any kernel dynamically generated by a callback is compiled through the full pipeline. This allows ISA translation and quantum error correction to be expressed as composable compiler passes, including concatenation of error-correcting codes, without manual intervention. We demonstrate end-to-end compilation from a high-level gate set through Clifford gates to trapped-ion native operations, with bit-flip and phase-flip repetition codes, the Steane code, and the Shor code obtained by composing two repetition passes.
Realizing a conceptual quantum algorithm on an actual physical device necessitates the algorithm's quantum circuit description to undergo certain transformations in order to adhere to all constraints imposed by the hardware. In this regard, the individual high-level circuit components are first synthesized to the supported low-level gate-set of the quantum computer, before being mapped to the target's architecture-utilizing several optimizations in order to improve the compilation result. Specialized tools for this complex task exist, e.g., IBM's Qiskit, Google's Cirq, Microsoft's QDK, or Rigetti's Forest. However, to date, the circuits resulting from these tools are hardly verified, which is mainly due to the immense complexity of checking if two quantum circuits indeed realize the same functionality. In this paper, we propose an efficient scheme for quantum circuit equivalence checking-specialized for verifying results of the IBM Qiskit quantum circuit compilation flow. To this end, we combine characteristics unique to quantum computing, e.g., its inherent reversibility, and certain knowledge about the compilation flow into a dedicated equivalence checking strategy. Experimental evaluations confirm that the proposed scheme allows to verify even large circuit instances with tens of thousands of operations within seconds or even less, whereas state-of-the-art techniques frequently time-out or require substantially more runtime. A corresponding open source implementation of the proposed method is publicly available at https://github.com/iic-jku/qcec.
While quantum hardware remains limited, hybrid quantum-classical algorithms with complex control structures, including unbounded loops, are emerging, posing new challenges for quantum program analysis, including the accurate estimation of the resource consumption of a given program. Meanwhile, precise analysis techniques such as symbolic execution have largely left out hybridization and unbounded recursion. On the other hand, current quantum Hoare logics that generally support them are lacking in expressiveness and miss out on efficient computational equational reasoning that could be implemented in a semi-automated tool. This leaves a gap awaiting to be filled. In this work, we answer this challenge with the first semi-automated static analysis solution combining effective functional verification and resource (termination or cost) estimation for hybrid quantum programs with unbounded loops. Towards that end, we introduce integer hybrid path-sums (IHPS), extending path-sums to handle unbounded while loops, as a representation of possible executions of a program. A generic strategy for determining termination and expected resource consumption via loop invariants is also proposed and illustrated on several examples. Finally, the solution is implemented as a semi-automatic Haskell program. This work is the first step toward the design of a complete static resource analysis tool for hybrid quantum programs, essential for the development of real-world quantum computing.