AI 中文总结
本文针对量子计算中辅助量子比特反计算仅覆盖清洁类型的问题，提出清洁与脏辅助量子比特反计算的统一形式化及两种方法，在Qiskit中实现原型，较Reqomp提升了多场景覆盖率。
AI 中文摘要
自动反计算旨在提供编程语言级别的支持，以促进量子计算中辅助量子比特的正确且安全使用，但现有工作仅针对清洁辅助量子比特，未涉及脏辅助量子比特。本文对清洁与脏辅助量子比特的反计算进行了统一形式化，首次证明反计算存在性检查问题是coNP难的。我们提出两种互补的面向综合的存在性检查方法：基于重写的归一化算法（RwUn）和基于模板的推理系统（TpUn），后者通过结构化存储-使用模式保证反计算。我们在Qiskit和Python中实现了两种方法的原型。与最先进的Reqomp相比，RwUn在实际复杂依赖基准上达到100%覆盖率，在随机经典电路上的覆盖率是其两倍，在现有方法未覆盖的随机量子电路上约为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 rewrite-based normalization algorithm (RwUn) and a template-based reasoning system (TpUn) that guarantees uncomputation through structured Store-Use patterns. We implement prototypes of both methods in Qiskit and Python. Compared to the state-of-the-art Reqomp~\cite{reqomp}, RwUn achieves 100% coverage on practical 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.
