Irene checks equivalence of hybrid quantum programs accurately and fast
Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction
Programming LanguagesLogic in Computer ScienceSoftware Engineering
Summary
Checking if two quantum programs do the same thing is hard, especially when they mix quantum and classical parts together. The authors present Irene, a tool that simplifies this process by breaking it down into different stages of reasoning and using symbolic math and graph comparisons. Irene can handle complex cases where measurements and classical controls interact, and it proved better than other tools on many test programs. It even found bugs in popular quantum programming tools, showing its practical usefulness.
What this means in practice
- •For quantum compiler developers: Automatically verify that compiler optimizations preserve program behavior across quantum and classical parts, improving compiler reliability.
- •For software quality assurance teams: Detect hidden bugs in hybrid quantum software by checking program equivalences during testing phases.
Authors
Jingyu Ke, Jingyang Li, Guoqiang Li
Abstract
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.