{"id":"97286564-253d-48fb-b4fd-ae427d3deba8","arxiv_id":"2411.09738","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"An SMT-based scheduler generates optimal state-preparation schedules for logical arrays on zoned neutral atom hardware, and shielding idle qubits in storage zones improves estimated fidelity.","lead":"This paper presents a compiler that uses an SMT solver to generate minimal instruction schedules for preparing logical qubit states on zoned neutral atom quantum computers. The schedules that exploit storage zones to shield idle atoms from Rydberg beams show higher estimated success probabilities than schedules that ignore zones.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The ASP comparison in Section V-A assumes unit shuttling fidelity; if realistic per-move transport error is included, the claimed zone-shielding advantage in Table I may shrink or reverse.","rationale":"I read the paper as an SMT-encoding contribution plus an evaluation of zone shielding on zoned neutral atom architectures. The SMT formulation is plausible, the encoding constraints are clearly stated, and the public open-source implementation is real evidence of reproducibility. However, the comparative fidelity claim is the central result, and it is evaluated under an ASP model whose Shuttling fidelity is set to 1.0. This is not an external-consensus issue; it is an internal modeling gap: the very mechanism proposed for improving fidelity—moving qubits into storage zones—introduces extra transport operations whose error cost is set to zero. The paper's own table lists Load/Store at 0.999 and shuttling speed but no shuttling error rate, so the natural extension of its model is a non-unit per-move fidelity. A small error per moved atom can plausibly erase the reported ASP differences, because the zoned schedules add many movements and the baseline does not. The objective function also minimizes the number of stages rather than ASP, and since transfer stages take roughly 200 µs while Rydberg stages take 0.27 µs, a stage-minimal schedule need not maximize ASP. This reinforces the need for a direct sensitivity test rather than a new asymptotic argument. The reader's weakest assumption identifies the same Shuttling 1.0 issue, and I agree with that assessment. My proposed check—recomputing ASP with a nonzero per-shuttle error rate from the actual schedules—would settle whether the concern actually lands. Given that the tooling and encoding are solid and the issue is isolated to the fidelity model, the appropriate verdict remains CONDITIONAL rather than REJECT.","tokens_in":12136,"tokens_out":6136,"duration_ms":68242,"concrete_test":"Recompute Table I's ASP for Layouts 2 and 3 from the released MQT schedules, replacing the unit Shuttling fidelity with p = 0.999 per moved atom (and optionally p = 0.9999), counting every AOD row/column movement per qubit while leaving CZ, IdRyd, and Load/Store figures unchanged. If for either p the resulting ASP for Layout 2 or 3 falls below Layout 1 on more than one of the six codes, the claimed advantage of zone shielding does not survive a realistic transport-error model and the central empirical claim should be revised. If the advantage persists, the concern is settled in the paper's favor.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central empirical claim ('actively utilizing zones ... consistently results in higher fidelities', abstract and Section V-C) rests on the figures-of-merit table in Section V-A, which assigns Shuttling a fidelity of 1.0 while Load/Store is 0.999. Zoned layouts achieve their ASP gains by moving qubits between the entangling and storage zones, so every schedule in columns (2) and (3) contains shuttling and transfer operations that the no-shielding baseline does not. If a single shuttled atom has non-negligible error or loss—as is typical for AOD transport in the cited experimental systems—then the exp(-t_idle/T_eff) and IdRyd terms that currently dominate the comparison are not the only costs: each movement contributes a factor p_shuttle < 1. For a modest schedule with roughly ten per-qubit movements, p_shuttle = 0.999 alone contributes about 0.99, which is comparable to the 0.01–0.03 ASP improvements reported in Fig. 4. Thus the 'consistently higher' claim is conditional on an unverified, favorable transport-error model. The paper supplies no sensitivity analysis over p_shuttle, and the ASP formula in Section V-A is used as the conclusive comparison without such a robustness check.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents an SMT-based compilation method for state preparation circuits of quantum error correction codes on zoned neutral atom architectures. The formulation symbolically represents qubit positions, AOD/SLM trap assignments, gate execution, trap transfers, shuttling, and zone shielding, and uses an objective that minimizes the total number of stages. The evaluation compares three layouts — no shielding, bottom storage, and double-sided storage — across six QEC codes, using an approximated success probability (ASP) as a fidelity proxy. The authors report that zoned layouts consistently yield higher ASP than the no-shielding baseline, and the implementation is released as open source in the Munich Quantum Toolkit.","tokens_in":12433,"tokens_out":4291,"duration_ms":45923,"significance":"The paper addresses a timely and practical compilation problem: preparing logical arrays on zoned neutral atom hardware, for which existing neutral-atom compilers lack zone support. Its main strengths are the explicit, verifiable SMT constraint system; the public open-source implementation; and the demonstration that small instances can be solved to proven optimality in stage count. If the fidelity conclusions hold, the work provides useful building blocks for future fault-tolerant neutral atom systems and a tool for exploring architectural design choices. However, the central empirical claim — that zone shielding consistently improves fidelity — is currently supported only under a specific, partially unverified error model, so the significance of the result is conditional on that model.","major_comments":[{"comment":"The comparison that underlies the abstract and Section V-C assigns a fidelity of 1.0 to shuttling, while Load/Store is assigned 0.999. Zone-shielded schedules in columns (2) and (3) contain additional shuttling and transfer operations that the no-shielding baseline does not, so the reported ASP gains of roughly 0.01–0.03 in Fig. 4 are computed without any per-move transport error. If a single shuttled atom has an infidelity or loss probability as small as 0.001, a schedule with about ten per-qubit movements contributes a factor near 0.99, which is comparable to the entire reported improvement. The manuscript supplies no sensitivity analysis over the shuttling fidelity and no experimental or cited evidence that unit shuttling fidelity is realistic for the considered AOD transport. Since the conclusion that shielding 'consistently results in higher fidelities' rests on this assumption, the authors should either justify the unit-fidelity assignment with direct evidence or add a sensitivity analysis over p_shuttle and qualify the claim accordingly.","section":"Section V-A, ASP formula and Table I"},{"comment":"The objective function minimizes the total number of stages S, not the ASP or any direct fidelity estimate. For each minimal S, the SMT solver returns an arbitrary satisfying assignment; the ASP values reported in Table I are therefore not guaranteed to be optimal among all schedules with that minimal stage count. Since ASP depends on the specific distribution of transfers, shuttling distances, and idle times, a different minimal-stage schedule could yield a different ASP. This does not invalidate the tool, but it means the title's 'optimal state preparation' and the discussion in Section V-C should be stated as optimal in stage count only, and the comparison in Table I should be described as a comparison of particular schedules, not necessarily ASP-optimal ones. The authors should clarify this limitation and, ideally, add an ASP-aware tie-breaking or post-processing step.","section":"Section IV-C and Section V-B"}],"minor_comments":[{"comment":"The definition of t_idle as 'the accumulated idle time of all qubits' is ambiguous: it is not clear whether this is a sum over qubits, a maximum, or a wall-clock quantity, nor how shuttling time enters it. Since ASP is the primary comparison metric, the formula should specify the aggregation precisely to make the results reproducible.","section":"Section V-A, ASP definition"},{"comment":"For the larger codes (Hamming, Tetrahedral, Honeycomb), the Layout 2 and 3 entries are marked as 'may not be optimal due to solver timeout.' Section V-C should explicitly state that the 'consistently higher' claim for these cases is based on suboptimal zoned schedules, which still beat the optimal baseline; this is a meaningful observation but should not be conflated with an optimality statement.","section":"Section V-B, Table I"},{"comment":"The vertical analog of the AOD ordering constraint and the loading-constraint analog of Eq. (20) are 'omitted for brevity.' Given that the paper's contribution is the verified constraint model, these omissions make it harder for readers to reproduce or audit the full SMT encoding. A short appendix or listing of the complete constraints would improve the paper.","section":"Section IV-B, constraints C5 and C6"},{"comment":"The notation for codes, e.g., 'J7, 1, 3K', is standard in some communities but may confuse readers; a one-line explanation that this denotes an [n, k, d] code would be helpful.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The paper describes a useful and reproducible compiler contribution, and I would be happy to see it published after the authors address the two load-bearing issues: the unit-shuttling-fidelity assumption in the fidelity comparison, and the mismatch between optimizing stage count and claiming fidelity-optimal or consistently higher-fidelity schedules. The sensitivity analysis requested in the major comments is a normal and feasible addition for this kind of systems paper."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague —\n\nThe genuinely new thing here is an SMT encoding for state preparation on zoned neutral atom architectures, with constraints for zone shielding, trap transfers, AOD ordering, and shuttling, plus a public implementation in MQT. The formulation is explicit and the small instances solve to proven optimality. The ASP metric and benchmark circuits come from external hardware parameters and STABGRAPH, not from the schedules produced by the tool, so the evaluation is not circular. That is a real step forward for compilation for neutral atoms, and the architecture-layout comparison (no shielding vs bottom storage vs double-sided storage) is useful for hardware design.\n\nThe soft spot is the fidelity claim, and the stress-test note lands. The abstract says shielding \"consistently results in higher fidelities,\" but the comparison rests on the ASP table in Section V-A, which assigns shuttling a fidelity of 1.0. Zoned schedules buy their ASP gains by moving atoms into storage zones; those movements are exactly the operations the no-shielding baseline avoids. If per-move transport error is, say, 0.999, then a schedule with ten movements contributes a factor of 0.99, which is in the same range as the 0.01–0.03 ASP improvements in Fig. 4. The authors do not provide a sensitivity analysis over p_shuttle, so the \"consistently higher\" conclusion is conditional on an unverified and favorable transport-error model. This is not fatal to the scheduling contribution, but it should be fixed before the paper is relied upon: either add a sensitivity sweep over shuttling fidelity and atom loss, or weaken the claim.\n\nA second, smaller issue: the objective function minimizes the number of stages, while the evaluation metric is ASP. Minimizing stage count is a reasonable proxy, but it is not the same as maximizing ASP, and transfer stages are about 100x slower than other operations. The paper should note this gap explicitly and justify the proxy.\n\nThe abstract's \"minimal schedules\" claim is also slightly too strong, since the large-code entries in Table I are starred as possibly non-optimal due to timeout. The introduction and discussion hedge appropriately; the abstract does not.\n\nFor the intended audience — people building compilers for neutral atom hardware or doing architecture exploration — this is a solid, reproducible contribution with an honest evaluation. It deserves a serious referee, and the revision should focus on the shuttling-fidelity assumption and the objective-function mismatch, not on the encoding itself.","headline":"Useful SMT scheduling encoder for zoned neutral atom state preparation, but the headline fidelity advantage rests on a shuttling-fidelity assumption the paper does not stress-test.","tokens_in":12902,"tokens_out":2452,"would_cite":true,"duration_ms":23531,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"State preparation on zoned neutral atom machines can be compiled to minimal schedules with a satisfiability solver, and shielding idle qubits raises fidelity.","keywords":["quantum error correction","state preparation","neutral atom architectures","zoned architectures","satisfiability modulo theories","schedule optimization","logical arrays","compilation"],"falsifier":"Run the same schedules on hardware with measured per-micron shuttling and atom-loss rates and recompute the success probability with those rates included; if the no-shielding baseline wins on any of the six codes, the claim that shielding consistently improves fidelity is refuted.","tokens_in":11942,"feed_emoji":"⚛️","tokens_out":6498,"duration_ms":62836,"temperature":0.7,"pith_summary":"This paper addresses how to turn a state-preparation circuit for a quantum error-correcting code into a minimal schedule of Rydberg beams, trap transfers, and shuttles on a zoned neutral atom machine. The authors propose a satisfiability modulo theories formulation whose satisfying assignments are physically valid schedules and whose objective minimizes the number of stages. They report that schedules that move idle qubits into storage zones during entangling pulses achieve higher approximated success probabilities than schedules that leave all qubits in the entangling zone. If correct, this gives quantum error correction a reusable compilation primitive and a way to compare hardware layouts before building them.","feed_headline":"Shielded schedules beat exposed ones on all six QEC codes","feed_subtitle":"A satisfiability-based compiler produces minimal Rydberg and transfer schedules; storage-zone shielding wins on every code tested.","key_machinery":"The load-bearing object is a symbolic stage-based schedule model. Time is divided into discrete stages; each stage is either an execution stage (a global Rydberg beam followed by shuttling of movable AOD traps) or a transfer stage (load and store operations between static SLM traps and movable AOD traps followed by shuttling). Boolean and integer variables encode qubit positions, AOD rows and columns, and gate assignment, while constraints enforce physical feasibility: one qubit per trap, ordered AOD lines, shielding of idle qubits outside the entangling zone, and no trap transfers during execution stages. Minimizing the total number of stages under these constraints produces the schedule with the fewest error-prone Rydberg and transfer operations.","core_discovery":"The central claim is that optimal state preparation for logical arrays on zoned neutral atom architectures can be generated with an SMT-based compiler, and that the optimal schedules consistently use storage zones to shield idle qubits. For all six tested QEC codes, every schedule produced for a layout with a storage zone has a higher approximated success probability than the no-shielding baseline, even after counting the added shuttling and transfer stages. The paper therefore positions itself as providing the first optimal state-preparation compiler for this architecture and as demonstrating quantitatively that zoned shielding is not just a hardware feature but a fidelity benefit.","pith_inferences":["If real per-micron shuttling error or atom loss is measured, the crossover at which shielding stops improving fidelity can be computed and used as a concrete hardware target.","The same encoding applies to any fixed list of CZ gates, so syndrome extraction or logical gate layers are plausible next targets beyond state preparation.","Because schedules are generated offline, even multi-day solver runs become acceptable for reusable building blocks, decoupling compilation cost from runtime speed."],"forward_implications":["For the smallest tested codes, the solver terminates in under a second, so optimal schedules can be precomputed once and reused as fixed building blocks.","Zone-shielded schedules use more transfer stages, yet their approximated success probability is higher than exposing idle qubits to Rydberg pulses.","A double-sided storage layout gives slightly higher approximated success probability than a single bottom storage zone because shuttle distances and transfer counts are smaller.","Zone-unaware compilers can at best match, never beat, the no-shielding baseline, because their schedules are a subset of the shielded search space.","The method also serves as a hardware-design probe: changing the number and placement of storage zones yields quantitative fidelity comparisons before a device is built."],"supporting_citations":[{"why":"Supplies the zoned neutral atom architecture, the load/store and shuttling figures of merit, and the experimental basis for shielding idle qubits.","marker":"[9]"},{"why":"Provides the SMT solver used to decide feasibility and optimality of the encoded schedules.","marker":"[10]"},{"why":"Defines the approximated success probability objective that compares schedules across layouts.","marker":"[17]"},{"why":"Provides the Rydberg CZ and faulty-identity fidelity values used in the ASP calculation.","marker":"[20]"},{"why":"Contributes the AOD column/row ordering and loading constraints adopted in the symbolic model.","marker":"[22]"},{"why":"Supplies the stage-based trap-site abstraction that the symbolic formulation extends to zones.","marker":"[24]"},{"why":"Generates the stabilizer-based state preparation circuits used as input benchmarks.","marker":"[31]"}],"fun_headline_variants":["SMT solver finds optimal shielded prep for atom qubits","All six QEC codes favor shielded schedules","Shield idle qubits for optimal atom state prep","Storage zones boost fidelity in atom state prep","SMT-based prep beats unshielded on every QEC code"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The fidelity comparison treats shuttling as error-free and counts only idle decoherence and gate fidelities, so if real atom shuttling has non-negligible error or loss, the measured advantage of shielding could shrink or disappear.","fun_headline_variants_meta":{"raw":{"variants":["SMT solver finds optimal shielded prep for atom qubits","All six QEC codes favor shielded schedules","Shield idle qubits for optimal atom state prep","Storage zones boost fidelity in atom state prep","SMT-based prep beats unshielded on every QEC code"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001286,"raw_usage":{"total_tokens":5219,"prompt_tokens":875,"completion_tokens":4344,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":491,"completion_tokens_details":{"reasoning_tokens":4268}},"tokens_in":491,"tokens_out":4344,"duration_ms":28502,"temperature":1.0,"reasoning_tokens":4268,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T20:22:10.313365+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the same schedules on hardware with measured per-micron shuttling and atom-loss rates and recompute the success probability with those rates included; if the no-shielding baseline wins on any of the six codes, the claim that shielding consistently improves fidelity is refuted.","supporting_citations":[{"cited_title":"Computational capabilities and compiler development for neutral atom quantum processors—connecting tool developers and hardware experts,","cited_arxiv_id":null,"evidence_quote":"Defines the approximated success probability objective that compares schedules across layouts."},{"cited_title":"Logical quantum processor based on reconfigurable atom arrays,","cited_arxiv_id":null,"evidence_quote":"Supplies the zoned neutral atom architecture, the load/store and shuttling figures of merit, and the experimental basis for shielding idle qubits."},{"cited_title":"Z3: An Efficient SMT Solver,","cited_arxiv_id":null,"evidence_quote":"Provides the SMT solver used to decide feasibility and optimality of the encoded schedules."},{"cited_title":"High-fidelity parallel entangling gates on a neutral-atom quantum computer,","cited_arxiv_id":null,"evidence_quote":"Provides the Rydberg CZ and faulty-identity fidelity values used in the ASP calculation."},{"cited_title":"Compiling Quantum Circuits for Dynamically Field-Programmable Neutral Atoms Array Processors,","cited_arxiv_id":null,"evidence_quote":"Supplies the stage-based trap-site abstraction that the symbolic formulation extends to zones."},{"cited_title":"Scalable characterization of localizable entanglement in noisy topological quantum codes,","cited_arxiv_id":null,"evidence_quote":"Generates the stabilizer-based state preparation circuits used as input benchmarks."}],"review_version":1}