{"id":"75b5bb03-d931-4e25-b905-ab717a304a43","arxiv_id":"2608.08282","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Stateful CARS exactly samples LLM-agent trajectories conditioned on a hard stateful validator by applying sound state-continuation schemas across histories, with correctness proved and verified but no matched speed advantage over root-prefix CARS.","lead":"Researchers built a sampling procedure that draws complete tool-use action histories from the exact conditional distribution under hard, state-dependent rules, while reusing proofs that a continuation is invalid at matching abstract states. Generalists should read it because it shows exactly when such cross-history invalidity reuse is sound, and honestly finds no speed advantage over an existing baseline.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 8 is sound under its assumptions, but the key obligation—certified sound schemas and exact policy probabilities for every reachable history—is verified only on enumerable, policy-restricted workflows; the abstract's exact-reuse claim is therefore narrower than it appears.","rationale":"I read the formal core carefully. Lemma 6's telescoping argument, Lemma 7's event-level soundness, Lemma 11's grounding soundness, and Theorem 8's conditioning on G_{k-1} and the tower property are internally consistent; the proof does not require E_B to be a trie union, which is what makes schema-induced events valid. Proposition 5's complexity boundary is stated honestly, and the matched B-C comparison plus the appended retractions show a careful empirical discipline. The reader's weakest assumption matches the concern I find most load-bearing: exactness is conditional on certified sound schemas and exact policy probabilities for every reachable history, and the paper verifies these only on enumerable bounded workflows via exhaustive enumeration, explicitly declining to claim verified exactness on free-form tasks. This is a genuine limitation of scope, not a flaw in the theorem. Because the paper already states this limitation clearly and frames the central claim as a conditional exactness result, the verdict should remain ACCEPT. My proposed concrete test—an SMT-based certification on a non-enumerable symbolic validator—would determine whether the obligation can be discharged beyond exhaustive enumeration, and thus whether the method's exact-reuse guarantee can extend past the currently verified regime.","tokens_in":38965,"tokens_out":17776,"duration_ms":172949,"concrete_test":"Build the Appendix S certification harness on a non-enumerable but symbolic validator—e.g., a tool-call grammar with unbounded integer arguments and an observation-conditioned eligibility predicate—and replace exhaustive enumeration with an SMT solver (Z3) to discharge Assumption 2 and each candidate schema's soundness over the infinite reachable set. If the solver certifies the abstraction and a finite projection of the sampler's law matches the enumerated target of a bounded sub-instance within the i.i.d. sampling floor, the concern is mitigated. If the solver finds a counterexample or cannot terminate, the exactness claim is not established outside enumerable workflows.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The theorem's exactness rests on two obligations that must hold for every reachable full history, not just sampled ones: (i) exact full-history policy probabilities for every node the residual recursion explores, and (ii) soundness of every schema, which requires a validity-preserving abstraction (Assumption 2) quantified over all reachable histories in an abstract class. The paper discharges (ii) by exhaustive enumeration on bounded grammars (Appendix S, 1300 histories over 8 worlds; Tables 7-8) and (i) by defining the policy as a float64 softmax over restricted first-token ids (Appendix Q). Within that scope the claims are exactly what they say, and Theorem 8 follows from Lemmas 6-8. The load-bearing gap is the step from these certified enumerable settings to the general LLM-agent framing: for a free-form agent with unbounded tool arguments and observation-conditioned histories, the reachable set is not enumerable, so schema soundness cannot be checked by the paper's method, and an unsound schema is not a benign approximation—Proposition 10 makes the removed valid mass exactly the TV error. The paper is explicit about this limitation, so this is a scope concern rather than an internal inconsistency; but it is the place where a reader could over-read the abstract's 'exact cross-history reuse' as a verified property of LLM agents in general.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"Stateful CARS proposes a constrained sampling algorithm for language-model agents under stateful hard validators. It freezes a bank of sound state–continuation schemas per attempt, uses the resulting schema-induced exclusion event to compute a residual Doob h-transform, and proves (Theorem 8) that returned trajectories are i.i.d. from the target conditional Pθ(·|C), with almost-sure termination, under exact full-history policy probabilities, sound schemas, event-preserving compression, and a fixed bank within each attempt. The paper also proves schema soundness via a future-validity bisimulation, characterizes computational cost as linear in reachable product states (exponential in worst case), and evaluates the method on enumerable tool-use workflows with enumerated targets, an exhaustive abstraction audit, a Qwen2.5 sweep, live sqlite/tau-bench validators, and a matched comparison against observation-keyed root-prefix CARS. The matched comparison is negative on sampler steps (root/Stateful 0.942), the Qwen comparison is null, and the authors retract earlier step-count advantages.","tokens_in":39260,"tokens_out":14829,"duration_ms":131836,"significance":"Assuming the proofs are correct—and I found no error in the fixed-exclusion and adaptive-exactness arguments of Appendices F.3/F.5—the paper delivers a sound exact construction for schema-induced conditioning, verified to machine precision against independently enumerated targets. The evaluation is unusually disciplined: exact enumerated targets, analytic TV of order 1e-16, zero-excluded-valid-mass audits, predeclared analyses, released vector tables, and explicit retractions of earlier empirical claims. The principal caveat is scope: the obligations of Theorem 8 (sound schemas for every reachable history, exact full-history policy probabilities) are discharged only on enumerable, bounded-policy workflows; the paper says so honestly in §8, but the title/abstract still invite over-reading. This is a scope limitation, not an internal inconsistency, and it does not undermine the theorem.","major_comments":[{"comment":"Section 8 states that the visited-grounding finite-trie variant \"has not been implemented or evaluated here,\" but §4.2 says it is implemented and Appendix U reports its implementation, obligations, and measurements, including Table 22 with VG/OK ratios of 0.21 and 0.38 on the high-fan-out domains and parity on low-fan-out domains. As written, the manuscript contradicts itself about which constructions are evaluated; please correct the Limitations paragraph and make explicit which measurements are part of the paper's claims.","section":"§8 vs. §4.2, Appendix U, Table 22"},{"comment":"The Limitations paragraph says \"we claim no step-count, wall-clock, or storage advantage over the closest exact method,\" but Table 18 reports a wall-clock ratio C/B = 1.268 [1.155,1.381] favoring Stateful CARS and a 6.10× [5.82,6.39] smaller serialized-byte footprint, and the Conclusion states \"a memory advantage—not a speed claim.\" The abstract's \"not a systems advantage over CARS\" needs the same qualification. The efficiency verdict must be rewritten so the negative claim and the reported wall-clock/memory results are consistent.","section":"§8 vs. Appendix N.1 (Table 18) and Conclusion"}],"minor_comments":[{"comment":"The exactness claim should be qualified in the abstract itself as holding for the enumerable, bounded-policy workflows in which the obligations of Theorem 8 are verified (Appendix S, Tables 7-8), since the paper explicitly disclaims verified exactness for free-form tasks in §8.","section":"Abstract and §8"},{"comment":"The sentence \"|0.895−0.500| ≈0.395 is exactly the tilt\" equates a world-marginal difference with total variation; please clarify that the reported TV for the two-world example is the enumerated value for the full joint law, not the difference of the two world marginals alone.","section":"Appendix G"},{"comment":"The Qwen sweep defines the action policy as a float64 softmax over restricted first-token ids, which is a declared scoring rule rather than the full autoregressive trajectory distribution; a one-sentence reminder in the main text near Table 14 would help prevent readers from interpreting the analytical TV rows as exactness for the LM's full conditional.","section":"Appendix Q and §6.2"}],"recommendation":"minor_revision","confidential_remarks":"This is a strong and unusually honest paper. The two contradictions in Section 8 are the only substantive problems I found; they should be reconciled before publication. The scope limitation to enumerable workflows is handled transparently and does not affect the soundness of the main theorem."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this is a genuinely careful paper. It proves an exact adaptive-rejection construction for stateful constraints with schema reuse, verifies it on enumerable workflows down to TV 1e-16, and explicitly retracts its own earlier efficiency claims when matched comparisons go negative. The main caveat is scope: Theorem 8 is conditional on exact full-history policy probabilities and certified sound schemas for every reachable history, and the paper only discharges those obligations on bounded, enumerable grammars. The abstract's 'exact cross-history reuse' for LLM agents is a construction with verified instances, not a verified property of free-form agents.\n\nWhat's new: the schema-induced exclusion event (Eq. 2), the freeze-and-commit update, the future-validity bisimulation condition, and the adaptive exactness theorem are real additions to the CARS line. The proofs in Appendix F are coherent; Lemmas 6-8 and Theorem 8 follow from the stated assumptions. I particularly respect the evaluation discipline: enumerated targets, analytic TV at 1e-16, exhaustive zero-excluded-valid-mass audits, matched observation-keyed CARS comparison, and public retractions. This is how you report negative results. The citation pattern looks fine; no self-citation inflation, and the related work is appropriately broad.\n\nSoft spots, in proportion. The biggest is the step from enumerable to free-form. The paper states this limitation clearly in Sections 7-8, so it's a scope issue rather than an internal flaw, but a casual reader of the abstract could over-read. Second, the requirement of exact per-history policy probabilities is strong; for real LLMs that's a float64 restriction to predeclared action codes, which is fine in the testbed but not a general property. Third, no code URL appears in the text, which caps reproducibility despite the careful manifest description. These are minor-to-moderate, not fatal.\n\nWho should read it: people working on constrained decoding, rejection sampling for LLM agents, or exact conditional sampling. It deserves a serious referee; I'd send it to a strong ML or NLP venue. Recommendation: accept after minor revision, and ask the authors to add the code link and to sharpen the abstract so 'exact' is explicitly scoped to enumerable, policy-restricted workflows.","headline":"A disciplined exact-sampling paper whose main theorem is sound but whose verified scope is enumerable workflows; the abstract slightly oversells the LLM-agent reach.","tokens_in":39779,"tokens_out":2261,"would_cite":true,"duration_ms":22425,"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":"Stateful CARS shows that adaptive cross-history reuse of invalidity certificates can be made exact: with a frozen bank of sound schemas and a residual Doob transform, accepted trajectories are i.i.d.","keywords":["constrained decoding","stateful validators","LLM agents","rejection sampling","Doob transform","schema reuse","exact conditional sampling","future-validity bisimulation"],"falsifier":"On any finite enumerable workflow with an enumerated target $P_\\theta(\\cdot \\mid C)$, run Stateful CARS while memoizing residuals by abstract state alone instead of by complete serialized history plus matcher state; if the accepted law differs from the enumerated conditional by more than sampling noise, the distinct-history cache requirement of Proposition 5 fails. Alternatively, build two reachable histories with the same abstraction but different future-validity continuation languages, store a schema certified at one of them, and check that the sampled TV to the target equals $P_\\theta(E \\mid C)$, the exact false-exclusion cost of Proposition 10.","tokens_in":38769,"feed_emoji":"🎲","tokens_out":10234,"duration_ms":99868,"temperature":0.7,"pith_summary":"The paper is trying to establish an exact sampling method for tool-using language-model agents whose validity constraint is stateful—the same continuation can be legal or illegal depending on earlier tool observations. It introduces Stateful CARS, which freezes a bank of sound state–continuation schemas at the start of each attempt and removes every trajectory that contains a certified continuation at a matching abstract state, then samples from the residual via a Doob h-transform. The central theorem states that, under finite horizon, exact full-history policy probabilities, sound schemas, event-preserving compression, and a bank frozen per attempt, every returned trajectory is drawn i.i.d. from the validator-conditional law $P_\\theta(\\cdot \\mid C)$, with almost-sure termination. The paper also proves that an unsound schema costs exactly its excluded valid mass in total variation, and it reports negative efficiency results: matched observation-keyed root-prefix CARS is cheaper in sampler steps, so the contribution is exact cross-history conditioning rather than a systems advantage.","feed_headline":"Frozen schema banks give exact conditional LLM-agent sampling","feed_subtitle":"Accepted draws are i.i.d. from the validator-conditional law even when validity is vanishingly rare—but root-prefix CARS stays cheaper.","key_machinery":"The load-bearing object is the schema-induced exclusion event $E_B=\\{\\tau : \\exists t,\\, (z,u)\\in B,\\, \\phi(h_t(\\tau))=z,\\, a_{t:t+|u|-1}=u\\}$, together with the residual mass $r_B(h)=P_\\theta(E_B^c \\mid h)$ and the residual proposal $Q_B(a \\mid h)=\\pi_\\theta(a \\mid h)\\,r_B(\\operatorname{Succ}(h,a))/r_B(h)$. A schema $(z,u)$ is sound when the continuation $u$ is non-completable at every reachable history with abstraction $z$; soundness is checkable by the future-validity bisimulation of Assumption 2, which says equal abstraction implies equal terminal acceptance and equal abstract successors. The fixed-exclusion lemma telescopes the residual ratios, so sampling from $Q_B$ is exactly conditioning on avoiding $E_B$; because frozen banks are always sound, that conditioning is exactly $P_\\theta(\\cdot \\mid C)$. The recursion is memoized on the complete serialized history plus matcher state, and lossless compression is allowed only when it preserves $E_B$. This is what carries the proof of adaptive exactness, i.i.d. returns, and almost-sure termination in Theorem 8.","core_discovery":"The central claim is that the exclusion object of constrained adaptive rejection sampling can be lifted from a single concrete root prefix to a schema $(z,u)$ that is sound for every history abstracting to $z$, without changing what is being sampled. The construction freezes the schema bank for the whole attempt, defines the induced exclusion event $E_B$, and uses the residual mass $r_B(h)=P_\\theta(E_B^c \\mid h)$ in the proposal $Q_B(a \\mid h)=\\pi_\\theta(a \\mid h)\\,r_B(\\operatorname{Succ}(h,a))/r_B(h)$. Telescoping the residual ratios along the trajectory shows $Q_B(\\tau)=P_\\theta(\\tau)/P_\\theta(E_B^c)$, and since $E_B \\cap C=\\emptyset$ the accepted law is exactly $P_\\theta(\\cdot \\mid C)$. Theorem 8 extends this to adaptive reuse: whatever sound bank the past selects, the returned trajectories are i.i.d. from the target, the next return is almost sure, and the expected attempt count is at most $1/P_\\theta(C)$. The mechanism is exact in the evaluated enumerable workflows—the analytic law matches the conditional to $10^{-16}$ at validity $6\\times10^{-8}$—while the matched efficiency comparison is negative: observation-keyed official CARS wins in sampler steps (root/Stateful ratio $0.942$ [$0.934,0.951$]).","pith_inferences":["For deployment on free-form agents, the exact global residual recursion is not the route; the delayed visited-grounding finite-trie variant, proved exact through the same fixed-exclusion lemma and measured only in an appendix, would be the more scalable engineering choice.","With stochastic tool outcomes the hidden world must be drawn from the residual-reweighted prior $\\propto \\rho(c)Z_c$; a uniform world draw is exact only in single-satisfiable-world settings, and in multi-world settings it tilts the world marginal (the paper measures TV $0.395$ for the naive draw).","Near-machine-epsilon TV values should be read as float64 arithmetic precision statements: under float32 policy bookkeeping the same exact sampler shows TV $\\approx10^{-8}$, so the published $10^{-16}$ numbers do not imply model-level exactness in ordinary serving precision.","Reuse benefit does not track reuse fan-out: across the paper's five domains, the highest-fan-out task had nearly the smallest reuse factor ($1.13$ at fan-out $55.9$), so high-fan-out workflows are not automatically where schema transfer pays."],"forward_implications":["Accepted samples can be used as statistically sound i.i.d. draws from the exact validator-conditional law, even when $P_\\theta(C)$ is as low as $6\\times10^{-8}$, so downstream probability-sensitive uses such as self-consistency, uncertainty, and decisions based on relative probability are valid.","Adaptive reuse and compression do not perturb the target: a missed certificate only slows the sampler, while any sound, event-preserving certificate leaves the accepted law unchanged.","The cost of an unsound abstraction is exactly quantified: removing a fraction $P_\\theta(E \\mid C)$ of valid mass moves the returned law by that same total-variation distance, so abstraction soundness must be verified over every reachable history, not just sampled ones.","The residual recursion visits $O(|A|\\,|R_B|)$ product nodes and can be exponential in the horizon for a history-dependent policy, so practical exactness is bounded to enumerable workflows or policies with finite Markov structure.","The method claims exactness, not speed: under matched observations and official updates, root-prefix CARS is cheaper in sampler steps (ratio $0.942$ [$0.934,0.951$]), and the open-weight LM comparison is null."],"supporting_citations":[{"why":"Supplies the root-prefix CARS construction and its official update, which Stateful CARS generalizes and against which the matched efficiency comparison is drawn.","marker":"Parys et al. (2025)"},{"why":"Provides the SMC-based constrained decoding perspective and the future-validity statistic that motivates the residual Doob transform.","marker":"Loula et al. (2025)"},{"why":"Frames the future-validity correction in constrained decoding, the quantity the paper makes exact through its residual recursion.","marker":"Nie et al. (2026a)"},{"why":"Provides the adaptive weighted rejection sampling baseline used in adjacent-sampler cost comparisons.","marker":"Lipkin et al. (2025)"},{"why":"Provides the Qwen2.5-Instruct models whose restricted softmax policy vectors drive the fifteen-cell open-weight LM evaluation.","marker":"Qwen Team (2024)"},{"why":"Provides the tau-bench retail tools and live-agent dialogue environment used for the live-system validators and the live-agent probe.","marker":"Yao et al. (2024)"}],"fun_headline_variants":["Exact conditional sampling, but root CARS stays cheaper","Stateful CARS: exact reuse, no systems gain","Frozen schemas give exact draws, yet CARS cheaper","Exact LLM-agent sampling, efficiency still with CARS","Exact stateful rejection, but official CARS wins steps"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The result rests on being able to read off the exact probability the language model assigns to every reachable full history and on proving each stored schema non-completable for every reachable history in its abstract class—obligations the paper verifies only on enumerable bounded workflows, not on free-form tasks.","fun_headline_variants_meta":{"raw":{"variants":["Exact conditional sampling, but root CARS stays cheaper","Stateful CARS: exact reuse, no systems gain","Frozen schemas give exact draws, yet CARS cheaper","Exact LLM-agent sampling, efficiency still with CARS","Exact stateful rejection, but official CARS wins steps"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000232,"raw_usage":{"total_tokens":1583,"prompt_tokens":1133,"completion_tokens":450,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":749,"completion_tokens_details":{"reasoning_tokens":366}},"tokens_in":749,"tokens_out":450,"duration_ms":4438,"temperature":1.0,"reasoning_tokens":366,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T00:11:42.109965+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"On any finite enumerable workflow with an enumerated target $P_\\theta(\\cdot \\mid C)$, run Stateful CARS while memoizing residuals by abstract state alone instead of by complete serialized history plus matcher state; if the accepted law differs from the enumerated conditional by more than sampling noise, the distinct-history cache requirement of Proposition 5 fails. Alternatively, build two reachable histories with the same abstraction but different future-validity continuation languages, store a schema certified at one of them, and check that the sampled TV to the target equals $P_\\theta(E \\mid C)$, the exact false-exclusion cost of Proposition 10.","supporting_citations":[],"review_version":1}