Pith. sign in

REVIEW 2 major objections 3 minor 12 references

Stateful CARS: Exact Cross-History Reuse for Policy-Constrained LLM Agents

T0 review · 2 major / 3 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2608.08282 v1 pith:K6R2DD2C submitted 2026-08-08 cs.LG

Ibne Farabi Shihab , Md Najmus Swaqeeb , Abu Sa-Adat Mohamed Moon-Im Al Ahsan This is my paper · ORCID
classification cs.LG
keywords constraineddecodingstatefulvalidatorsLLMagentsrejectionsamplingDoobtransformschemareuseexactconditionalfuture-validitybisimulation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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$]).

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 3 minor

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.

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 (2)
  1. [§8 vs. §4.2, Appendix U, Table 22] 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.
  2. [§8 vs. Appendix N.1 (Table 18) and Conclusion] 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.
minor comments (3)
  1. [Abstract and §8] 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.
  2. [Appendix G] 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.
  3. [Appendix Q and §6.2] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the exactness proof is a self-contained telescoping argument, and the numerical matches are independent enumerative verifications rather than fitted predictions.

full rationale

The paper's central derivation is not circular. Lemma 6 proves the residual proposal Q_E(a|h)=pi_theta(a|h) r_E(Succ(h,a))/r_E(h) produces P_theta(tau|E^c) by telescoping residual ratios; this is a standard identity and does not assume the target. Theorem 8 then follows from sound schemas (Lemma 7) and a fixed exclusion event per attempt, with the bank update measurable with respect to the past but not altering the conditional law. The controlled experiments verify exactness by two independent enumerations: the target P_theta(tau|C) is obtained by enumerating the complete action tree, and the proposal's analytic law is obtained by enumerating the frozen excluded event; the reported 1e-16 agreement is an implementation conformance check, not a fit. The evaluated method's efficiency claims are honestly negative, and the enumerability scope of verification is stated as a limitation rather than disguised as a universal guarantee. No load-bearing self-citation chain, imported uniqueness theorem, or ansatz-smuggling-by-citation appears; references to prior CARS work are external and used as baselines. Accordingly, the paper's derivation is self-contained and warrants a circularity score of 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The exactness theorem is conditional on exact policy scoring, a validity-preserving abstraction with sound schemas, and a finite deterministic setting. Those are verified only on enumerable bounded workflows; no free parameter is fitted to the target. The scaling exponents are post-hoc measurements.

assumptions (4)
  • domain assumption Exact full-history policy probabilities are available for every reachable node.
    Correctness section and Eq. 4 require these; for LLMs they are implemented as float64 softmax over restricted label logits, which is an approximation (Appendix Q). This is the load-bearing premise for the exact residual recursion.
  • ad hoc to paper The abstraction phi is validity-preserving and every committed schema is sound for every world consistent with the abstraction.
    Lemma 7 and Proposition 10 make soundness a necessary condition; the paper verifies it by exhaustive enumeration on bounded workflows (Appendix S, Tables 8, 20) and leaves free-form tasks unverified.
  • domain assumption Finite horizon, finite action alphabet, and deterministic environment.
    Section 3 defines the setting; stochastic outcomes require a residual-reweighted prior and are handled in Appendix G, and infinite domains break the recursion.
  • ad hoc to paper The schema bank is frozen within each attempt and compression preserves the induced exclusion event.
    This design choice is required by Lemma 6 and Theorem 8; the audit in Table 7 checks it for the implementation.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Stateful CARS: Exact Cross-History Reuse for Policy-Constrained LLM Agents." pith.science (2026). https://pith.science/paper/K6R2DD2C

@misc{pith2026260808282,
  author       = {Pith},
  title        = {Pith review of: Stateful CARS: Exact Cross-History Reuse for Policy-Constrained LLM Agents},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/K6R2DD2C}},
  note         = {Machine review of arXiv:2608.08282}
}
abstract

Tool-using language-model agents face constraints whose meaning changes with observations and prior actions. We study exact sampling from the model distribution conditioned on a hard stateful validator while reusing invalidity certificates across histories. Stateful CARS freezes a bank of sound state--continuation schemas within each attempt and removes every trajectory containing a certified continuation at a matching abstract state. An exact residual Doob transform samples from the resulting proposal. We give a checkable future-validity bisimulation condition, prove schema soundness, adaptive exactness, i.i.d.\ outputs, almost-sure termination, monotone acceptance, and compression invariance, and characterize computation by the number of reachable full-history product states. This number can be exponential for a history-dependent language model; the evaluated method therefore makes no generic finite-trie scalability claim. On enumerable workflows, its analytic law matches the valid conditional to $10^{-16}$ at validity probability $6\times10^{-8}$, whereas state-aware local decoding can be $0.97$ away. A matched comparison is negative: observation-keyed official CARS is cheaper in sampler steps (root/Stateful ratio $0.942$ $[0.934,0.951]$), and the Qwen comparison is null ($0.99$ $[0.90,1.08]$). Cross-history transfer helps only in an internal matched-key ablation ($1.27\times$). Thus the evidence supports exact schema-induced conditioning, not a systems advantage over CARS.

Figures

Figures reproduced from arXiv: 2608.08282 by the authors.

Figure 1
Figure 1. Evaluated Stateful CARS. A frozen schema [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Evaluated schema-induced Stateful CARS with the matched official update. The bank fixes the exclusion event before the first proposal action and changes only after final validation. The post-invalid￾only arm reported in Appendix N is an ablation, not Algorithm 2. The visited-grounding finite-trie alterna￾tive in §4 uses a different exclusion event; it is a separate construction, evaluated on its own terms in Appendi… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

12 extracted references · 7 canonical work pages

  1. [1]

    Initialize the schema bankB ← ∅

    work page

  2. [2]

    At the start of attempt k, freeze B ← Band initialize a pending schema set∆← ∅

    work page

  3. [3]

    Preprint, arXiv:2504.05410

    Fast controlled generation from language models with adaptive weighted rejection sampling. Preprint, arXiv:2504.05410. Xiao Liu, Hao Yu, Hanchen Zhang, Yifan Xu, Xuanyu Lei, Hanyu Lai, Yu Gu, Hangliang Ding, Kaiwen Men, Kejuan Yang, Shudan Zhang, Xiang Deng, Ao- han Zeng, Zhengxiao Du, Chenhui Zhang, Sheng Shen, Tianjun Zhang, Yu Su, Huan Sun, and 3 others

    arXiv

  4. [4]

    If a sound monitor proves that the realized prefix has no valid completion, terminate the attempt as invalid; otherwise continue to a terminal trajectory and apply VALIDATE

    work page

  5. [5]

    Paweł Parys, Sairam Vaidya, Taylor Berg-Kirkpatrick, and Loris D’Antoni

    Grammar-aligned decoding.Preprint, arXiv:2405.21047. Paweł Parys, Sairam Vaidya, Taylor Berg-Kirkpatrick, and Loris D’Antoni. 2025. Constrained adaptive rejection sampling.Preprint, arXiv:2510.01902. Shishir G. Patil, Tianjun Zhang, Xin Wang, and Joseph E. Gonzalez. 2023. Gorilla: Large lan- guage model connected with massive apis.Preprint, arXiv:2305.153...

    arXiv 2025

  6. [6]

    cannot see

    Commit B ←κ(B ∪∆), with Eκ(B∪∆) =E B∪∆. If the completed trajectory was valid, yield it. Repeat for further samples. Figure 2: Evaluated schema-induced Stateful CARS with the matched official update. The bank fixes the exclusion event before the first proposal action and changes only after final validation. The post-invalid- only arm reported in Appendix ...

    work page

  7. [8]

    Com- pute rB by memoized recursion keyed by the com- plete serialized history and matcher state, and sample the attempt from QB in Equation (4)

    Construct the fixed event EB from Equation (2). Com- pute rB by memoized recursion keyed by the com- plete serialized history and matcher state, and sample the attempt from QB in Equation (4). Do not mutate Bor the residual cache’s defining event

    work page

  8. [10]

    Add (z, u)to ∆ only when CERTIFYproves u /∈L(h′) for every reachable h′ with ϕ(h′) =z

    After the attempt ends, inspect every visited proper prefix and its invalid siblings. Add (z, u)to ∆ only when CERTIFYproves u /∈L(h′) for every reachable h′ with ϕ(h′) =z . This official update is run after valid and invalid attempts. A failure observed in one concrete world is not a schema proof

    work page

Show all 12 references
  1. [15]

    this action is dead

    Appendix P gives the setup, statistics, and the reasons we draw no systems conclusion. M Reuse-Only Ablation Comparing against root-prefix CARS changes the certificate key and the per-attempt bookkeeping Sampler Calls/validTV(95% CI) Exact? Batched terminal reject.† 1557.5 0.0...

    2025

  2. [2023]

    Leonardo de Moura and Nikolaj Bjørner

    Prompting is programming: A query language for large language models.Proceedings of the ACM on Programming Languages, 7(PLDI):1946–1969. Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. InTools and Algorithms for the Construction and Analysis of System...

    1946 arXiv

  3. [2024]

    In The Twelfth International Conference on Learning Representations

    AgentBench: Evaluating LLMs as agents. In The Twelfth International Conference on Learning Representations. Yanming Liu, Xinyue Peng, Jiannan Cao, Xinyi Wang, Songhang Deng, Jintao Chen, Jianwei Yin, and Xuhong Zhang. 2026. ToolGate: Contract-grounded and verified tool executi...

    2026 arXiv

  4. [2025]

    Sooyeon Kim, Giung Nam, Byoungwoo Park, and Juho Lee

    Enforcing temporal constraints for LLM agents.Preprint, arXiv:2512.23738. Sooyeon Kim, Giung Nam, Byoungwoo Park, and Juho Lee. 2025. Improving constrained language genera- tion via self-distilled twisted sequential monte carlo. Preprint, arXiv:2507.02315. Benjamin Lipkin, Ben...

    2025

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.