Quantum Uncomputation of Clean and Dirty Ancilla Qubits

Quantum programs frequently use ancilla qubits—auxiliary storage—to decompose complex operations and optimize circuit depth. However, these ancillas must be 'uncomputed' (restored to their initial state) before disposal to prevent information loss and ensure correctness. While automated uncomputation exists for clean ancillas (initialized to |0⟩), it has remained largely unexplored for dirty ancillas (initialized to arbitrary, unknown states). This paper addresses the challenge of automatically synthesizing uncomputation for both types of ancillas.

The authors provide a unified formalization of uncomputation for clean and dirty ancillas. They prove that determining whether a valid uncomputation exists for a given circuit is coNP-hard. To overcome this, they propose a two-tiered synthesis pipeline:

1. Static Reasoning: A syntax-directed system that acts as a lightweight filter to verify programs and guarantee synthesis for common patterns, such as toggle-detection.
2. Rewrite-based Normalization (RwUn): A more robust procedure that uses local rewrite rules to push ancilla-modifying operations toward the end of the circuit, transforming it into a 'normal form' where uncomputation is straightforward to derive.

The authors implemented their approach as a Qiskit plugin and evaluated it against Reqomp, the current state-of-the-art. Their method achieved 100% success on 17 practical benchmarks with complex dependencies, compared to 10/17 for Reqomp. Furthermore, the approach successfully handled random quantum circuits containing Z, S, and T gates—a category previously unsupported by automated tools—demonstrating that their normalization technique is significantly more versatile than existing dependency-tracking methods.