发表机构
Shanghai Jiao Tong University（上海交通大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出Irene框架，通过保结构符号化简在门级、混合路径和及密度核三个层次验证混合量子程序等价性，在1982个程序对中解决79.92%，并发现15个编译器缺陷。
AI 中文摘要
等价性检查对于验证混合量子程序的编译器变换至关重要，此类程序结合了量子操作、测量和经典控制。依赖于测量的控制限制了酉推理，而经典结果与量子操作之间的依赖关系可能扩大中间符号状态。我们提出Irene，一个基于保结构符号化简的有界混合量子程序等价性检查框架。该框架通过三个推理层次逐步简化等价性义务。在门级，代数恒等式简化酉区域。在混合路径和（HPS）级别，简化的符号执行状态表示为类型化图，其同构性证明等价性。剩余义务由密度核处理，密度核刻画输入密度算子到可观测输出的变换，即使在内部测量历史不同的情况下也能进行比较。残余系数差异被编码为SMT查询。一组通用的符号化简通过保留因式化的布尔和算术表达式来支持HPS和密度核推理，在展开剩余和之前消除可归约的依赖关系。我们针对七个基准套件中的1,982个程序对，将Irene与五个等价性检查器进行评估。Irene解决了1,584对（79.92%），而基线中聚合覆盖率最高的MQT QCEC解决了57.52%，每个已解决对的平均端到端时间为3.93秒。作为等价性检查预言机应用时，Irene还识别了量子编译器（包括Qiskit、Cirq和PennyLane）中15个先前未知的缺陷。
英文摘要
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.
Comments21 pages, 5 figures, 3 tables, 1 algorithm
