{"id":"73080ed7-6b5e-4bad-8c6e-5d966e97cd5e","arxiv_id":"2508.15866","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"A constrained decoding algorithm using a context-sensitive tree of parsers guarantees generated programs in the sLua language are semantically correct and, for the game API, run without errors.","lead":"A new decoding method steers a language model to only output code that passes a live type-and-scope checker built as a tree of parsers, so every finished program is guaranteed to be valid in a custom scripting language. The authors demonstrate this by generating error-free game mechanics for a roguelike, where a failed script would crash the game.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Assumption A1 (non-extensible regexes) is unproven for the sLua ToP; Algorithm 1's stopping rule and token healing depend on it, so the central correctness guarantee is conditional.","rationale":"The reader's weakest_assumption identifies the same load-bearing concern: Assumption A1 is not proven for the regexes produced by the sLua ToP. This is the right focus because A1 is the mechanism that makes incremental decoding with token healing deterministic: without it, the DFA can be in a final state and still accept more input, so the algorithm's stopping condition is not sound. The paper's own appendix explicitly defers A1 to 'case-by-case' application, and Algorithm 2's comment leaves the lookahead out of the pseudocode. This is an internal correctness gap rather than a disagreement with external consensus, so it is a legitimate condition to place on the central claim. The paper has real independent support: a detailed ToP construction, a linear-time parsing theorem, and experiments that isolate failure modes; these make the approach plausible but do not close the A1 gap. The reader's CONDITIONAL verdict is therefore appropriate: the contribution is promising, but the strong correctness guarantee should be accepted only after A1 is either proven for the sLua ToP or verified by exhaustive runtime checking. I would not escalate to REJECT because the failure case is concrete and testable, and the paper is honest about its limitations; I would not lower to ACCEPT because the central theorem is conditional on an unproven assumption. Thus the verdict remains UNCHANGED from the reader's CONDITIONAL.","tokens_in":28855,"tokens_out":8712,"duration_ms":112198,"concrete_test":"Instrument Algorithm 1 so that every regex returned by P.next_regex() is checked for A1 before the prefix/'.*' modification: build the DFA, then run a graph search for any accepting state reachable from an accepting state via a non-empty path (decidable for regular languages). Run this check across (1) all 80 DCI talent/effect generations reported in §6.2, and (2) a fuzz suite of thousands of partial sLua programs that exercise multi-child ToP states, prefix expressions, type specs, and keyword boundaries. If any regex fails the check, A1 is violated and the central guarantee is refuted. If no failure occurs, A1 is supported for tested paths but still not proven for all inputs; a rigorous proof would need to formalize the lookahead construction and show it preserves non-extensibility through union and child composition.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central guarantee—that programs generated by Algorithm 1 are accepted by the ToP—rests on Assumption A1: no regex returned by P.next_regex() matches a string that can be extended to another match. A1 is what makes the decoder stop at a final DFA state and makes token healing reliable. The paper does not prove A1 for the constructed sLua ToP. Section 4 says a look-ahead strategy is 'recommended' and Appendix A.2 states that the strategy 'needs to be applied on a case-by-case basis depending on the specific CFGs and the child parsers.' No global argument or theorem shows that every regex produced by the sLua ToP satisfies A1. The gap is not merely aesthetic: even if each child regex is non-extensible, the union of child regexes in Algorithm 2 need not be (e.g., R1='ab', R2='abc' is a violation), and union is performed when multiple children exist. If A1 fails, the DFA in Algorithm 1 can be in a final state with further accepting transitions; the decoder may stop a segment early, misattribute a suffix in token healing, and feed the parser a string that does not correspond to a valid continuation. The paper even acknowledges this risk by not including the lookahead in the BaseParser pseudocode. Thus, the claimed correctness guarantee is not established, only assumed for the demonstrated system.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a constrained decoding algorithm (Algorithm 1) that uses a context-sensitive parser implemented as a dynamic Tree of Parsers (ToP). The parser emits at each step a regular expression satisfying a non-extensibility property (Assumption A1), which lets the decoder stop segment generation and heal token boundaries. The ToP is built from modular CFG templates enriched with scope and type information, and the framework is instantiated for sLua, a strongly typed Lua variant. The authors claim that Algorithm 1 generates semantically correct sLua programs, preserves the ability to generate all semantically correct programs, and, for DCI talent/effect scripts, guarantees termination and runtime-error-free execution (Theorem 6.1). They report a game application and experiments comparing their method with unconstrained baselines.","tokens_in":29306,"tokens_out":3446,"duration_ms":44851,"significance":"If the guarantees were fully established, the paper would make a valuable contribution to constrained decoding: it moves from syntactic to semantic correctness by incorporating contextual information incrementally, and it includes a token-healing procedure that addresses a real practical issue. The use of adaptive rejection sampling is pragmatic and the runtime validation in a game environment gives evidence that the system works. The paper is also transparent about nontermination and distribution distortion. However, the central formal claim is currently conditional on an unverified property (A1) and on the ToP correctly formalizing sLua semantics; the empirical results are consistent with the approach but do not replace the missing proofs.","major_comments":[{"comment":"Assumption (A1) is load-bearing: Algorithm 1's stopping rule (the inner while loop checking final DFA states) and the token-healing logic both require that no regex returned by P.next_regex() matches a string and any extension of it. The paper does not prove that the sLua ToP satisfies A1. Section 4 says a look-ahead strategy is 'recommended', and Appendix A.2 explicitly states it 'needs to be applied on a case-by-case basis'. Algorithm 2, which defines BaseParser.next_regex, omits the look-ahead entirely. Moreover, even if every child regex satisfies A1, the union of child regexes in Algorithm 2 (the regexes.append(child.next_regex()) loop and the final join) can violate it: R1='ab' and R2='abc' is a counterexample. The text notes some concrete cases (e.g., Actor vs ActorInfo, user.power vs user.powerups) but gives no global argument covering all terminals in all sLua node classes. With","section":"Section 3, Algorithm 1; Section 4, 'Satisfying the non-extensible match property'; Appendix A.2"},{"comment":"The paper claims that the method generates 'semantically correct' programs and 'preserves the ability to generate all possible semantically correct programs', but no formal semantics for sLua is given and no soundness/completeness theorem relating ToP acceptance to semantic validity is proved. Theorem 5.1 is only a linear-time parsing statement under bounded scope; it says nothing about whether the ToP accepts exactly the semantically correct programs. Without such a theorem, 'correctness-guaranteed' is internal to the parser rather than a guarantee about the language or the API. I recommend stating the intended semantics (e.g., via a type system or translation to Lua) and proving that (a) every program accepted by the ToP is semantically valid, and (b) every semantically valid program can be produced by some path in the ToP. The current appendix gives parser grammar details but no such","section":"Section 5; Theorem 5.1; Section 1 claims"},{"comment":"The runtime guarantee depends on an unverified assumption about the external engine: 'the API in Appendix C.3 is designed so that for any input arguments, as long as they type check ... the API calls will not raise any runtime error.' The theorem statement says 'Given the API in Appendix C.3 ... scripts ... are guaranteed to terminate and execute without runtime errors', but the proof does not verify the API implementation; it takes the API's total correctness as an axiom. This should be made an explicit assumption in the theorem (e.g., 'Assuming the game engine implements the API as a total function on type-correct inputs'), or the API implementation must be verified. Additionally, the induction step 'any expression should terminate because any top-level function call inside can be a single smaller statement' is not fully formal; the paper should specify the induction measure and cover","section":"Appendix C.5, proof of Theorem 6.1"},{"comment":"Algorithm 1 is not guaranteed to terminate; the paper acknowledges this and the experiments count generations over 1500 tokens as failures. This does not contradict Theorem 6.1 (which is conditional on successful generation), but it conflicts with the headline claim of 'one-shot correctness' in the abstract. The paper should qualify the guarantee as applying only to terminating runs of Algorithm 1, and should state the termination issue prominently in the abstract or introduction. The current framing overstates what is actually proved.","section":"Section 1, Abstract; Appendix C.9; Section 6.2"}],"minor_comments":[{"comment":"The sentence 'This failure case can be treated if we only allow spaces inside an expression' appears to mean 'addressed' or 'fixed', not 'treated' in the medical sense. Please rephrase.","section":"Appendix C.10.3, Example C.15"},{"comment":"The reference to 'irregular' (https://github.com/MegaIng/interegular) has a typo: it is written as 'irregular' but the package is 'interegular'. This could confuse readers trying to reproduce the DFA construction.","section":"Appendix C.2"},{"comment":"The type specification grammar allows BASE_TYPE as a single terminal, and the look-ahead strategy is described in prose. A small example showing how the appended regex is constructed for a concrete case (e.g., Actor vs ActorInfo) would improve clarity.","section":"Appendix B.2.6"},{"comment":"The histogram combines 8 prompts with 10 runs each, but the paper does not report per-prompt variance. Since the claim is about success rate and quality across categories, a table with per-prompt success counts or confidence intervals would strengthen the evaluation.","section":"Section 6.2, Figure 3"},{"comment":"Algorithm 2 uses Python syntax and omits type annotations; more importantly, the 'look-ahead strategy' is not shown anywhere. Since it is central to A1, consider including a dedicated pseudocode or a worked example of how the look-ahead modifies a regex.","section":"Section 4, 'Get next regex'"}],"recommendation":"major_revision","confidential_remarks":"The paper is within scope for a conference on machine learning and programming languages, and the application to a real-time game is compelling. The main risk is that the formal guarantees are presented more strongly than what is proved: A1 is not established for the sLua ToP, and the runtime theorem rests on an external API correctness assumption. These are fixable with additional proofs or by making the assumptions explicit, so I do not recommend rejection. I would also encourage the authors to compare with Mündler et al. (2025) more concretely in the evaluation, since the concurrent work addresses similar prefix-automata construction."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Plain take: this is a solid systems paper, and the ToP construction is the real contribution. The authors show how to build an incremental context-sensitive parser that outputs regular expressions to guide an LM, with token healing for token boundaries, and they get a working game-script generation pipeline in a typed Lua variant. The empirical results are credible: compared to unconstrained Qwen and Claude, their method fails only by nontermination, and they are upfront about that failure mode and the distribution distortion that causes it. That honesty is real and worth crediting.\n\nThe main soft spot is exactly what the stress-test note says. Assumption A1 is load-bearing: the decoder stops when the DFA is in a final state, and token healing relies on it. The paper recommends a look-ahead strategy but explicitly says it must be applied case-by-case, and there is no proof that every regex generated by the sLua ToP satisfies A1. Worse, Algorithm 2 takes unions of child regexes, and non-extensibility is not preserved under union: `ab` and `abc` both match extensions of `ab`. So the guarantee that generated programs are accepted by the ToP is not actually established. It may well hold for the hand-built sLua parsers—the empirical results suggest it does—but the formal claim is weaker than advertised.\n\nTwo smaller points. First, no code or data is shipped, so the experiments can't be reproduced. Second, the runtime-correctness theorem is a consequence of API design (no nil, loop caps, recursion caps) plus type checking; that's a reasonable engineering tradeoff, but it shouldn't be oversold as a deep result. The 'semantic correctness' is also defined internally as acceptance by the ToP; that's acceptable because the ToP is a concrete artifact with external validation in the game, but readers should keep the distinction.\n\nBottom line: worth reading for anyone working on constrained decoding or code generation for embedded scripting. It deserves a serious referee. I'd ask the authors to either prove A1 for their constructed parsers or add a runtime check that asserts non-extensibility per regex, and to release the parser and evaluation scripts. With those, conditional accept.","headline":"A well-engineered constrained-decoding pipeline with a real game application, but the central correctness guarantee depends on an unproven assumption about the constructed regexes.","tokens_in":29678,"tokens_out":1962,"would_cite":true,"duration_ms":22390,"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":"Constrained decoding, steered by a context-sensitive parser emitting non-extensible regexes, can guarantee semantic correctness — not just syntax — and, for a restricted game-scripting language, proven termination with no runtime errors.","keywords":["constrained decoding","code generation","semantic correctness","tree of parsers","context-sensitive parsing","token healing","runtime correctness","sLua"],"falsifier":"Instrument the sLua implementation's next regex() and search for an A1 violation: put prefix-related names in scope (the paper itself names `do`/`do_it` and `power`/`powerups` as hazards) and check whether any returned regex matches both s and s·c for some character c. One such pair would let Algorithm 1 stop a segment early or advance the parser into a wrong state, breaking the guarantee. Complementary empirical check: rerun the paper's 8 talent-category prompts and measure the fraction of runs that exceed a fixed token budget — the paper reports all its failures are nontermination, so that r","tokens_in":28766,"feed_emoji":"✅","tokens_out":18029,"duration_ms":181396,"temperature":0.7,"pith_summary":"Constrained decoding forces a language model to produce text that obeys a grammar, but obeying a grammar is not the same as being correct: the code can still reference out-of-scope variables, call nonexistent functions, or crash at runtime. The paper's claim is that the constraint oracle can be promoted from a grammar to a context-sensitive parser that tracks scopes, types, and partial programs, and that at each step emits a pattern (regex) with a non-extensible property — once text matches, no extension of it matches. That property makes segment-by-segment generation safe: the decoder knows when a segment is complete, can repair tokens that straddle segment boundaries, and can treat the parser's acceptance of the finished program as proof of semantic correctness. The Tree of Parsers (ToP) builds such an oracle incrementally from modular grammars whose context slots (variables, types, allowed fields) are filled as generation proceeds, with ambiguity kept as branches that are pruned the moment they conflict with the code being written; in the strongly typed sLua dialect the tree stays compact, giving linear-time verification. The payoff, demonstrated on the Dungeon Crawl Infinite game, is one-shot code that is proven to terminate and run without errors, at the price of a deliberately restricted language — and the decoding loop, the paper notes, is itself not guaranteed to terminate.","feed_headline":"Prove code correct while the model writes it","feed_subtitle":"A parser tree checks scope and types at each step, so generated game scripts run error-free.","key_machinery":"The Tree of Parsers (ToP): a dynamic tree whose nodes are interactive parsers for modular CFG templates with context slots filled live — variables in scope, types, table fields, registered effect ids. Placeholder terminals spawn child parsers, a self-copy child keeps the parent continuation alive, and branches are pruned on conflict. Assumption (A1), non-extensible match, does the logical work: because no extension of a matched string can match again, the decoder can stop a segment, heal a straddling token, and advance parser state safely. A look-ahead strategy appends regexes for terminals that must follow a construct (semicolon, end, closing parenthesis) so every emitted regex satisfies A1","core_discovery":"Algorithm 1 couples a language model with a context-sensitive parser and generates only programs the parser accepts; for sLua, acceptance by the Tree of Parsers is semantic correctness, because the parser's nodes already encode scopes, types, allowed fields, and API signatures. The load-bearing property is Assumption (A1): each regex the parser emits is non-extensible — once a string matches, no extension matches — which makes segment stops and token healing safe. The paper also claims completeness (no semantically correct program is excluded) and, for the DCI API, Theorem 6.1: generated scripts terminate and run without runtime errors.","pith_inferences":["The non-extensible-regex requirement transfers to other domains: any DSL whose valid continuations end in explicit delimiters (closing brackets, terminators, keywords) could get the same segment-level semantic guarantee; the main cost is building the modular grammars, since Algorithm 1 and token healing apply unchanged.","Theorem 6.1's strength rests on expressiveness cuts — no nil, no dynamic tables, no recursion, capped loops. A testable extension: run a corpus of hand-written Lua game scripts through the sLua restrictions and measure how many require rewriting, quantifying the trade-off the paper only asserts.","The paper's own failures are all nontermination, and at the moment of failure the parser knows the exact pending regex; using that regex (or the last rejected token) as an explicit prompt hint or training signal is a concrete fix whose effect could be measured directly as a drop in the >1500-token failure rate.","The broom-shape condition doubles as a design rule for future languages: front-load type and scope information before expressions (as sLua's mandatory type annotations do), and the tree stays small — the criterion to check when porting the framework to another language."],"forward_implications":["Any sLua program produced by Algorithm 1 is accepted by the ToP, so it is semantically correct with respect to the prescribed scripting API — no separate verification pass at generation time.","For DCI talents and effects, every successfully generated script is guaranteed to terminate and run without runtime errors in the live game engine (Theorem 6.1).","The ToP's incremental acceptance check can serve as a dense reward signal for fine-tuning a language model to write semantically correct code, not just as a filter at decoding time.","The pipeline is practical: about 7.6 tokens/sec versus 2.0 and 1.5 tokens/sec for per-step token-DFA compilation baselines (Table 1), because adaptive rejection sampling avoids recompiling automata at each segment.","The method is complete as well as sound: every semantically correct sLua program remains generatable, so the constraints exclude no valid program."],"supporting_citations":[{"why":"The prior Synchromesh completion engine that returns valid continuations for partial programs but rechecks after every token; the contrast motivates the incremental design and Assumption (A1).","marker":"Poesia et al. (2022)"},{"why":"Concurrent type-constrained decoding via prefix automata; the closest comparison point, and the work this paper extends by adding runtime and termination guarantees.","marker":"Mündler et al. (2025)"},{"why":"Monitor-guided decoding with repository static analysis; its known failure to reject tokens that start valid but end invalid is exactly the misalignment that token healing fixes.","marker":"Agrawal et al. (2023)"},{"why":"The outlines implementation used for index-based guided generation inside Algorithm 1, and the primary speed baseline in Table 1.","marker":"Willard & Louf (2023)"},{"why":"Automata-based constraint decoding via finite-state transducers; used as the second baseline showing the compilation overhead of per-step token-level DFAs.","marker":"Koo et al. (2024)"},{"why":"Lark, the LALR(1) parser generator that produces every interactive parser node in the ToP and gives the linear-time parsing guarantee its implementation hook.","marker":"Shinan (2018)"},{"why":"Grammar-aligned decoding's expected-future-grammaticality analysis of distribution distortion; cited to ground the paper's own nontermination failure mode in the constrained-decoding literature.","marker":"Park et al. (2024)"},{"why":"The Gumbel-top-k trick that implements the adaptive rejection sampling step in Algorithm 1.","marker":"Kool et al. (2019)"},{"why":"Adaptive rejection sampling, the mechanism that makes the decoder fall back to unconstrained sampling whenever the first candidate token is valid.","marker":"Gilks & Wild (1992)"}],"fun_headline_variants":["Guaranteed-correct code: parser constrains each LM step","Tree of parsers forces AI to output error-free programs","Non-extensible regex: why generated scripts always run","Constrained decoding ensures semantic correctness in sLua","Parser-driven generation yields proven-correct game code"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"Every regex the parser emits must be non-extensible: if a string matches, no longer string with that string as a prefix may also match. Algorithm 1's stop rule and token healing both presume this, and the paper enforces it with a look-ahead strategy that Appendix A.2 concedes must be applied case-by-case — no global proof is given for the sLua parser.","fun_headline_variants_meta":{"raw":{"variants":["Guaranteed-correct code: parser constrains each LM step","Tree of parsers forces AI to output error-free programs","Non-extensible regex: why generated scripts always run","Constrained decoding ensures semantic correctness in sLua","Parser-driven generation yields proven-correct game code"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000294,"raw_usage":{"total_tokens":1533,"prompt_tokens":716,"completion_tokens":817,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":460,"completion_tokens_details":{"reasoning_tokens":737}},"tokens_in":460,"tokens_out":817,"duration_ms":8922,"temperature":1.0,"reasoning_tokens":737,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T18:08:01.896190+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Instrument the sLua implementation's next regex() and search for an A1 violation: put prefix-related names in scope (the paper itself names `do`/`do_it` and `power`/`powerups` as hazards) and check whether any returned regex matches both s and s·c for some character c. One such pair would let Algorithm 1 stop a segment early or advance the parser into a wrong state, breaking the guarantee. Complementary empirical check: rerun the paper's 8 talent-category prompts and measure the fraction of runs that exceed a fixed token budget — the paper reports all its failures are nontermination, so that r","supporting_citations":[],"review_version":1}