Formal Verification of Quantum Ancilla Safety

• URL: http://arxiv.org/abs/2608.13099v1
• Date: Thu, 13 Aug 2026 11:20:06 GMT
• Title: Formal Verification of Quantum Ancilla Safety
• Abstract summary: We propose an end-to-end verification-and-repair framework for clean and dirty ancilla safety.<n>We first prove that verifying an $m$-qubit dirty ancilla register decomposes into $2m$ independent clean ancilla safety checks.<n>We then reduce each clean ancilla safety instance to an algebraic commutativity check against Pauli-$Z$ and Pauli-$X$ operators.
• Score: 3.5368690233168114
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Sound Debloating of Redundant Checks in Zero-Knowledge Machine-Learning Circuits [8.87115326771099]
  We present an automated framework that removes redundant checks while provably preserving soundness.<n>Our tool removes up to 48.7% of constraints and reduces prover time by up to 72.8%, without weakening security.
  arXiv  Detail & Related papers  (2026-09-09T13:27:25Z)
• The Gain-Engineered Transmon [68.89136228609398]
  We introduce and experimentally realize a noise-biased qubit in a standard transmon-readout resonator circuit.<n>Our results open a path towards using this system as a simple building-block for hardware-efficient quantum error detection and correction schemes.
  arXiv  Detail & Related papers  (2026-08-26T17:00:42Z)
• Quantum Uncomputation of Clean and Dirty Ancilla Qubits [1.6179458386967447]
  We present a unified formalization of the uncomputation of both clean and dirty ancillas.<n>We introduce two complementary synthesis-oriented existence-checking methods.<n>Compared to the state-of-the-art Reqompcitereqomp, RwUn achieves 100% coverage on practical complex-dependency benchmarks.
  arXiv  Detail & Related papers  (2026-08-10T13:13:54Z)
• Raw-Curve Quantum Fingerprints: A Mahalanobis Authentication Framework with Drift Early Warning and Adversarial Detection [11.819995530903567]
  Quantum cloud platforms are poised to deliver powerful computing capabilities, but users have no direct means to verify which physical device executes their workload.<n>This lack of transparency enables hardware substitution attacks, where a malicious adversary could redirect a job to a substituted or inferior processor.<n>We present a general authentication framework that addresses this problem by constructing multi-dimensional quantum fingerprints from raw measurement data.
  arXiv  Detail & Related papers  (2026-06-10T04:10:21Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA (Dynamic Analysis-enhanced Issue Resolution Agent) is an automated repair framework that embeds dynamic analysis into the agent's reasoning cycle.<n> Driven by a Test Tracing-Driven methodology, DAIRA utilizes lightweight monitors to extract critical runtime data.<n>When powered by Gemini 3 Flash Preview, DAIRA establishes a new state-of-the-art (SOTA) performance, achieving a 79.4% resolution rate on the SWE-bench Verified dataset.
  arXiv  Detail & Related papers  (2026-03-23T14:48:54Z)
• Dynamical error reshaping for dual-rail erasure qubits [1.6312989763677892]
  We show how to suppress the adverse effects of transmon-induced noise while performing erasure checks or two-qubit gates.<n>We present control schemes for these operations that suppress erasure check errors by two orders of magnitude.
  arXiv  Detail & Related papers  (2025-10-09T16:35:22Z)
• Verification-Aided Learning of Neural Network Barrier Functions with Termination Guarantees [6.9060054915724]
  Barrier functions are a general framework for establishing a safety guarantee for a system. There is no general method for finding these functions. Recent approaches use self-supervised learning techniques to learn these functions.
  arXiv  Detail & Related papers  (2024-03-12T04:29:43Z)
• Demonstrating a long-coherence dual-rail erasure qubit using tunable transmons [59.63080344946083]
  We show that a "dual-rail qubit" consisting of a pair of resonantly coupled transmons can form a highly coherent erasure qubit. We demonstrate mid-circuit detection of erasure errors while introducing $ 0.1%$ dephasing error per check. This work establishes transmon-based dual-rail qubits as an attractive building block for hardware-efficient quantum error correction.
  arXiv  Detail & Related papers  (2023-07-17T18:00:01Z)
• Software mitigation of coherent two-qubit gate errors [55.878249096379804]
  Two-qubit gates are important components of quantum computing. But unwanted interactions between qubits (so-called parasitic gates) can degrade the performance of quantum applications. We present two software methods to mitigate parasitic two-qubit gate errors.
  arXiv  Detail & Related papers  (2021-11-08T17:37:27Z)
• Fault-tolerant parity readout on a shuttling-based trapped-ion quantum computer [64.47265213752996]
  We experimentally demonstrate a fault-tolerant weight-4 parity check measurement scheme. We achieve a flag-conditioned parity measurement single-shot fidelity of 93.2(2)%. The scheme is an essential building block in a broad class of stabilizer quantum error correction protocols.
  arXiv  Detail & Related papers  (2021-07-13T20:08:04Z)
• Efficient and robust certification of genuine multipartite entanglement in noisy quantum error correction circuits [58.720142291102135]
  We introduce a conditional witnessing technique to certify genuine multipartite entanglement (GME) We prove that the detection of entanglement in a linear number of bipartitions by a number of measurements scales linearly, suffices to certify GME. We apply our method to the noisy readout of stabilizer operators of the distance-three topological color code and its flag-based fault-tolerant version.
  arXiv  Detail & Related papers  (2020-10-06T18:00:07Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.