AI 中文总结
针对量子编译中辅助量子位安全性的形式验证难题，提出端到端验证-修复框架，通过两步归约策略实现高效并行验证，可分类错误并修复局域故障，工具可扩展至数千量子位且效果良好。
AI 中文摘要
确保辅助量子位（ancilla）安全性是量子编译的关键正确性要求，因为辅助量子位常被引入以用更少的门和更浅的深度实现复杂操作。然而，由于量子位数量导致的状态空间爆炸，形式验证该属性计算难度极大，尤其是对于携带未知初始状态且使用后必须恢复的脏辅助量子位（dirty ancillae）。我们提出一种端到端的验证-修复框架，严格解决干净和脏辅助量子位的安全性问题。核心贡献是两步归约策略：首先证明验证m位脏辅助量子位寄存器可分解为2m个独立的干净辅助量子位安全性检查；随后将每个干净辅助量子位安全性实例归约为与Pauli-Z和Pauli-X算子的代数交换性检查。该方法生成高效且天然并行的验证器，并通过将违规分类为逻辑错误和相位错误实现可操作的诊断。利用此诊断，我们进一步设计轻量级修复例程，附加局域单量子位旋转以消除广泛类别的局域辅助量子位故障。我们使用结合决策图和加权模型计数的双后端架构在原型工具中实现完整流程，并在从算术基准到Grover算法的各类电路上验证。实验表明其可扩展至数千量子位，且所提出的修复措施在保留电路功能的同时有效提升辅助量子位安全性。
英文摘要
Ensuring ancilla safety is a critical correctness requirement for quantum compilation, since ancilla qubits are routinely introduced to implement complex operations with fewer gates and reduced depth. However, formally verifying this property is computationally hard due to state-space explosion in the number of qubits, particularly for dirty ancillae, which carry unknown initial states and must be restored after use. We propose an end-to-end verification-and-repair framework that rigorously addresses both clean and dirty ancilla safety. Our core contribution is a two-step reduction strategy: we first prove that verifying an $m$-qubit dirty ancilla register decomposes into $2m$ independent clean ancilla safety checks; subsequently, we reduce each clean ancilla safety instance to an algebraic commutativity check against Pauli-$Z$ and Pauli-$X$ operators. This approach yields an efficient and naturally parallel verifier and enables actionable diagnosis by classifying violations into logic errors and phase errors. Leveraging this diagnosis, we further design lightweight repair routines that append local single-qubit rotations to eliminate a broad class of local ancilla faults. We implement the full pipeline in a prototype tool using a dual-backend architecture combining decision diagrams and weighted model counting, and validate it on diverse circuits ranging from arithmetic benchmarks to Grover's algorithm. Our experiments demonstrate scalability to thousands of qubits and show that the proposed repairs effectively improve ancilla safety while preserving circuit functionality.
DOI：10.1007/978-3-032-32537-2_16
