一句话：统一形式化干净与脏辅助比特的逆计算，证明存在性检查为 coNP-hard，并提出与实现合成方法 RwUn。
自动逆计算旨在从编程语言层面支持量子计算中辅助量子比特的正确安全使用，但已有工作仅覆盖干净辅助比特，脏辅助比特仍未被探索。本文首次给出干净与脏辅助比特逆计算的统一形式化，并证明判定逆计算是否存在是 coNP-hard 的。为处理该问题，作者提出两种互补的、面向合成的存在性检查方法：语法导向的静态推理系统与基于重写的归一化过程 RwUn，二者构成自顶向下的流水线。作者在 Qiskit 中实现了 RwUn，并与当前最优的 Reqomp 进行比较。实验表明，RwUn 在复杂依赖基准上达到 100% 覆盖率，在随机经典电路上覆盖率约为 Reqomp 的两倍，在现有方法无法处理的随机量子电路上仍能达到约 50% 覆盖率，展示了更广的适用性。
Automatic uncomputation aims to provide programming-language-level support to facilitate the correct and safe use of ancilla qubits in quantum computing, but efforts have only been made for clean ancillas, leaving dirty ancillas unexplored. We present a unified formalization of the uncomputation of both clean and dirty ancillas. For the first time, we prove that checking the existence of uncomputation is coNP-hard. We introduce two complementary synthesis-oriented existence checking methods: a syntax-directed static reasoning system and a rewrite-based normalization procedure (RwUn), together forming a top-down pipeline. We implement RwUn in Qiskit. Compared to the state-of-the-art Reqomp, RwUn achieves 100% coverage on complex-dependency benchmarks, twice the coverage on random classical circuits, and about 50% coverage on random quantum circuits beyond the scope of existing methods, demonstrating broader applicability.
@article{paperbot12143,
title = {Quantum Uncomputation of Clean and Dirty Ancilla Qubits},
author = {Chenke Liu and Li Zhou and Boning Meng},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839528}
}