{"id":"fdd3a0df-3987-4bbf-bb67-7e0f30fb95d2","arxiv_id":"2508.17190","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper gives QBorrow a formal borrow/release semantics, defines safe uncomputation of a dirty qubit as the program acting as identity on that qubit, and reduces verification for classical circuits to SAT.","lead":"This paper adds a borrow/release construct for dirty qubits to a quantum programming language and defines what it means for a borrowed qubit to be safely uncomputed. It also gives an SAT-based verifier that checks safe uncomputation on constant adders and multi-controlled-NOT circuits with hundreds to thousands of qubits.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 6.1's proof has a false inference: nonzero overlap with |−⟩ does not force ρ_{+i}=ρ_−; the finite-state reduction for general programs is unproven as written, though the classical SAT result may survive.","rationale":"The reader's stated weakest assumption concerns the syntactic idle set and runtime availability of borrowed qubits. That is a modeling concern, but within the paper's own single-program, explicit-lifetime semantics the substitution-based treatment of nested borrows is largely self-consistent. I find a more concrete and load-bearing gap in the proof of Theorem 6.1, which the reader also flagged in the rationale: the (2)⇒(1) direction relies on a false linear-algebra inference about |−⟩⟨−| and on an unjustified conversion from reduced-state conditions to product-output conditions. This matters because Theorem 6.1 is what licenses the paper's general claim that safe uncomputation of arbitrary finite-dimensional QBorrow programs reduces to checking finitely many states. The SAT-based verification of classical X/C^mNOT circuits, which is the main experimental contribution, is proved through Theorems 6.2 and 6.4 and appears sound: formula (6.1) forces the q=0 block into itself, which by bijectivity forces q=1 to q=1, and formula (6.2) forces independence of all other outputs from q; together these imply U=I_q⊗V for a permutation U. Thus the practical result likely survives, and the appropriate verdict remains CONDITIONAL rather than REJECT. The proposed check—expanding |−⟩⟨−| and attempting a Choi-matrix proof—would settle whether Theorem 6.1 is merely missing a fix or is genuinely false; either way the paper needs revision because the current proof does not support the stated theorem.","tokens_in":26869,"tokens_out":32788,"duration_ms":361335,"concrete_test":"Verify the disputed step by computing the expansion of |−⟩⟨−| in the basis {|0⟩⟨0|,|1⟩⟨1|,|+⟩⟨+|,|+i⟩⟨+i|}; the coefficient of |+i⟩⟨+i| is 0, so the overlap argument cannot force ρ+i=ρ−. Then attempt to reprove direction (2)⇒(1) using Choi-matrix/complete-positivity reasoning (the five test states are tomographically complete, so a correct proof should exist if the theorem is true). If the theorem survives, add the missing argument; if not, weaken Theorem 6.1 and remove the 'any finite-dimensional quantum program' claim in Section 6, since the practical SAT result for X/C^mNOT circuits does not depend on it.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 9.4 (proof of Theorem 6.1, direction (2)⇒(1)) is the only justification that safe uncomputation of an arbitrary QBorrow program can be checked on the finite set ℬ of one-qubit states. The proof asserts: 'Observe that |−⟩⟨−| is an operator with non-zero overlap with each of the other four basis operators ... Hence, it follows that ρ0=ρ1=ρ+=ρ+i=ρ−.' This does not follow. Nonzero Hilbert–Schmidt overlap with a basis operator is not the same as having a nonzero coefficient when expanded in that basis. In fact |−⟩⟨−| = |0⟩⟨0|+|1⟩⟨1|−|+⟩⟨+|, so the coefficient of |+i⟩⟨+i| is exactly 0; the condition for |−⟩ only links ρ0, ρ1, ρ+ and says nothing about ρ+i. The proof also silently converts the reduced-state hypothesis E(ρ⊗|ψ⟩⟨ψ|)|q=|ψ⟩⟨ψ| into the product-output conclusion E(ρ⊗|ψ⟩⟨ψ|)=ρψ⊗|ψ⟩⟨ψ|; this second step is true for pure reduced states but is not stated or proven. Consequently the claim that 'verifying the safe uncomputation of a dirty qubit requires checking only a finite number of input–output cases' for all finite-dimensional QBorrow programs is not established by the text. The classical-circuit SAT reduction (Theorems 6.2 and 6.4) is proved separately and may remain correct, but the general finite-case theorem needs repair.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper extends the quantum programming language QWhile with a borrow/release construct for dirty qubits, giving a denotational semantics in which programs denote sets of quantum operations and a borrowed qubit is nondeterministically chosen from a syntactically computed idle set. It defines safe uncomputation of a dirty qubit q as the requirement that every execution act as the identity on q, and it states equivalences with restoration of arbitrary pure states, preservation of external entanglement, and determinism of the program. For verification, the paper claims a general finite-state reduction (Theorem 6.1), and for circuits made of X and multi-controlled NOT gates it reduces safe uncomputation to checking two Boolean formulas (Theorems 6.2 and 6.4). Experiments on constant adders and multi-controlled-NOT circuits show the SAT/SMT-based verifier scaling to hundreds and thousands of qubits, respectively. An artifact appendix provides the QBorrow grammar, benchmark programs, and build instructions.","tokens_in":58,"tokens_out":11461,"duration_ms":521447,"significance":"If the theoretical claims are repaired, this is a useful contribution: it gives the first formal language-level account of dirty-qubit borrowing, a clean definition of safe uncomputation, and an efficient, parameter-free verification method for the practically important class of classical reversible circuits. The SAT reduction is a genuine algorithmic idea, and the reported experiments on adders and MCX circuits support the scalability claim for those families. The paper also ships an artifact with grammar files, benchmark programs, and build instructions, which is a strength. The main risk is not in the classical-circuit fragment but in the general finite-state and entanglement-preservation theorems, whose proofs have gaps.","major_comments":[{"comment":"The step asserting that nonzero Hilbert–Schmidt overlap of |−⟩⟨−| with the basis {|0⟩⟨0|,|1⟩⟨1|,|+⟩⟨+|,|+i⟩⟨+i|} implies ρ0=ρ1=ρ+=ρ+i=ρ− is incorrect. In that basis, |−⟩⟨−| = (|0⟩⟨0|+|1⟩⟨1|−|+⟩⟨+|)/2, so the coefficient of |+i⟩⟨+i| is exactly zero; the |−⟩ input only relates ρ0, ρ1, and ρ+, and gives no constraint on ρ+i. Additionally, the proof silently strengthens the hypothesis: condition (5.1) only asserts preservation of the reduced state on q, whereas the proof writes E(ρ⊗|ψ⟩⟨ψ|)=ρψ⊗|ψ⟩⟨ψ|. For these reasons, condition (2) of Theorem 6.1 is not established as a sufficient criterion, and the general claim that safe uncomputation of arbitrary finite-dimensional QBorrow programs can be checked on the finite set ℬ is unsupported as written.","section":"Section 9.4, proof of Theorem 6.1, direction (2)⇒(1)"},{"comment":"There is a nontrivial gap in deriving the factorization (E_k⊗I)(|i⟩⊗(|00⟩+|11⟩)) = |β_{i,k}⟩⊗(|00⟩+|11⟩) for each Kraus operator E_k. The hypothesis only fixes the partial trace of the sum over k, and it is not automatic that each term individually factorizes in this way; one must argue that a positive sum of rank-one terms with a pure partial trace forces each term's partial trace to be proportional to that same pure state. This is likely repairable, but the proof as written omits the argument.","section":"Section 9.4, proof of Theorem 6.1, direction (3)⇒(1)"},{"comment":"The proof of Theorem 5.4 only gives the forward (⇒) direction and stops at the end of that direction; there is no (⇐) argument. Since the theorem states an equivalence between safe uncomputation and preservation of external entanglement, the converse must either be proved or explicitly derived from Theorem 5.3 or another stated result. As it stands, the entanglement-preservation characterization is unproven.","section":"Section 9.2, proof of Theorem 5.4"}],"minor_comments":[{"comment":"The expression ρ′ ∈ ℬ^{⊗(n−2)} is not defined for n=1 or n=2; the low-dimensional base cases of the statement should be handled explicitly or excluded.","section":"Theorem 6.1, item 3"},{"comment":"The intuitive explanation of condition (6.2) says only that the final states of the other qubits must be independent of the initial value of q; it omits the injectivity argument that also forces the final value of q itself to be toggled, which is needed for the two branches to recombine into |+⟩ rather than into |0⟩. The formulas appear correct, but the accompanying text should make this point.","section":"Section 6.1, formula (6.2)"},{"comment":"The definition of idle(borrow a; S; release a) = idle(S) and the use of substitution S[q/a] deserve a short formal clarification, especially for nested borrows: the reader must verify that a qubit selected for an inner borrow is excluded from the inner body only after substitution, while remaining available for the outer computation after release. The example in Figure 4.4 is helpful but the general definition should state this more explicitly.","section":"Section 4.2 / Figure 4.2"},{"comment":"The sentence in the introduction that the experimental results “provide an affirmative answer to the most pressing research question in quantum verification” is an overstatement; the experiments support scalability for two circuit families, not a general resolution of quantum verification scalability.","section":"Section 6.2, experimental results"}],"recommendation":"major_revision","confidential_remarks":"The paper's most valuable and likely correct component is the SAT-based verification for classical circuits (Theorems 6.2 and 6.4), which is proved independently of the flawed argument in the proof of Theorem 6.1. I would not reject on the basis of the current gaps, because the errors are localized and repair routes exist, in particular through the Bell-state condition in Theorem 6.1(3). The authors should be asked to provide a correct proof of the finite-state reduction and to supply the missing converse of Theorem 5.4 before publication. The artifact and benchmark suite are a positive feature of the submission."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's my read of 2508.17190. The main practical result—the SAT reduction for classical circuits—is real and worth your time. The paper's general theory is not fully proven as written.\n\nWhat's genuinely new: a first formal semantics for dirty-qubit borrow/release in a quantum programming language, the identity-on-the-qubit definition of safe uncomputation, and a reduction of safe-uncomputation verification to checking two Boolean formulas for X/controlled-NOT circuits. Theorems 6.2 and 6.4 are proved independently, with a permutation-matrix argument, and the experiments on adder and MCX circuits are plausible: hundreds to thousands of qubits, scaling as described. That part I trust.\n\nThe soft spot is Theorem 6.1, which underpins the claim that arbitrary finite-dimensional programs reduce to checking five one-qubit states. The proof of (2)=>(1) has a false inference: it says |−⟩⟨−| has nonzero overlap with each of the four basis operators |0⟩⟨0|, |1⟩⟨1|, |+⟩⟨+|, |+i⟩⟨+i|, and concludes ρ0=ρ1=ρ+=ρ+i=ρ−. Nonzero Hilbert–Schmidt overlap is not coefficient. In fact |−⟩⟨−| = |0⟩⟨0|+|1⟩⟨1|−|+⟩⟨+|, so the coefficient of |+i⟩⟨+i| is exactly zero; the |−⟩ condition says nothing about ρ+i. The proof also jumps from a reduced-state condition to a product-output condition without justification. This step can be true for pure reduced states, but it needs an argument. As written, the theorem is unproven. The classical SAT reduction does not depend on Theorem 6.1, so the paper's practical core survives.\n\nSmaller issues: the artifact appendix has an unedited anonymous-submission header mentioning Separation Logic, and the intro's 'most pressing research question' is overblown for two benchmark families. Housekeeping.\n\nNet: an original and useful paper with a genuine gap in one central theorem. I'd guess the gap is repairable, since the classical result is independent, but the authors need to fix the proof or weaken the claim. Send it to peer review; I'd cite the SAT-reduction result. If I were the editor, I'd ask for a revision that addresses Theorem 6.1 before acceptance.","headline":"Original, useful SAT-based verification for dirty qubits in classical circuits, but the general finite-state theorem (6.1) is not proven as written and needs repair before the theory catches up with the claims.","tokens_in":27717,"tokens_out":9622,"would_cite":true,"duration_ms":94665,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q12","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper defines safe uncomputation of dirty qubits in quantum programs and proves that, for circuits made of NOT and multi-controlled NOT gates, safety reduces to two Boolean unsatisfiability checks.","keywords":["dirty qubits","safe uncomputation","quantum programming languages","quantum circuit verification","Boolean satisfiability","qubit reuse","ancilla qubits","denotational semantics"],"falsifier":"Take a classical circuit with a borrowed qubit, such as the five-qubit example in the paper's Figure 1.4, and run the reduction: if a SAT solver reports both formulas (6.1) and (6.2) unsatisfiable while a direct simulation of the circuit on the state $|+\\rangle$ shows that the borrowed qubit's reduced state is changed, the central theorem is false. More generally, brute-force search over small classical circuits can look for a circuit whose two Boolean formulas are both unsatisfiable but whose unitary is not of the form $V\\otimes I_q$.","tokens_in":26538,"feed_emoji":"⚛️","tokens_out":5536,"duration_ms":58187,"temperature":0.7,"pith_summary":"The paper gives quantum programming a formal way to borrow dirty qubits—ancilla qubits that may start in any state, including entangled ones—and to know when a borrow is safe. Safety means the borrowed qubit is returned exactly as found, so that no experiment can tell it was used. For circuits built only from NOT and multi-controlled NOT gates, the paper shows that checking safety reduces to two classical Boolean unsatisfiability questions. The authors implement this reduction and report that it scales to constant adders with hundreds of qubits and multi-controlled NOT circuits with thousands of qubits. If correct, this turns a quantum verification problem into a task for ordinary SAT solvers.","feed_headline":"Safe dirty-qubit reuse reduces to two SAT checks","feed_subtitle":"A new semantics and verifier make sure borrowed qubits are returned intact, scaling to thousands of qubits.","key_machinery":"The central machinery is the denotational semantics of the borrow statement, which nondeterministically selects a qubit from the syntactically computed idle set $\\mathit{idle}(S)$, together with a Boolean-formula tracking scheme for classical circuits. Each qubit $q$ is assigned a Boolean formula $b_q$ updated by the rules for $X$ gates and multi-controlled NOT gates. Formula (6.1) checks that $q$'s final Boolean value implies its initial value, and formula (6.2) checks that when $q$ is in $|+\\rangle$, the outputs of all other qubits are independent of $q$. The paper also proves a finite-state refinement (Theorem 6.1): general safe uncomputation can be verified using only five one-qubit states, and for classical circuits only $|0\\rangle$ and $|+\\rangle$ suffice.","core_discovery":"A QBorrow program $S$ safely uncomputes a qubit $q$ if and only if every quantum operation in its denotational semantics factors as $I_q \\otimes E'$ acting on the other qubits; equivalently, $q$ is restored for any pure input state and its external entanglement is preserved. For circuits implementing classical functions, the paper proves that only two input states need to be checked: $|0\\rangle$ and $|+\\rangle$. Restoration of $|0\\rangle$ becomes the Boolean formula (6.1), and restoration of $|+\\rangle$ becomes formula (6.2), which requires the final state of every other qubit to be independent of $q$'s initial value. Theorem 6.4 states that the circuit safely uncomputes $q$ if and only if both formulas are unsatisfiable.","pith_inferences":["If the syntactically defined idle set were replaced with a runtime-aware resource manager that tracks dynamic entanglement, the same SAT reduction could plausibly be lifted to dynamic scheduling; the paper does not develop this direction.","The two-state criterion for classical circuits suggests a testable extension: circuits made of Clifford gates plus classical controls might also admit a finite-state reduction, using the fact that $|+\\rangle$ and $|0\\rangle$ are stabilizer states.","Theorem 6.4 applies to circuits without borrow statements; extending the reduction to circuits that themselves contain nested borrows would require composing Boolean checks across instantiations, a natural next step not covered by the paper.","The semantics could serve as a specification for a type-and-effect system that statically enforces safe dirty-qubit borrowing, turning the verification result into a compile-time discipline rather than a post-hoc check."],"forward_implications":["Compilers for quantum programming languages can automatically verify borrow statements before allowing dirty-qubit reuse, instead of assuming safety by construction.","Safe uncomputation can be checked per dirty qubit individually, so a program may safely borrow some qubits while other borrows in the same program remain unsafe.","The finite-state refinement means full verification never requires enumerating all pure states: five basis states suffice in general, and two suffice for classical circuits.","The experimental results indicate that verification overhead grows polynomially with circuit size for the benchmarks, making the approach practical on current hardware.","Because safe uncomputation preserves external entanglement, verified dirty-qubit borrows are candidates for use in multi-program scheduling, where disturbing another program's qubits would cause errors."],"supporting_citations":[{"why":"Supplies the set-of-quantum-operations denotational semantics that the paper adapts to handle nondeterministic borrow choices.","marker":"[10]"},{"why":"Provides the constant-adder circuit and the toggling-trick construction used as the primary benchmark.","marker":"[15]"},{"why":"Provides the large multi-controlled-NOT construction used as the second benchmark.","marker":"[11]"},{"why":"Supplies the SMT solver used to check the generated Boolean formulas in the experiments.","marker":"[1]"},{"why":"Supplies the bit-vector SAT solver used to check the generated Boolean formulas in the experiments.","marker":"[22]"},{"why":"Defines the QWhile language whose syntax and semantics QBorrow extends.","marker":"[38, 39]"}],"fun_headline_variants":["Dirty qubits: two SAT checks verify safe return","Two SAT checks certify dirty-qubit uncomputation","Safe qubit reuse verified by just two SAT instances","Verify dirty-qubit borrowing with two SAT checks","Dirty qubit reuse reduced to two SAT checks"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the syntactically computed set of idle qubits faithfully describes which qubits are actually available at runtime, including the assumption that a nested borrow can reuse the same physical qubit sequentially; if a qubit looks idle but is entangled with the surrounding computation, the verification could certify a borrow that is not safe in practice.","fun_headline_variants_meta":{"raw":{"variants":["Dirty qubits: two SAT checks verify safe return","Two SAT checks certify dirty-qubit uncomputation","Safe qubit reuse verified by just two SAT instances","Verify dirty-qubit borrowing with two SAT checks","Dirty qubit reuse reduced to two SAT checks"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.0006,"raw_usage":{"total_tokens":2755,"prompt_tokens":848,"completion_tokens":1907,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":464,"completion_tokens_details":{"reasoning_tokens":1831}},"tokens_in":464,"tokens_out":1907,"duration_ms":14524,"temperature":1.0,"reasoning_tokens":1831,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T17:08:49.532230+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a classical circuit with a borrowed qubit, such as the five-qubit example in the paper's Figure 1.4, and run the reduction: if a SAT solver reports both formulas (6.1) and (6.2) unsatisfiable while a direct simulation of the circuit on the state $|+\\rangle$ shows that the borrowed qubit's reduced state is changed, the central theorem is false. More generally, brute-force search over small classical circuits can look for a circuit whose two Boolean formulas are both unsatisfiable but whose unitary is not of the form $V\\otimes I_q$.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the set-of-quantum-operations denotational semantics that the paper adapts to handle nondeterministic borrow choices."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the constant-adder circuit and the toggling-trick construction used as the primary benchmark."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the large multi-controlled-NOT construction used as the second benchmark."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the SMT solver used to check the generated Boolean formulas in the experiments."}],"review_version":2}