Correctness-Guaranteed Code Generation via Constrained Decoding

Lingxiao Li; Salar Rahili; Yiwei Zhao

REVIEW 4 major objections 5 minor 1 cited by

Correctness-Guaranteed Code Generation via Constrained Decoding

T0 review · 4 major / 5 minor · reviewed 2026-08-05 · deepseek-v4-flash

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

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

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

arxiv 2508.15866 v1 pith:RE5AQ2P3 submitted 2025-08-20 cs.PL cs.LGcs.SE

Lingxiao Li , Salar Rahili , Yiwei Zhao This is my paper

classification cs.PLcs.LGcs.SE

keywords constraineddecodingcodegenerationsemanticcorrectnesstreeofparserscontext-sensitiveparsingtokenhealingruntimesLua

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

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.

What carries the argument

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

What would settle it

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

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

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

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.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the 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.

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

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

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

Referee Report

4 major / 5 minor

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.

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 (4)

[Section 3, Algorithm 1; Section 4, 'Satisfying the non-extensible match property'; Appendix A.2] 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 5; Theorem 5.1; Section 1 claims] 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
[Appendix C.5, proof of Theorem 6.1] 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 1, Abstract; Appendix C.9; Section 6.2] 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.

minor comments (5)

[Appendix C.10.3, Example C.15] 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.
[Appendix C.2] 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.
[Appendix B.2.6] 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 6.2, Figure 3] 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 4, 'Get next regex'] 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.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity; the central guarantee is by construction of the ToP and is conditional on unproven Assumption A1, but no fitted input is repackaged as a prediction.

full rationale

Algorithm 1 maintains an invariant: each generated segment is matched against a regex supplied by parser P and is then fed back into P, so acceptance by the ToP follows by construction. That is not circular in the damaging sense, because the ToP is a hand-built artifact embodying modular CFGs plus scope/type environment, not a parameter fitted to make a benchmark pass. The sLua correctness claim is internal—correctness is operationalized as parseability by the ToP—but the DCI game-engine runtime validation and Theorem 6.1's structural argument (API design, no nil, no unbounded recursion, bounded loops) give independent external content. The main flagged caveat is a correctness gap rather than circularity: Assumption A1 (non-extensible regexes) is load-bearing for Algorithm 1's stopping rule and token healing, and the paper explicitly defers its enforcement, saying in Appendix A.2 that the lookahead strategy is 'Not included in Algorithm 2' and 'needs to be applied on a case-by-case basis depending on the specific CFGs and the child parsers.' No global proof is supplied that every regex produced by the sLua ToP satisfies A1. Nontermination of Algorithm 1 is also acknowledged in Section 7 and Appendix C.9. These are unproven assumptions or limitations, not the equivalence-by-construction or fitted-input patterns of circularity. There are no load-bearing self-citations, and no known result is merely renamed as a new derivation.

Assumptions & free parameters 4 free parameters · 7 assumptions · 2 invented entities

The system's guarantees depend on hand-chosen caps and design assumptions, and the ToP's characterization of semantic correctness is internal to the paper.

free parameters (4)

loop iteration cap = 100
Hand-chosen constant capping while-loop iterations to guarantee termination (Appendix C.5). Central to Theorem 6.1's termination guarantee.
effect hook recursion cap = 3
Stops triggering new hooks when callstack has 3 hooks to prevent infinite recursion (Appendix C.5). Required for runtime termination.
maximum variable name length = 50
Limits CFG template size so node spawning is constant time (Appendix B.2.2, Theorem 5.1 proof).
output token failure limit = 1500
Experimental threshold beyond which generation is counted as failed (nontermination) in Section 6.2.

assumptions (7)

ad hoc to paper Assumption (A1): any regex returned by P.next regex() is non-extensible (no extension of a match still matches).
Stated in Section 3 as an imposed requirement; the sLua ToP is claimed to satisfy it via a look-ahead strategy applied case-by-case, but no general proof is provided (Section 4, Appendix A.2).
ad hoc to paper Assumption (A3): a terminal that is a placeholder or violates A1 in a modular CFG must be followed by non-placeholder terminals satisfying A1.
Stated in Section 4 as the basis for the look-ahead strategy; sLua enforces it by requiring semicolons and other delimiters.
ad hoc to paper Assumption (A2): broom-shaped ToP, when a node spawns more than one child, all ancestors have only one child.
Stated in Section 4; Lemma B.1 claims sLua ToP satisfies it, used in Theorem 5.1.
domain assumption The DCI API is safe: for any type-checking inputs, API calls terminate without runtime errors.
Used in proof of Theorem 6.1; asserted in Appendix C.5 but not formally verified.
domain assumption Number of variables in scope, nested function calls, and scopes are bounded by a constant during parsing.
Assumption in Theorem 5.1 for the linear-time parsing guarantee.
domain assumption The modular CFG templates in Appendix B.2 exactly characterize the intended sLua semantics (type-correct, in-scope, API-conforming programs).
Implicit assumption: the ToP's accepted language is taken to define 'semantically correct'; no soundness/completeness theorem with respect to an external semantics is proved.
domain assumption The Lua runtime (lupa) with modified metatables executes translated sLua as specified, including auto-passing self for method calls.
Required for Theorem 6.1 to transfer from sLua to executed Lua; stated in Example B.1 and Appendix C.2.

invented entities (2)

sLua
purpose: Strongly typed subset of Lua designed to make semantic parsing tractable and runtime correctness provable.
A constructed language introduced by the paper; its only specification is in the paper and appendices. Executable examples appear in the paper but no external implementation is shipped.
Tree of Parsers (ToP)
purpose: Dynamic tree of context-enriched CFG parsers whose root produces non-extensible regexes to guide constrained decoding.
A software framework described in the paper; no released code or formal machine-checked implementation.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Correctness-Guaranteed Code Generation via Constrained Decoding." pith.science (2026). https://pith.science/paper/RE5AQ2P3

@misc{pith2026250815866,
  author       = {Pith},
  title        = {Pith review of: Correctness-Guaranteed Code Generation via Constrained Decoding},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RE5AQ2P3}},
  note         = {Machine review of arXiv:2508.15866}
}

read the original abstract

Language Models (LMs) are increasingly being used for code generation, but ensuring the correctness of generated programs remains a significant challenge. Although imperfect code may be acceptable during software development with human oversight, domains such as video games and robotics require one-shot correctness for runtime-critical components. We present a constrained decoding algorithm for generating semantically correct programs that incorporates a context-sensitive parser, which, at each step, outputs a regular expression that satisfies a critical non-extensible property to guide the generation of the next token sequence that can continue to a correct program. To build such a context-sensitive parser, we propose a framework of a dynamic tree of parsers (ToP) during parsing, where each parser corresponds to a modular context-free grammar enriched with contextual information such as variable scopes and type constraints, with tree branches representing ambiguity in the future code segment. We demonstrate our approach through sLua, a strongly typed variant of Lua, showing that our method can generate semantically correct programs conforming to any prescribed scripting API. We further show that, with careful design, our semantic guarantees extend to runtime correctness, as validated in the application of generating game mechanics for a roguelike video game.

Figures

Figures reproduced from arXiv: 2508.15866 by the authors.

**Figure 2.** Illustration of token healing for a code segment in the talent script of DCI (Sec [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

**Figure 3.** Histogram on talent category scores for various methods. For each of the 8 tal [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗

Figures from the paper (3 more)

**Figure 4.** Figure 4: Left: starting screen for DCI before entering an adventure prompt. Right: gener [PITH_FULL_IMAGE:figures/full_fig_p024_4.png]

**Figure 5.** Figure 5: Left: quest panel that shows the story, the main quest, and a list of enemies in the [PITH_FULL_IMAGE:figures/full_fig_p024_5.png]

**Figure 6.** Figure 6: Left: character progression screen. Right: candidate talents to evolve given a text [PITH_FULL_IMAGE:figures/full_fig_p025_6.png]

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

The Alignment Problem in Constrained Code Generation
cs.SE 2026-06 unverdicted novelty 7.0 of 10

Incomplete constrainers in constrained decoding push LLMs into low-probability program regions, making unconstrained decoding outperform constrained decoding on functional correctness across seven models and three benchmarks.

Reference graph

Works this paper leans on

17 extracted references · 11 canonical work pages · cited by 1 Pith paper

[1]

GlobalString: doc: | String library

RandomInt: | (low: number, high: number) −> number Get a random integer in [low, high −1]. GlobalString: doc: | String library. Do not use string functions not present in this ,→ table. Use ”..” to concatenate strings. fields: from num: | (num: number) −> string Convert a number to a string rounded to the nearest integer. It is by design to never have a d...

work page 2025
[2]

Xgrammar: Flexible and efficient structured generation engine for large language models

Yixin Dong, Charlie F Ruan, Yaxing Cai, Ruihang Lai, Ziyi Xu, Yilong Zhao, and Tianqi Chen. Xgrammar: Flexible and efficient structured generation engine for large language models. arXiv preprint arXiv:2411.15100,

arXiv
[3]

B Details on sLua Language and Parsing B.1 sLua Language Here are the main differences between sLua and Lua: • Statements must end in

of using a context-sensitive parser with interface described in Section 3 to parse a complete or incomplete program. B Details on sLua Language and Parsing B.1 sLua Language Here are the main differences between sLua and Lua: • Statements must end in ;. This is to simplify the parsing algorithm to satisfy Assump- tion (A3) by having natural boundaries bet...

work page 2025
[6]

an aquatic adventure as a seal warrior

triggers on-the-fly code generation given a player’s text prompt, and the player can choose from one of the three generated talents. All the game UI follows a minimalist design, with texts replacing textures whenever they would normally be needed (e.g., each actor is a moving text). Figure 4: Left: starting screen for DCI before entering an adventure prom...

work page 2025
[7]

Synchromesh: Reliable code generation from pre-trained language models

Gabriel Poesia, Oleksandr Polozov, Vu Le, Ashish Tiwari, Gustavo Soares, Christopher Meek, and Sumit Gulwani. Synchromesh: Reliable code generation from pre-trained language models. arXiv preprint arXiv:2201.11227,

arXiv
[8]

Efficient guided generation for llms

Brandon T Willard and R ´emi Louf. Efficient guided generation for llms. arXiv preprint arXiv:2307.09702,

arXiv
[12]

C.3 API for DCI Below is the scripting API for DCI

for the indexing step and irregular5 to construct finite deterministic automata (DFA), en- abling efficient constrained generation of syntactically valid code. C.3 API for DCI Below is the scripting API for DCI. The implementation of the API in the game engine ensures that regardless of the game state, as long as the API call sites type check, the API cal...

work page 2025
[14]

ensures that only variables in scope and only predefined fields in a table will be accessed, all memory access is valid in the generated code. Furthermore, the API in Appendix C.3 is designed so that for any input arguments, as long as they type check (as guaranteed again by Algorithm 1), the API calls will not raise any runtime error. Therefore, it remai...

work page 2025

Show all 17 references

[15]

C.10.1 Unconstrained (Claude-3.5-Sonnet) with or without Reflection Example C.3 (Incorrect expression type)

In case of parsing error, we will use red to indicate the part that the sLua context-sensitive parser failed to parse, and provide the regex returned from the next regex function that the next part needs to match against. C.10.1 Unconstrained (Claude-3.5-Sonnet) with or withou...

2025
[16]

but we do not allow such syntax. local function GetHealAmount(user: Actor): number return g math.Floor(GetHealingFactor(user) * user.attack power / 10); end; 34 Published as a conference paper at COLM 2025 The red part failed to match regex: \s*([a−zA−Z ]\w{0,49 }\s*:) C.10.2 ...

2025
[17]

We show a few failure cases here

are due to nontermination of the genera- tion. We show a few failure cases here. Example C.15 (Intend for comments but parsed as operators) . As we have seen in Exam- ple C.13, despite prompt instruction, Qwen2.5-32B-Coder can still output comments sometimes. While constrained...

2025
[2001]

Binyuan Hui, Jian Yang, Zeyu Cui, Jiaxi Yang, Dayiheng Liu, Lei Zhang, Tianyu Liu, Jiajun Zhang, Bowen Yu, Keming Lu, et al. Qwen2. 5-coder technical report. arXiv preprint arXiv:2409.12186,

arXiv
[2018]

While this poses some restrictions on the allowed CFGs, most programming languages can be rewritten in a CFG that belongs to LALR(1)

for its linear time complexity and ease of use. While this poses some restrictions on the allowed CFGs, most programming languages can be rewritten in a CFG that belongs to LALR(1). A.2 Implementation of ToP We use an object-oriented approach to define classes for the parser n...

2025
[2019]

Openfst: A general and efficient weighted finite-state transducer library: (extended ab- stract of an invited talk)

Cyril Allauzen, Michael Riley, Johan Schalkwyk, Wojciech Skut, and Mehryar Mohri. Openfst: A general and efficient weighted finite-state transducer library: (extended ab- stract of an invited talk). In Implementation and Application of Automata: 12th International Conference, ...

2007
[2021]

Automata-based constraints for language model decoding

Terry Koo, Frederick Liu, and Luheng He. Automata-based constraints for language model decoding. arXiv preprint arXiv:2407.08103,

arXiv
[2023]

Type-constrained code generation with language models

11 Published as a conference paper at COLM 2025 Niels M ¨undler, Jingxuan He, Hao Wang, Koushik Sen, Dawn Song, and Martin Vechev. Type-constrained code generation with language models. Proceedings of the ACM on Pro- gramming Languages, 9(PLDI):601–626,

2025
[2024]

Kanghee Park, Jiayu Wang, Taylor Berg-Kirkpatrick, Nadia Polikarpova, and Loris D’Antoni

URL https://platform.openai.com/docs/guides/ structured-outputs. Kanghee Park, Jiayu Wang, Taylor Berg-Kirkpatrick, Nadia Polikarpova, and Loris D’Antoni. Grammar-aligned decoding. arXiv preprint arXiv:2405.21047,

Pith tools

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

[1] [1]

GlobalString: doc: | String library

RandomInt: | (low: number, high: number) −> number Get a random integer in [low, high −1]. GlobalString: doc: | String library. Do not use string functions not present in this ,→ table. Use ”..” to concatenate strings. fields: from num: | (num: number) −> string Convert a number to a string rounded to the nearest integer. It is by design to never have a d...

work page 2025

[2] [2]

Xgrammar: Flexible and efficient structured generation engine for large language models

Yixin Dong, Charlie F Ruan, Yaxing Cai, Ruihang Lai, Ziyi Xu, Yilong Zhao, and Tianqi Chen. Xgrammar: Flexible and efficient structured generation engine for large language models. arXiv preprint arXiv:2411.15100,

arXiv

[3] [3]

B Details on sLua Language and Parsing B.1 sLua Language Here are the main differences between sLua and Lua: • Statements must end in

of using a context-sensitive parser with interface described in Section 3 to parse a complete or incomplete program. B Details on sLua Language and Parsing B.1 sLua Language Here are the main differences between sLua and Lua: • Statements must end in ;. This is to simplify the parsing algorithm to satisfy Assump- tion (A3) by having natural boundaries bet...

work page 2025

[4] [6]

an aquatic adventure as a seal warrior

triggers on-the-fly code generation given a player’s text prompt, and the player can choose from one of the three generated talents. All the game UI follows a minimalist design, with texts replacing textures whenever they would normally be needed (e.g., each actor is a moving text). Figure 4: Left: starting screen for DCI before entering an adventure prom...

work page 2025

[5] [7]

Synchromesh: Reliable code generation from pre-trained language models

Gabriel Poesia, Oleksandr Polozov, Vu Le, Ashish Tiwari, Gustavo Soares, Christopher Meek, and Sumit Gulwani. Synchromesh: Reliable code generation from pre-trained language models. arXiv preprint arXiv:2201.11227,

arXiv

[6] [8]

Efficient guided generation for llms

Brandon T Willard and R ´emi Louf. Efficient guided generation for llms. arXiv preprint arXiv:2307.09702,

arXiv

[7] [12]

C.3 API for DCI Below is the scripting API for DCI

for the indexing step and irregular5 to construct finite deterministic automata (DFA), en- abling efficient constrained generation of syntactically valid code. C.3 API for DCI Below is the scripting API for DCI. The implementation of the API in the game engine ensures that regardless of the game state, as long as the API call sites type check, the API cal...

work page 2025

[8] [14]

ensures that only variables in scope and only predefined fields in a table will be accessed, all memory access is valid in the generated code. Furthermore, the API in Appendix C.3 is designed so that for any input arguments, as long as they type check (as guaranteed again by Algorithm 1), the API calls will not raise any runtime error. Therefore, it remai...

work page 2025