{"id":"0b2c5924-4698-4d76-a27e-94ca12d44795","arxiv_id":"2608.09578","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"Quantum compilers can now automatically uncompute dirty ancillas with a rewrite-based normalizer, and the existence problem is coNP-hard.","lead":"A new framework lets quantum compilers automatically uncompute both clean and dirty ancilla qubits, proving the existence problem is coNP-hard. The rewrite-based tool RwUn succeeds on more benchmark circuits than the previous state of the art Reqomp, including phase-gate circuits beyond Reqomp's scope.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The coNP-hardness reduction appears sound, but the empirical claims of 100%/2x/50% coverage rest on unreleased code and a single-seed SAT filter; they cannot be verified as stated.","rationale":"I read the paper in good faith. The formal framework is coherent: Proposition 3.1 correctly ties func validity to clean and dirty uncomputation; the R-kRBF reduction is coNP-complete with a polynomial certificate; and the rewrite rules (R-1)-(R-3) are algebraically sound. The reader's Lemma 3.1 concern seems resolvable, because the negatively controlled Fredkin construction uses X gates on a control line that is disjoint from the five ancilla bits and is restored, so no sixth ancilla is needed. The genuine soft spot is evidential: the headline experimental numbers are not reproducible from the manuscript because artifacts are withheld, the SAT filter is unspecified, and the random benchmarks are single-seed. This does not refute the theory, but it prevents full acceptance of the stronger practical claim; the existing CONDITIONAL verdict is appropriate. I would not adjust the verdict, hence UNCHANGED.","tokens_in":57681,"tokens_out":32745,"duration_ms":334057,"concrete_test":"Release the supplementary artifact and run an independent reproducibility pass: for each width/gate-count batch in Benchmark 2 (small/medium/large), resample 100 uncomputable circuits with seeds 0-9 using a named SAT solver (e.g., PySAT Glucose 4) and verify each selected circuit with an independent truth-table check at small sizes; then recompute RwUn vs Reqomp success rates. Also rerun Benchmark 1 with the exact parameter list from Table 2 and the same 30s budget. If the 2x, ~50%, and 100% coverage figures do not reproduce across seeds or the SAT filter is not certified, the practical central claim should be downgraded.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The core complexity argument is in better shape than the reader's weakest-assumption line suggests. Corollary D.1's negatively controlled Fredkin construction is sound: for a triple (i, alpha, 1), surrounding the control line with two X gates before/after the Fredkin decomposition flips the control only during the gate and restores it; since the control is an input bit disjoint from the five ancilla bits, no sixth ancilla is required. The Barrington/Jordan reduction to a controlled-SWAP on n+5 qubits therefore goes through, and Theorem 3.1 stands. The load-bearing weakness is instead the empirical support for the paper's practical claim. Section 7 reports success-rate comparisons against Reqomp (100% on 17 hand-picked benchmarks, about 2x on random qfree circuits, ~50% on random quantum circuits) using an implementation that is not released, a single seed (42), and a benchmark filter that invokes an unnamed SAT solver. Benchmark 3 is not filtered for uncomputability at all. Without the artifact, the reader cannot distinguish a real advantage from a solver/encoding quirk or a bug in the filter. The coNP-completeness result is unaffected, but the central 'broader applicability' claim is not yet independently checkable.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a unified framework for automatic uncomputation of clean and dirty ancilla qubits in quantum circuits. It formalizes when the functionality of a circuit is valid, proves that deciding uncomputation existence is coNP-hard for reversible Boolean circuits over CCNOT and X gates, and presents two synthesis-oriented existence checkers: a template-based static reasoning system (TpUn) and a rewrite-based normalization procedure (RwUn). The experimental section reports that RwUn outperforms the state-of-the-art Reqomp on practical and random benchmarks, claiming 100% coverage on 17 practical cases, roughly double the success rate on random qfree circuits, and about 50% success on random quantum circuits outside Reqomp's scope.","tokens_in":57874,"tokens_out":19353,"duration_ms":193974,"significance":"If the results are correct and the implementation is available, this is a useful step for quantum programming-language support: it gives the first coNP-hardness result for the uncomputation existence problem, unifies clean and dirty ancilla semantics, and provides a concrete synthesis pipeline with normal forms. The coNP-hardness reduction is detailed and appears substantially correct, and the rewrite rules are accompanied by nontrivial semantic proofs. The paper also gives a sufficient syntactic criterion (absence of aw-cycles) for RwUn to succeed, which is a valuable practical insight. However, the termination proof of the central normalization algorithm is not fully established as written, and the empirical claims are currently not independently verifiable because the artifact, benchmark code, and details of the filtering procedure are not provided.","major_comments":[{"comment":"The termination proof of Algorithm 1 is incomplete. Lemma D.2 only treats circuits that contain exactly one violating pair and where that pair is at the end of the circuit. The step from this special case to termination for arbitrary circuits is asserted in the preamble of Appendix D.13 ('the global execution can be decomposed into a sequence of local subproblems') but no formal measure or inductive argument is given. Since termination is part of Theorem 6.1 and is a precondition for the synthesis theorem (Theorem 6.2) and for the experimental success claims, this gap is load-bearing. Please provide a complete termination proof or a revised statement that makes the termination assumption explicit.","section":"Section 6.3, Theorem 6.1; Appendix D.13, Lemma D.2"},{"comment":"The central practical claims are not reproducible from the manuscript. The implementation is not released, the random benchmarks use a single seed (42), the SAT filter used to select 'uncomputable' qfree circuits is not named, and Benchmark 3 is deliberately not filtered for uncomputability. Consequently, the reported 100% / 2x / 50% success rates could be affected by the particular seed, by the SAT solver's encoding, or by the unknown fraction of uncomputable circuits in Benchmark 3. Please release the artifact and benchmarks, report results over multiple seeds, and describe the SAT filter precisely; alternatively, substantially weaken the empirical claims to clearly verified case studies.","section":"Section 7, Benchmarks 2 and 3; Data-Availability Statement"},{"comment":"The proof that every uncomputable qfree circuit has a semantically equivalent circuit satisfying condition (2) of Proposition 6.1 is not self-contained. It invokes the canonical form of [Feng and Li 2025] and asserts that MPMCX gates in the 'head part' whose target is an ancilla can be implemented using only MCX gates controlled by another ancilla, but the required construction is not shown. This is a key characterization result for the normal-form approach, so the proof should either spell out the construction or give a precise reference to a theorem that does.","section":"Appendix D.9, proof of Proposition 6.1"}],"minor_comments":[{"comment":"The heading 'Normal form of quantum circutis' contains a typo; it should read 'circuits'.","section":"Section 6.2, heading"},{"comment":"The displayed definitions of uncomputation read as if the uncomputation operator G_a is applied directly to the original input, rather than after the compute circuit G. Consider clarifying that G_a denotes the full uncomputed circuit (or state explicitly whether it is post-composed with G), since this affects the reading of Proposition 3.1.","section":"Section 3.1, Definitions 3.2 and 3.3"},{"comment":"The text immediately below the circuit diagram says '4 Qubits c,d,e remain unchanged' but only three qubits c,d,e are listed; please fix the numbering or the list.","section":"Theorem 3.1 proof diagram"},{"comment":"There are minor typos such as 'simliar' and 'fixed function' used where 'fixed-input function' or similar is meant; a proofreading pass is needed.","section":"Appendix D.7.4 and D.10"},{"comment":"The Aw-Dep metric depends on a depth bound L=10 and on the cycle-gated source collection heuristic; the paper should state whether the reported conclusions are sensitive to L and to the choice of the bound.","section":"Section 7.1, Aw-Dep definition"}],"recommendation":"major_revision","confidential_remarks":"The theoretical core of the paper is plausible and the coNP-hardness part appears in good shape, but the termination proof and the empirical reproducibility are the two points that decide whether the practical claims can be trusted. I would advise the editor to require a full termination proof and an artifact (or a clearly weakened empirical section) before acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: I think the paper has a solid theoretical core and a genuinely new complexity result. The coNP-completeness of uncomputation for reversible Boolean circuits (Cor 3.1) goes through. I checked the disputed Lemma 3.1 construction: the two-X-gate trick for negatively controlled Fredkin gates works because the control is an input bit disjoint from the five ancilla bits, so no sixth ancilla is needed. The reduction from SAT via Jordan/Barrington is sound. Proposition 3.1 unifying clean/dirty existence is clean and correct. This is a real contribution.\n\nThe rewrite-based normalizer RwUn is the practical engine. The rules (R-1)-(R-3) are semantically justified; the termination argument in Lemma D.2 is intricate but I did not find an actual gap. It is not machine-checked, so I would not bet the farm on it, but it is plausible. The normal form is sufficient not necessary for quantum circuits, and the paper says so. TpUn is a reasonable syntax-directed filter, though the CQBF rules are heavy. The benchmark table shows RwUn scales better than Reqomp on many cases and handles phase gates that Reqomp cannot.\n\nSoft spots are mostly evidential. No code or data are released, the SAT-based filter in Benchmark 2 uses an unnamed solver and a single seed, and Benchmark 3 is not filtered for uncomputability at all, so the ~50% success rate there has no clear denominator. The 100% on 17 hand-picked benchmarks is suggestive but not independently checkable. Aw-Dep is purpose-built to explain RwUn's behavior; it is not fitted, but it is also not independently validated. None of these undermine the coNP result, but they do mean the broader applicability claim is not yet verifiable.\n\nWho should read it: people working on quantum circuit compilation, especially uncomputation and ancilla management. It deserves a serious referee. I would send it to review and require artifact release before final acceptance.","headline":"The coNP-hardness result is real and the rewrite system is worth engaging; the empirical coverage claims cannot be independently checked until the artifact is released.","tokens_in":58462,"tokens_out":1652,"would_cite":true,"duration_ms":17464,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q12","68Q17","81P68"],"pacs":[],"model":"deepseek-v4-flash","headline":"Deciding whether an ancilla can be uncomputed is coNP-complete for reversible Boolean circuits, yet rewrite-based normalization and template reasoning synthesize uncomputation for far more circuits than prior tools.","keywords":["quantum uncomputation","dirty ancilla","clean ancilla","coNP-completeness","reversible Boolean circuits","rewrite-based normalization","static reasoning","ancilla synthesis"],"falsifier":"Build the controlled-SWAP circuit of Lemma 3.1 for a small satisfiable CNF and a small unsatisfiable CNF, and check on all inputs whether the swap fires exactly when the formula is true; if the n+5-qubit construction silently needs a sixth qubit preset to a known state, the reduction fails. A direct check of the hardness chain: for an unsatisfiable formula the 1-fixed reversible function must equal the identity, so any observed collision on the remaining inputs would falsify the claimed equivalence.","tokens_in":57426,"feed_emoji":"⚛️","tokens_out":11966,"duration_ms":100652,"temperature":0.7,"pith_summary":"This paper gives a unified treatment of uncomputation for clean ancillas (initialized in |0>) and dirty ancillas (initialized in an unknown state), showing that in both cases the ancilla must be restored to the same state it started in, and that existence of such an operation is exactly the same decision problem. The central hardness claim is that for polynomial-size reversible Boolean circuits built from CCNOT and X gates, deciding whether uncomputation exists is coNP-complete, proved by reducing SAT to the question of whether a reversible Boolean function stays reversible after some inputs are fixed to 0. On the constructive side, the paper shows that uncomputation is guaranteed and regularly synthesizable whenever a circuit can be rewritten into a prefix-suffix normal form in which all ancilla-modifying gates sit at the tail; two systems, a template-based static checker and a rewrite-based normalizer, exploit this structure. The rewrite-based method succeeds on all 17 practical complex-dependency benchmarks, solves roughly twice as many random reversible circuits as the previous baseline, and handles about half of random quantum circuits that use phase gates. If correct, the paper makes automatic uncomputation of both clean and dirty ancillas a realistic compiler front-end problem.","feed_headline":"Deciding if an ancilla can be uncomputed is coNP-hard","feed_subtitle":"A rewrite-based tool can still uncompute clean and dirty ancillas on all 17 practical benchmarks.","key_machinery":"Two objects carry the argument. The first is the k-fixed reversible Boolean function f|_k, obtained by fixing k input bits of a reversible Boolean function to 0 and deleting the same outputs; deciding whether f|_k is reversible is exactly the uncomputation problem for qfree circuits, and the coNP-completeness proof reduces SAT to it via a controlled-SWAP gate built from a CNF formula on n+5 qubits. The second is the prefix-suffix normal form: a circuit is in normal form with respect to an ancilla when every gate that modifies the ancilla has only ancilla-modifying gates to its right, so the circuit splits into a working-qubit prefix that implements the functionality and an ancilla tail that can be inverted. The rewrite rules (R-1) to (R-6) push ancilla-modifying gates rightward, inserting compensating gates when a naive swap would change the semantics, and the no-aw-cycle condition on the circuit graph guarantees the rules never get stuck for qfree circuits. The static template system uses const, qfree, and CQBF properties of store-use and toggle-detection patterns to certify uncomputability and produce regular synthesis.","core_discovery":"The paper's central claim is that uncomputation existence is a single unified problem for clean and dirty ancillas, and that for reversible Boolean circuits of polynomial gate size this problem is coNP-complete. The reduction goes through the k-fixed reversible Boolean function: fix k input positions to 0, discard the corresponding outputs, and ask whether the remaining function is a bijection; uncomputation exists exactly when it is. The paper proves coNP-hardness by reducing SAT to non-reversibility of the 1-fixed function, using a polynomial-time construction of a CCNOT-and-X circuit implementing a controlled-SWAP conditioned on a CNF formula over n+5 qubits. On the constructive side, it proves that a qfree circuit is uncomputable if and only if it has a semantically equivalent prefix-suffix normal form, where the prefix acts on working qubits and the suffix modifies only ancillas; for general quantum circuits the normal form is a sufficient condition. Two synthesis-oriented existence checkers, the template-based static system TpUn and the rewrite-based normalizer RwUn, certify this normal form in different regimes and synthesize an uncomputation by inverting the ancilla tail. Empirically, the paper claims RwUn correctly uncomputes all 17 practical benchmarks with complex dependencies, about twice as many random reversible circuits as the baseline, and about half of random quantum circuits beyond the baseline's scope.","pith_inferences":["The coNP-completeness result suggests that a SAT-based decision procedure for k-fixed reversibility could serve as a complete fallback for the qfree fragment, complementing the incomplete rewrite approach.","Because the paper proves normal-form existence is necessary and sufficient for qfree circuits, complete rewriting systems for reversible circuits could turn uncomputation checking into a reachability problem with a known set of rules.","The store-use/toggle-detection pattern generalizes beyond these benchmarks: it could be exposed as a first-class language construction for dirty ancillas, making the safety argument part of the type system.","The Aw-Dep dependency-complexity metric used in the evaluation may itself be a predictor of synthesis hardness; testing it on a broader circuit corpus could give compiler authors a cheap way to decide when to attempt uncomputation."],"forward_implications":["Compiler-level uncomputation cannot be a complete, fully automatic polynomial-time pass for arbitrary reversible Boolean circuits; it must either accept a restricted fragment or solve a coNP-hard existence problem.","For classical reversible (qfree) circuits, uncomputability is equivalent to reachability of the prefix-suffix normal form, so the no-aw-cycle graph condition gives a structural test and uncomputation then reduces to inverting the tail.","Dirty ancillas can be uncomputed automatically whenever their usage follows the store-use/toggle-detection pattern, and the dirty-ancilla uncomputation is unique when it exists, giving a canonical synthesis target.","The rewrite-based method broadens automatic uncomputation beyond the previous baseline: full success on the 17 practical benchmarks, roughly double the success on random reversible circuits, and partial success on circuits with Z, S, and T gates.","Separating existence checking from synthesis lets a front-end accept a program only when a witness circuit is produced, keeping the back-end focused on optimization."],"supporting_citations":[{"why":"Jordan's construction of controlled-SWAP from a width-5 branching program is the technical bridge that the paper extends from n+6 to n+5 qubits using X gates, yielding the SAT reduction.","marker":"[32]"},{"why":"Barrington's theorem gives width-5 branching programs for log-depth formulas, the starting point of Lemma 3.1.","marker":"[5]"},{"why":"SAT is the NP-complete source problem in the reduction proving R-kRBF and hence uncomputation coNP-hard.","marker":"[11]"},{"why":"Supplies the canonical-form analysis of reversible circuits used to prove the prefix-suffix characterization for qfree circuits.","marker":"[17]"},{"why":"Defines the clean-ancilla uncomputation problem and circuit-graph synthesis method that this paper unifies and extends to dirty ancillas.","marker":"[42]"},{"why":"The previous automatic uncomputation synthesizer used as the baseline in the experimental comparison.","marker":"[43]"},{"why":"Formalizes the safety condition for dirty-qubit usage that the unified dirty-ancilla definition extends.","marker":"[54]"},{"why":"SPARE's rewrite-based treatment of compute-uncompute sequences is the stated inspiration for the normalization procedure.","marker":"[50]"}],"fun_headline_variants":["Ancilla uncomputation existence is coNP-hard—proven","Uncomputing clean and dirty ancillas: coNP-hard to verify","Despite coNP-hard problem, RwUn tool uncomputes all 17 benchmarks","New proof: ancilla uncomputation is coNP-complete for reversible circuits","RwUn: 100% uncomputation on practical benchmarks, beyond cost of proof"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The hardness result depends on the assumption that any CNF formula can be compiled, in polynomial time and using only CCNOT and X gates on n+5 qubits, into a circuit whose controlled swap fires exactly when the formula is satisfiable, with no extra qubit initialized to zero.","fun_headline_variants_meta":{"raw":{"variants":["Ancilla uncomputation existence is coNP-hard—proven","Uncomputing clean and dirty ancillas: coNP-hard to verify","Despite coNP-hard problem, RwUn tool uncomputes all 17 benchmarks","New proof: ancilla uncomputation is coNP-complete for reversible circuits","RwUn: 100% uncomputation on practical benchmarks, beyond cost of proof"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000334,"raw_usage":{"total_tokens":1884,"prompt_tokens":1004,"completion_tokens":880,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":620,"completion_tokens_details":{"reasoning_tokens":776}},"tokens_in":620,"tokens_out":880,"duration_ms":6452,"temperature":1.0,"reasoning_tokens":776,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T14:45:55.022418+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Build the controlled-SWAP circuit of Lemma 3.1 for a small satisfiable CNF and a small unsatisfiable CNF, and check on all inputs whether the swap fires exactly when the formula is true; if the n+5-qubit construction silently needs a sixth qubit preset to a known state, the reduction fails. A direct check of the hardness chain: for an unsatisfiable formula the 1-fixed reversible function must equal the identity, so any observed collision on the remaining inputs would falsify the claimed equivalence.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Jordan's construction of controlled-SWAP from a width-5 branching program is the technical bridge that the paper extends from n+6 to n+5 qubits using X gates, yielding the SAT reduction."},{"cited_title":"M Barrington","cited_arxiv_id":null,"evidence_quote":"Barrington's theorem gives width-5 branching programs for log-depth formulas, the starting point of Lemma 3.1."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the canonical-form analysis of reversible circuits used to prove the prefix-suffix characterization for qfree circuits."}],"review_version":1}