Formal Verification of Quantum Ancilla Safety

Abstract

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.

References in corpus (15)

• Quantum Computing in the NISQ era and beyond
• Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer
• Elementary gates for quantum computation
• The ITensor Software Library for Tensor Network Calculations
• Simulating quantum computation by contracting tensor networks
• Halving the cost of quantum addition
• QuEST and High Performance Simulation of Quantum Computers
• Q#: Enabling scalable quantum computing and development with a high-level domain-specific language
• PyZX: Large Scale Automated Diagrammatic Reasoning
• Trading T gates for dirty qubits in state preparation and unitary synthesis
• QWIRE Practice: Formal Verification of Quantum Circuits in Coq
• ReQWIRE: Reasoning about Reversible Quantum Circuits
• Beyond NISQ: The Megaquop Machine
• Decision Diagrams for Quantum Computing
• Reqomp: Space-constrained Uncomputation for Quantum Circuits