Borrowing Dirty Qubits in Quantum Programs

Qubits are painfully scarce on today's quantum computers, so a valuable trick is to briefly borrow a qubit that some other part of the program is not currently using — a "dirty" qubit in an unknown state — do work with it, and hand it back exactly as it was; but proving you handed it back untouched is subtler than it looks, because the naive check that works for a fresh qubit silently misses failures involving superposition and entanglement; this paper (Tsinghua, Chinese Academy of Sciences, UTS) gives the first proper formal meaning of dirty-qubit borrowing in a programming language, a correct definition of returning it safely, and an algorithm that verifies it by reducing the question to ordinary logic solvers, scaling to thousands of qubits.

The argument in one glance

Problem

Qubits are scarce, so it pays to borrow ones already in use — but you must return them untouched

Today's quantum computers have very few usable qubits and can run only shallow circuits, so qubits are a precious resource a program must conserve. A powerful way to save them is to borrow ancillary qubits from idle parts of the computation rather than demanding fresh ones. These borrowed qubits are "dirty": they start in some arbitrary, unknown, possibly entangled state, because they belong to another part of the program. Their appeal is flexibility — since the computation is not supposed to care what state they start in, you can grab any idle qubit anywhere as a temporary helper, which is often cheaper than allocating clean qubits initialized to a known state. But borrowing comes with a strict contract. First, the work you do must not depend on the dirty qubit's unknown initial state, or your result is garbage. Second, and harder, you must give the qubit back exactly as you found it — restoring its original state, including any entanglement it shared with other qubits — before releasing it. This restoration is called safe uncomputation, and getting it right is what makes borrowing valid.
What people did

Check safe uncomputation the way you would for a clean qubit

For an ordinary clean ancilla, uncomputation just means returning it to its known ground state, and for a circuit that computes a classical function you can verify this by checking every classical input: run the circuit on each combination of zeros and ones and confirm the ancilla comes back to the value it started with. The natural instinct is to define safe uncomputation of a dirty qubit the same way — require that if it started as a zero it ends as a zero, and if it started as a one it ends as a one, for every classical input.
Why it fell short

The classical check silently misses superposition and entanglement failures

That classical-basis check is correct for clean qubits but dangerously insufficient for dirty ones, and the paper shows this with an elementary circuit. There exists a circuit that passes the naive test — it does return the borrowed qubit to a zero when it started as a zero and to a one when it started as a one — yet fails to restore that same qubit when it was initialized in a superposition, an equal mix of zero and one. Because a dirty qubit borrowed from a running computation can be in exactly such a superposition, or entangled with other qubits, a definition that only checks the two classical basis states declares this corruption safe when it is not. So even for the simplest circuits, safely uncomputing a dirty qubit demands a genuinely quantum criterion that accounts for superposition and entanglement, not the classical one that works for clean qubits. And beyond the definition, borrowing had not even been given a proper meaning as a programming-language feature, so unsafe uses could not be described, let alone caught.
This paper's idea

Define borrowing formally, define safe uncomputation as "leaving the qubit untouched," and verify it

This paper puts dirty-qubit borrowing on a rigorous footing. It extends a core quantum programming language with a primitive to borrow and release a dirty qubit in a matched pair, and gives it a formal semantics that captures every possible behavior of borrowing — including the unsafe ones — so they can be reasoned about. It then defines safe uncomputation cleanly: a program safely uncomputes a borrowed qubit exactly when all of its executions are indistinguishable from operations that leave that qubit untouched, as if the gates had acted only on the other qubits and the borrowed one were an idle wire. This definition correctly handles superposition and entanglement. Finally, it gives an efficient verification algorithm: for the broad class of circuits computing classical functions, checking safe uncomputation reduces to restoring just two specific initial states, turning the quantum question into an ordinary logic-satisfiability problem that off-the-shelf solvers verify for circuits with thousands of qubits.

Why this problem is worth solving

Borrowing is one of the few ways to stretch a tiny qubit budget, and its whole validity rests on returning the qubit perfectly.

Ancillary qubits are helper qubits that let a circuit reduce its size or depth. A clean ancilla starts in a known state, usually the ground state, and stores intermediate results; a dirty ancilla starts in an arbitrary, possibly entangled state and is borrowed from an idle part of the computation. Dirty qubits are attractive because their initial state is not supposed to matter, so they can be borrowed from anywhere idle, giving great scheduling flexibility and letting a program reuse qubits rather than pay for scarce clean ones — a real saving when hardware offers only a handful of qubits. Correct use rests on two requirements. The computation must be independent of the dirty qubit’s initial state, achievable through an established technique for propagating information regardless of a qubit’s starting value. And the computation must safely uncompute the qubit before releasing it: restore it, together with any entanglement it holds with other qubits, to precisely its original state. This is strictly harder than uncomputing a clean qubit, which need only be returned to the ground state. A clean qubit began in one known state; a dirty qubit could have begun in any state at all, including a superposition or one half of an entangled pair, and safe uncomputation must return it faithfully for every such possibility, not just the ones you can enumerate classically.

The subtlety is that the obvious correctness check is wrong, in a way that hides real bugs.

Many circuits that use dirty qubits, such as constant adders and multi-controlled gates, compute classical functions: they are built from NOT and multi-controlled-NOT gates and permute the basis states. For such a circuit it is tempting to verify uncomputation by treating it as a classical function and checking all combinations of zeros and ones as inputs, requiring the borrowed qubit to come back to whatever classical value it started with. That check is sound for clean qubits. But the paper exhibits an elementary circuit that passes it and still fails to restore a dirty qubit initialized in a superposition of zero and one — the circuit preserves the two classical basis states individually yet corrupts their quantum combination, for instance by attaching a wrong relative phase or by leaving residual entanglement. Since a borrowed qubit taken from a live computation is exactly the kind of qubit that may be in superposition or entangled, this false negative is not a corner case; it is the common case that the classical definition cannot see. Safe uncomputation of dirty qubits therefore cannot be reduced to classical input-output behavior, and needs a definition grounded in the full quantum semantics — which is what makes even defining the property, before verifying it, a genuine research problem.

What people did before, and where it broke

Use dirty qubits in circuit design, assuming safe uncomputation. Prior work on gates, arithmetic, and cryptography borrows dirty qubits and presumes they are returned correctly. Where it broke. It assumes safe uncomputation rather than defining or checking it, so unsafe uses cannot be described or detected at the program level.
Treat dirty-qubit uncomputation like clean-qubit uncomputation. Require the borrowed qubit to return to its starting classical value on every classical input. Where it broke. This is sound only for clean qubits; it passes circuits that corrupt a qubit initialized in a superposition or entangled state, missing real failures.
Rely on language support for borrowing where it exists. A few languages, notably one industrial quantum language, offer a borrow keyword. Where it broke. Borrowing had not been given a full formal semantics capturing its complete range of behaviors, including unsafe ones, so there was no rigorous basis for reasoning about or verifying it.
The gap. No work formally defined the semantics of dirty-qubit borrowing as a language feature, gave a correct quantum definition of safe uncomputation, and provided a scalable way to verify it. Doing all three is what this paper contributes.

How the approach works

From a language primitive to a scalable safety check

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Give borrowing a precise meaning that admits it can go wrong. The paper’s first move is to stop treating dirty-qubit borrowing as an informal circuit-design convenience that is simply assumed to work, and instead make it a first-class language construct with a formal semantics. It extends a core quantum programming language with a matched borrow-and-release pair, and interprets programs as sets of quantum operations so that the meaning of a borrow captures every behavior it can exhibit in practice — crucially including the unsafe ones, where the qubit is not returned faithfully. Only once unsafe borrowing has a well-defined meaning can it be reasoned about and ruled out. Pinning down the exact formal semantics of a quantum program so that its properties can be stated and checked rigorously, including the ways it can misbehave, is the same foundational commitment the work on verification of nondeterministic quantum programs covered elsewhere on this site makes, treating a formal semantics as the prerequisite for any trustworthy claim about quantum code.

Define safety as indistinguishability from doing nothing to the qubit. The conceptual heart is the definition of safe uncomputation itself. Rather than the flawed classical check, the paper defines a program to safely uncompute a borrowed qubit exactly when all of its executions are indistinguishable from quantum operations that leave that qubit untouched — the intuition that a safe use can be rewritten into an equivalent circuit in which the gates act only on the other qubits and the borrowed qubit is a bare idle wire. Because this equivalence must hold as full quantum operations, not just on classical inputs, it automatically demands that superposition and entanglement be preserved, catching exactly the failures the naive definition misses. Certifying that a piece of a circuit is genuinely equivalent to a simpler one that omits certain activity, as a formally-grounded equivalence rather than a hopeful transformation, is the same rewriting-by-proof discipline the work on formally-verified dataflow circuit rewrites covered elsewhere on this site relies on, where a rewrite is legitimate only when it is proven to leave behavior unchanged.

Collapse the quantum check into two states and hand it to a logic solver. The final move makes the correct definition practical. Verifying indistinguishability over all quantum inputs sounds intractable, but the paper proves it needs only finitely many cases in general, and for the large class of circuits that compute classical functions — the NOT and multi-controlled-NOT circuits where dirty qubits are most used — it collapses to checking the restoration of just two carefully chosen initial states. That reduction turns a quantum-verification problem into an ordinary Boolean satisfiability problem: each qubit’s outcome becomes a logical formula of the inputs, and the safety condition becomes a satisfiability query dispatched to mature solvers, verifying circuits with thousands of qubits. Recasting a hard quantum question as a classical satisfiability problem to be discharged by powerful off-the-shelf SAT and SMT solvers is the same leverage the work on optimal compilation for fermion-to-qubit encoding covered elsewhere on this site exploits, turning a quantum design problem into constraints a solver can settle.

Following a borrowed qubit through the verification

Checking that a circuit returns a borrowed qubit untouched

A trace, following the paper's approach, of how safe uncomputation of a dirty qubit is defined and verified, using a classical-function circuit like a constant adder.

Step 1 of 5

A program borrows an idle qubit as a dirty ancilla

A subprogram needs a scratch qubit and, rather than allocating a scarce clean one, borrows an idle qubit from elsewhere in the computation with a matched borrow-and-release construct. That qubit is in an unknown, possibly entangled state.

The language chooses the borrowed qubit nondeterministically from the qubits left idle by the program structure.

Why it works

A borrowed qubit can be in a superposition, so the check must be quantum. A dirty qubit taken from a live computation may hold a superposition or entanglement → but the classical-basis check only tests the two definite values and misses corruption of their combination → so a correct definition must demand indistinguishability as a full quantum operation, which the paper’s criterion does.
Equivalence to an idle wire captures exactly the right property. Safe uncomputation intuitively means the borrowed qubit ends as it began → but defining that as indistinguishability from operations that leave the qubit untouched makes it precise → so superposition and entanglement preservation follow automatically rather than needing separate ad-hoc conditions.
A formal semantics for unsafe borrowing lets bugs be named. You cannot rule out a behavior you cannot express → but interpreting borrowing as sets of quantum operations, including unsafe ones, gives every misuse a meaning → so unsafe uncomputation becomes a checkable property rather than undefined behavior.
Finiteness makes an infinite check decidable. There are infinitely many possible quantum initial states to preserve → but the paper proves only finitely many input-output cases need testing for a finite-dimensional program → so the property is decidable rather than requiring exhaustive quantum simulation.
Two states plus a solver make it scale. Even finitely many cases could be many → but for classical-function circuits the check collapses to two specific initial states and becomes a Boolean satisfiability query → so mature SAT and SMT solvers verify circuits with thousands of qubits, which naive quantum reasoning could not.

What it costs (trade-offs and scope)

The efficient reduction is for classical-function circuits. The two-state shortcut, and the reduction to Boolean satisfiability, apply to circuits built from NOT and multi-controlled-NOT gates; these are broad and cover most dirty-qubit uses like adders and multi-controlled gates, but a general finite-dimensional quantum program falls back on the finite-input-output check rather than the two-state solver route.
It verifies, rather than synthesizes, safe uncomputation. The contribution is a definition and a checker: given a program, it decides whether the borrowed qubit is safely returned. It does not automatically make an unsafe program safe or choose the optimal qubit to borrow; the semantics is designed to expose unsafe uses so they can be caught.
Scalability rests on external solvers. The check is discharged by state-of-the-art SAT and SMT solvers, so its practical limits are those of the solvers, and different solvers behave differently across circuit families — one may handle adders better and another multi-controlled circuits.
The first correctness requirement is prior work. Making a computation independent of the borrowed qubit’s initial state uses an established technique; this paper’s focus is the second requirement, defining and verifying safe uncomputation, so the two together are what make borrowing valid.
It is a semantics-and-verification result, not a hardware speedup. The payoff is correctness assurance that enables trustworthy qubit reuse on scarce hardware, not a direct performance gain; its value is realized when programs that borrow dirty qubits can be certified rather than merely assumed correct.

The evaluation

Checking safe uncomputation of a dirty qubit

Property	Assume it is safe	Classical-basis check
Catches superposition or entanglement corruption
Handles unsafe borrowing formally
Decidable in general	n/a
Verification method	None
Scale reached	n/a	n/a

From the paper. The naive classical-basis check is unsound for dirty qubits, passing circuits that corrupt superposition or entanglement. The paper's criterion — indistinguishability from leaving the qubit untouched — is correct, is decidable in finitely many cases for finite-dimensional programs, and for classical-function circuits reduces to checking two initial states as a Boolean satisfiability problem, which state-of-the-art solvers verify for constant adders with hundreds of qubits and multi-controlled-NOT circuits with thousands.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

The contribution is foundational rather than a device or speedup: the first formal semantics of dirty-qubit borrowing as a programming-language feature, a correct definition of safely returning a borrowed qubit, and a scalable way to verify it. The key insight is that the natural classical check — restoring the zero and one values — is unsound for dirty qubits, because a borrowed qubit may be in a superposition or entangled, so safety must mean indistinguishability from leaving the qubit untouched, a full quantum-operation equivalence. The paper then makes this checkable, proving verification needs only finitely many cases and, for the important class of classical-function circuits, collapses to two initial states and an ordinary satisfiability query that mature solvers settle for thousands of qubits. Read it within scope. The efficient two-state-plus-solver route is for circuits built from NOT and multi-controlled-NOT gates; general programs use the broader finite check. It verifies rather than synthesizes safe uncomputation, its scalability inherits the strengths and quirks of external solvers, and the initial-state-independence requirement relies on prior work. Within those bounds it turns a subtle, error-prone practice into something with a precise meaning and a practical correctness guarantee.

Background

Why saving qubits demands this kind of rigor

It helps to see why a formal-methods paper belongs in the story of making quantum computers useful. The defining constraint of current quantum hardware is scarcity: only a small number of usable qubits, and only shallow circuits before noise overwhelms the computation. Every technique that squeezes a bigger computation into fewer qubits is therefore precious, and reusing qubits — computing something into an ancilla, then cleaning it up so it can serve again — is one of the most important. But qubit reuse is treacherous in a way classical memory reuse is not, because a quantum state cannot simply be overwritten; it must be carefully uncomputed, and any residue of superposition or entanglement left behind silently corrupts the rest of the computation. The stakes of getting reuse exactly right are what make a rigorous, checkable account of it valuable, not merely elegant. Shrinking a quantum computation’s qubit footprint by reusing qubits across a circuit is the same resource-saving goal the work on compiler-assisted qubit reuse through dynamic circuits covered elsewhere on this site pursues, and this paper supplies the missing formal guarantee that such reuse is actually correct — so that borrowing a dirty qubit, one of the cheapest ways to save the scarcest resource in computing, can be trusted rather than hoped.

If you remember only three things

1. Dirty qubits let a quantum program reuse idle qubits instead of demanding scarce fresh clean ones, but correct use requires that the computation not depend on the borrowed qubit's unknown initial state and that it restore that state exactly — including any entanglement — before releasing it, a property called safe uncomputation that is strictly harder than uncomputing a clean qubit, which need only return to the ground state.
2. The paper shows the natural correctness check is unsound: for a circuit computing a classical function, verifying that the borrowed qubit returns to its starting value on every classical (zero or one) input passes circuits that nonetheless corrupt a qubit initialized in a superposition or entangled state, so safe uncomputation needs a genuinely quantum definition — the paper extends a core quantum language with a formal borrow-and-release primitive whose semantics captures all behaviors including unsafe ones, and defines a program to safely uncompute a borrowed qubit exactly when all its executions are indistinguishable from operations that leave that qubit untouched, an idle-wire equivalence that automatically preserves superposition and entanglement.
3. It makes this checkable at scale: for any finite-dimensional program, verifying the property needs only finitely many input-output cases, and for the broad class of circuits built from NOT and multi-controlled-NOT gates it reduces to checking the restoration of just two specific initial states, turning the quantum question into a Boolean satisfiability problem that state-of-the-art SAT and SMT solvers (such as CVC5 and Bitwuzla) verify for constant adders with hundreds of qubits and multi-controlled-NOT circuits with thousands; the approach verifies rather than synthesizes safe uncomputation, the efficient route targets classical-function circuits, and its scalability rests on external solvers.

Check yourself

Check your understanding

1. What is a dirty qubit, and why is returning it correctly harder than for a clean qubit?
2. Why is the natural classical check for uncomputation unsound for dirty qubits?
3. How does the paper define safe uncomputation, and why is that definition correct?
4. How does the paper make verifying this quantum property practical, and how far does it scale?

Sources

The paper is “Borrowing Dirty Qubits in Quantum Programs” by Bonan Su, Li Zhou, Yuan Feng, and Mingsheng Ying (Tsinghua University; the Institute of Software, Chinese Academy of Sciences; and the University of Technology Sydney), published at ASPLOS 2026, DOI 10.1145/3779212.3790134. It is released under a Creative Commons Attribution license.

This explainer is written from the full text of the authors’ arXiv version (arXiv:2508.17190). Everything above comes from the paper’s own sections: the introduction on the scarcity of qubits in the current noisy intermediate-scale era and the motivation for conserving them; clean versus dirty ancillary qubits, the appeal of dirty qubits’ scheduling flexibility (with the summary of constant-addition circuit costs adapted from prior work), and the two requirements for correct use — independence from the initial state via the toggling trick, and safe uncomputation, which for dirty qubits must restore the original state including entanglement, a stricter condition than for clean qubits; the illustrative three-controlled-NOT circuit realized with four Toffoli gates and one dirty qubit, and the counterexample showing that a circuit can satisfy the classical-basis restoration condition yet fail to restore a dirty qubit initialized in the equal superposition, establishing that the naive definition is unsound; the paper’s contributions — extending the core quantum programming language QWhile with a matched borrow-and-release construct (QBorrow) whose denotational semantics interprets programs as sets of quantum operations and captures the full range of borrowing behaviors including unsafe ones, with nondeterministic selection of the borrowed qubit and support for measurement-guarded branching and looping using partial density operators; the definition of safe uncomputation as all executions being indistinguishable from operations acting as the identity on the borrowed qubit, understood as rewriting the circuit so the dirty qubit is an idle wire; and the verification results proving that for a finite-dimensional program only finitely many input-output cases must be checked, that for circuits implementing classical functions (built from NOT and multi-controlled-NOT gates) verification reduces to two specific initial states and thence to a Boolean satisfiability problem, and that using state-of-the-art SMT and SAT solvers (CVC5 and Bitwuzla) the approach verifies safe uncomputation for constant adders with hundreds of qubits and multi-controlled-NOT circuits with thousands.