{"id":"a057efc1-5239-48a3-9517-35f562e9ccee","arxiv_id":"2501.05527","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"A SAT-based tool automatically synthesizes deterministic, fault-tolerant state preparation circuits for any small CSS quantum error-correcting code, with optimal measurement count.","lead":"This paper automates the design of quantum circuits that reliably prepare error-protected logical states for small quantum error-correcting codes, using a classical logic solver. It provides open-source tools and shows that the generated circuits prepare states in a single run instead of retrying, which is important for near-term quantum computers.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Correction-circuit faults are not included in the synthesis error model; a single CNOT fault inside the step-(d) measurements can spread to a weight-2 data error that no later protocol step is proven to catch.","rationale":"Agreement: the reader's weakest_assumption pinpoints the same gap—correction-circuit faults are only simulated, not formally included in the synthesis model. I agree with that reading, and I think it is the most load-bearing issue because it attacks the exact theorem stated in Section III-B ('we determine a correction circuit such that the overall procedure is fault-tolerant according to Definition 1'), not just the optimality or scalability claims. The paper's own technical section defines error sets only from faults in C and from single-qubit errors, and the conditional-correction measurements are unmodeled as fault locations. A single fault in the final correction layer has no later verification, so if it creates a weight-2 data error, the protocol fails Definition 1 for d=3/4 codes. The circuit-level DSS simulation is genuine supporting evidence: it includes all gate and measurement faults and shows quadratic p_L scaling, so the generated circuits likely are safe for the tested cases. This is why I would not move the verdict to REJECT; a targeted exact check is feasible and would convert the concern into a theorem or a counterexample. The paper also overstates optimality (two-hour timeout, weight-vs-CNOT equivalence), but that is secondary. Verdict remains CONDITIONAL as the reader had it.","tokens_in":10846,"tokens_out":8972,"duration_ms":94234,"concrete_test":"Use the released MQT open-source code to run an exact single-fault enumeration for each synthesized protocol. For every fault location inside the correction subcircuits of Fig. 3(d) (each CNOT, each ancilla fault, each measurement), inject the corresponding Pauli fault, propagate it through the full Clifford circuit, follow both branches of the conditional recovery, and apply the perfect final decoder. Check whether the final error is always stabilizer-equivalent to weight <= 1 for all codes in Table I. Because the circuits are Clifford and small, this is a finite enumeration that settles whether any unmodeled correction-circuit fault violates Definition 1; if all faults pass, the concern is resolved, and if any fails, the Section III-B claim is false as stated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central theorem in Section III-B claims that for a given non-deterministic FT preparation and verification, the synthesized correction circuit makes the overall procedure fault-tolerant according to Definition 1. The proof of this, in Section IV, builds the error sets E_X(C) and E_Z(C) exclusively from single faults in the non-fault-tolerant preparation circuit C, plus single-qubit errors that may be present when the correction is applied. Faults occurring inside the newly added correction measurements—the stabilizer measurements in step (d) of Fig. 3—are not elements of these sets. Concretely, in a weight-4 Z-stabilizer correction measurement implemented with an ancilla target, a single Z fault on the ancilla between CNOTs propagates as a weight-2 (or larger) Z error on the data qubits; an X fault on that ancilla can flip the very measurement outcome used to choose the recovery. Neither event is constrained by the synthesis condition that every error in a syndrome class be reducible to weight <= 1. If this happens in the last correction layer, no subsequent verification is available to catch the multi-qubit error, so Definition 1 would be violated. The DSS simulation in Section V-B exercises these faults and shows quadratic scaling, but it is numerical evidence, not part of the synthesis guarantee; the theorem as stated (and the abstract's unconditional optimality wording) claims more than the construction establishes. The concrete open question is whether the solver only ever outputs correction circuits whose internal hook faults are benign or are caught by a later layer—and whether that property holds for all codes, not just the tested ones.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper addresses deterministic fault-tolerant initialization of encoded logical states for small CSS codes. It builds on non-deterministic repeat-until-success state preparation: a generally non-fault-tolerant preparation circuit followed by verification. Given such a preparation and verification for an [[n,k,d]] CSS code with d<5, the authors formulate the synthesis of a correction circuit—additional stabilizer measurements followed by Pauli recovery—as a Boolean satisfiability problem. By iterating over the number of measurements and their weights, the correction circuit is claimed optimal in measurement count and CNOT weight. The protocol treats X and Z layers separately, uses flag qubits for hook errors in the verification measurements, and optionally globally optimizes verification and correction together. The paper reports circuit metrics for nine codes and validates the circuits by Dynamic Subset Sampling circuit-level noise simulations showing quadratic logical-error scaling, with code available as part of MQT.","tokens_in":11100,"tokens_out":7908,"duration_ms":83177,"significance":"If the central theorem were fully established, this would be a useful design-automation contribution: it replaces manual, code-specific constructions of deterministic fault-tolerant state preparation with a SAT-based search that gives per-branch optimality guarantees, and it ships open-source software. The DSS simulations provide strong empirical evidence that the generated circuits have no linear-error term for the tested depolarizing model, and the table of circuit metrics allows direct comparison with prior hand-crafted circuits. The paper is clearly written and the treatment of hook errors in verification via flag qubits is a sound and practical idea. The main gap concerns the fault model for the newly added correction measurements, which prevents the theorem as stated from being established.","major_comments":[{"comment":"The error sets E_X(C) and E_Z(C) are built exclusively from single faults in the non-fault-tolerant preparation circuit C, together with single-qubit errors present when the correction is applied; there is no corresponding error set for faults inside the newly added correction measurements of step (d) in Fig. 3. A single Z fault on the ancilla between two CNOTs of a weight-four correction stabilizer measurement propagates to a weight-two data error, and a single X fault on that ancilla can flip the very measurement outcome used to choose the recovery. Neither event is constrained by the synthesis condition that every error in a syndrome class be reducible to weight at most one, so the theorem that the overall procedure is fault-tolerant according to Definition 1 is not proven. The DSS simulations in Section V-B are numerical evidence, not part of the guarantee; without either an argument that correction-measurement faults are covered by subsequent verification or an extension of the error model, the abstract's unconditional fault-tolerance claim should be weakened.","section":"Section IV, 'CORRECTION CIRCUIT SYNTHESIS' and Section III-B"},{"comment":"The simulation protocol appends a perfect round of error correction before the final destructive measurement. This means the reported logical error rate does not directly test the fault-tolerance condition of Definition 1, which concerns the weight of the error on the output state before any further correction. A single fault in a correction measurement could produce a weight-two error that is nevertheless corrected by the final perfect decoder, so the quadratic scaling of p_L is necessary but not sufficient evidence for the strict fault-tolerance claim. The paper should either state that the numerical validation targets logical failure probability rather than the strict weight condition, or it should directly inspect the output error weight before the final correction.","section":"Section V-B, 'Simulation'"},{"comment":"The abstract and Section III-B claim that the synthesized correction circuits are guaranteed optimal, 'requiring as few CNOTs as possible.' However, Section V-A reports that the global optimization was canceled after two hours for the Carbon and [[16,2,4]] codes and explicitly describes the reported numbers as 'currently best-known circuits.' For those codes, exhaustive optimality is not established. The per-branch optimality for a fixed verification circuit is valid, but the global optimality claim must be qualified to the circuits actually explored, or the optimization must be run to completion with a documented runtime bound.","section":"Section V-A, 'Circuit Generation', and abstract"}],"minor_comments":[{"comment":"The future-work sentence states that codes beyond distance four would require 'correct handling of two or more independent errors, i.e., also within the conditional correction circuits.' This phrasing suggests that correction-circuit faults are only a problem starting at d>=5, but a single fault inside a correction measurement already needs to be handled for d=3 and d=4, since Definition 1 with t=1 applies to the entire circuit including the correction part.","section":"Section VI"},{"comment":"The exact SAT encoding is not described in the paper but only referenced to the source code. A short appendix with the Boolean constraints or a correctness argument for the encoding would make the method self-contained and easier to verify.","section":"Section IV"},{"comment":"The table is difficult to read because several entries are malformed, e.g., '0 .5 1 .5' and 'T etrahedal'; also 'Jn, k, dK' should be rendered as [[n,k,d]] for consistency with the text.","section":"Table I"},{"comment":"Reference [27] is a bare URL with no author or title; it should be replaced with a proper citation to the underlying public dataset or database.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The central issue is not fatal: with a modest extension of the error model to include faults in correction measurements, or a proof that the synthesized stabilizers are hook-error-safe or that such faults are caught by the second layer, the theorem can be repaired. I would therefore not recommend rejection. The paper fits the journal's scope; the heavy self-citation is justified by the close relation to the authors' prior work. The reviewer stress-test concern about correction-circuit faults lands and should be addressed before publication."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper does something genuinely useful: it automates the synthesis of deterministic correction circuits for non-deterministic fault-tolerant state preparation, across nine small CSS code families, and ships an open-source tool (MQT-QECC). The SAT encoding, the per-branch optimality in measurement count and CNOT weight, and the global search over verification/correction combinations are real new content, not just a repackaging of Ref. [17]. The DSS simulations show clean quadratic logical error scaling for every tested code, which is strong empirical evidence that the synthesized circuits behave fault-tolerantly under depolarizing noise. That part deserves credit.\n\nThe main soft spot is exactly what the stress-test note flags. The formal construction defines error sets E_X(C) and E_Z(C) from faults in the non-fault-tolerant preparation circuit and from single-qubit errors at correction time, plus hook faults from the verification circuit. It does not include faults occurring inside the newly added correction measurements in step (d) of Fig. 3. A single CNOT fault inside one of those stabilizer measurements can propagate to a weight-2 data error, and if that happens in the last correction layer, no later verification is available to catch it. The synthesis condition therefore does not actually prove that the overall procedure is fault-tolerant according to Definition 1; it proves it for faults in everything except the correction circuit itself. The simulation does exercise those faults, and the quadratic scaling is reassuring, but that is numerical evidence, not part of the claimed guarantee. This is an addressable gap, but it is load-bearing for the abstract's unconditional wording.\n\nSecondary issues are minor. The claim that the circuits are \"guaranteed to be optimal\" is too strong for the Carbon and [[16,2,4]] codes, where the global search hit the two-hour timeout, and Fig. 4 lacks error bars. The paper builds transparently on the authors' own prior work; the self-citation is appropriate here, since the new result explicitly extends that work rather than re-deriving it.\n\nMy verdict: this deserves a serious referee. The gap is fixable by either extending the error sets to include faults in the correction circuit and proving the synthesized circuits are hook-fault-safe, or by softening the claim to match what is actually proven. The empirical evidence is strong enough to justify that effort. I would bring it to our reading group and would cite it in work on FT state preparation.","headline":"Genuinely useful automation for fault-tolerant state preparation on small CSS codes, with a real but fixable gap in the formal guarantee for faults inside the correction circuit.","tokens_in":11674,"tokens_out":2067,"would_cite":true,"duration_ms":20549,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Satisfiability solving turns repeat-until-success state preparation into a deterministic, fault-tolerant protocol.","keywords":["quantum error correction","fault-tolerant state preparation","CSS codes","Boolean satisfiability","circuit synthesis","near-term quantum hardware","repeat-until-success","logical state initialization"],"falsifier":"Run the deterministic protocol under circuit-level depolarizing noise and inject a single Pauli fault on a CNOT inside one of the synthesized correction measurements, then decode the final state. If any such single fault produces a final data error of weight two or more that no later step detects, the deterministic fault-tolerance claim fails. Concretely, the error sets $E_b$ would need to be redefined to include the images of correction-circuit faults, and the SAT instance would have to be re-solved; a circuit with all such faults included in the verification would be the positive counterpart.","tokens_in":10606,"feed_emoji":"⚛️","tokens_out":7297,"duration_ms":66479,"temperature":0.7,"pith_summary":"This paper claims that the final obstacle to deterministic fault-tolerant state preparation for small CSS codes can be eliminated automatically. Given a non-deterministic preparation circuit, whose verification can detect but not fix dangerous errors, the authors synthesize a correction circuit that turns the whole procedure into a single-shot protocol, without post-selection or repeat-until-success. The search for the additional stabilizer measurements and the conditional recovery is encoded as a Boolean satisfiability problem and solved to optimality, minimizing both the number of measurements and the CNOT weight of the correction. If the claim holds, it removes a practical synchronization and time-overhead problem for near-term quantum hardware that encodes qubits in [[n,k,d]] CSS codes with $d < 5$. The paper supports the claim with circuit-level noise simulations showing that logical error rates scale quadratically in the physical error rate.","feed_headline":"SAT synthesis makes fault-tolerant state prep deterministic","feed_subtitle":"Automated correction circuits replace repeat-until-success with one-shot, fixed-depth encoded-state initialization.","key_machinery":"The load-bearing object is the syndrome partition of dangerous errors: errors from a single fault in preparation are grouped by the verification syndrome $b$ into sets $E_b$, and the correction circuit is a list of additional stabilizer measurements that splits each $E_b$ until every resulting class has a common recovery Pauli. The synthesis task, called CORRECTION CIRCUIT SYNTHESIS, is a decision problem asking whether $u$ stabilizer measurements of total weight at most $v$ can achieve this splitting, and it is solved by iterating over $u$ and $v$ with a Boolean satisfiability solver to obtain an optimum. For hook errors, the flag-qubit syndrome $f$ is appended to $b$ before the partition, so the same machinery makes the flag-based verification deterministic rather than repeat-until-success.","core_discovery":"The central claim is that any non-deterministic fault-tolerant state preparation for an [[n,k,d]] CSS code with $d < 5$ can be extended into a deterministic one by appending a correction circuit, while preserving strict fault-tolerance. The construction goes through the syndrome structure: for each syndrome $b$ of the verification measurements, the set of dangerous errors $E_b$ is further partitioned by additional stabilizer measurements until all errors in a class share a single recovery Pauli $c_b$; executing $c_b$ leaves at most a weight-one error. Hook errors, which arise when a fault in a verification measurement spreads to the data, are handled by flag qubits whose syndrome is fed into the same partition. The paper establishes that the synthesized correction circuits are optimal in the number of additional measurements and in the summed CNOT weight, and it reports globally optimized verification-plus-correction circuits for nine near-term codes, including the Steane, Shor, surface, and tesseract codes.","pith_inferences":["The same SAT formulation could be extended to distance-five codes if the correction circuit itself were made fault-tolerant, since the current $d < 5$ assumption keeps single-fault and hook-fault cases mutually exclusive.","A natural tightening of the method would be to add the correction-circuit CNOT faults into the error sets $E_b$ explicitly; this would turn the numerical fault-tolerance check into a formal guarantee.","Because the correction search depends only on the stabilizer structure, the technique could be composed with any verification synthesis approach, such as reinforcement-learning methods, to scale to larger codes without hand derivation.","On real hardware the protocol should show a fixed latency distribution rather than the heavy-tailed runtime of repeat-until-success, which is a directly testable signature of the deterministic procedure."],"forward_implications":["Any existing non-deterministic repeat-until-success state preparation for a $d < 5$ CSS code can be converted into a deterministic protocol with a guaranteed, fixed execution depth per run.","For a fixed verification circuit, the appended correction is optimal in measurement count and CNOT weight, so no smaller correction exists for that verification.","When the global optimization is run, the resulting verification-plus-correction pair is the smallest among all minimal verification circuits, which the table shows can beat the hand-crafted construction for the Shor and [[11,1,3]] codes.","The synthesized circuits achieve logical error rates $O(p^2)$ for $d < 5$ codes, meaning two independent physical errors are required for a logical error, as required by strict fault-tolerance.","The open-source implementation lets a user generate deterministic state preparation for a new small CSS code without manual analysis."],"supporting_citations":[{"why":"defines the existing manual deterministic scheme for one code that this work generalizes and improves","marker":"[17]"},{"why":"supplies the state preparation and minimal verification circuits to which correction circuits are appended","marker":"[22]"},{"why":"introduces flag fault-tolerant stabilizer measurement used to herald hook errors","marker":"[8]"},{"why":"provides the Dynamic Subset Sampling method used for circuit-level noise simulation","marker":"[14]"},{"why":"implements the Boolean satisfiability solving backend for correction synthesis","marker":"[9]"},{"why":"provides the simulation software used to compute logical error rates","marker":"[37]"},{"why":"demonstrates SAT-based Clifford circuit synthesis, the design-automation basis for this approach","marker":"[32]"},{"why":"states the strict fault-tolerance definition that the deterministic protocol is required to satisfy","marker":"[21]"}],"fun_headline_variants":["SAT turns probabilistic fault-tolerant state prep deterministic","Optimal fault-tolerant state prep automatically synthesized","One-shot fault-tolerant state prep via SAT synthesis","Deterministic fault-tolerant state prep is SAT-optimal"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The protocol is guaranteed fault-tolerant only if a fault inside the newly added correction circuit cannot spread into an undetectable weight-two data error; the paper's formal error model explicitly covers single-qubit and measurement errors in the correction stage, while the safety of correction-circuit CNOT faults is checked by simulation rather than by the synthesis condition.","fun_headline_variants_meta":{"raw":{"variants":["SAT turns probabilistic fault-tolerant state prep deterministic","Optimal fault-tolerant state prep automatically synthesized","One-shot fault-tolerant state prep via SAT synthesis","Deterministic fault-tolerant state prep is SAT-optimal"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000634,"raw_usage":{"total_tokens":2922,"prompt_tokens":936,"completion_tokens":1986,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":552,"completion_tokens_details":{"reasoning_tokens":1939}},"tokens_in":552,"tokens_out":1986,"duration_ms":15778,"temperature":1.0,"reasoning_tokens":1939,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T21:12:57.999292+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the deterministic protocol under circuit-level depolarizing noise and inject a single Pauli fault on a CNOT inside one of the synthesized correction measurements, then decode the final state. If any such single fault produces a final data error of weight two or more that no later step detects, the deterministic fault-tolerance claim fails. Concretely, the error sets $E_b$ would need to be redefined to include the images of correction-circuit faults, and the SAT instance would have to be re-solved; a circuit with all such faults included in the verification would be the positive counterpart.","supporting_citations":[{"cited_title":"Heußen et al","cited_arxiv_id":null,"evidence_quote":"defines the existing manual deterministic scheme for one code that this work generalizes and improves"},{"cited_title":"Chamberland et al","cited_arxiv_id":null,"evidence_quote":"introduces flag fault-tolerant stabilizer measurement used to herald hook errors"},{"cited_title":"Heußen et al","cited_arxiv_id":null,"evidence_quote":"provides the Dynamic Subset Sampling method used for circuit-level noise simulation"},{"cited_title":"de Moura et al","cited_arxiv_id":null,"evidence_quote":"implements the Boolean satisfiability solving backend for correction synthesis"},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"provides the simulation software used to compute logical error rates"},{"cited_title":"Shutty et al","cited_arxiv_id":null,"evidence_quote":"demonstrates SAT-based Clifford circuit synthesis, the design-automation basis for this approach"}],"review_version":1}