Flexible and Efficient Grammar-Constrained Decoding
Authors: Kanghee Park
Timothy Zhou
Loris D'Antoni
Venue: ICML 2025 poster (2025)
Keywords: Language Models
Decoding
Context-free Grammars
Primary area: applications->language_speech_and_dialog
TL;DR: This paper presents a novel approach to grammar-constrained decoding that significantly reduces preprocessing overhead while preserving state-of-the-art efficiency in online mask computation.

Abstract: Large Language Models (LLMs) are often asked to generate structured outputs that obey precise syntactic rules, such as code snippets or formatted data. Grammar-constrained decoding (GCD) can guarantee that LLM outputs matches such rules by masking out tokens that will provably lead to outputs that do not belong to a specified context-free grammar (CFG). To guarantee soundness, GCD algorithms have to compute how a given LLM subword tokenizer can ``align'' with the tokens used by a given context-free grammar and compute token masks based on this information. Doing so efficiently is challenging and existing GCD algorithms require tens of minutes to preprocess common grammars. We present a new GCD algorithm together with an implementation that offers 17.71x faster offline preprocessing than existing approaches while preserving state-of-the-art efficiency in online mask computation.

Flexible and Efficient Grammar-Constranne Decoding
Kanghee Park
Timothy Zhou' Loris D'Antoni
Abstract
ognized by a lexer in preprocessing phase, while the gram- matical structure of how terminals can be arranged e.g.. that the body of a loop should be sequence of statements is enforced by an automaton operating over lexed terminals. A key challenge with implementing GCD algorithms is that the tokens used by subword tokenizers in LLMs do not align with the terminals used by parsers.
Large Language Models (LLMs) are often asked to generate structured outputs that obey precise syntactic rules, such as code snippets or formatted data. Grammar--onstrrineed decoding (GCD) can guarantee that LLM outputs matches such rules by masking out tokens that will provably lead outputs that do not belong to specified context- free grammar (CFG). To guarantee soundness, GCD algorithms have to compute how given LLM subword tokenizer can "align" with the to- kens used by a given context-free grammar and compute token masks based on this information. Doing so efficiently is challenging and existing GCD algorithms require tens of minutes pre- process common grammars. We present new GCD algorithm together with an implementation that offers 17.71x faster offline preprocessing than existing approaches while preserving state-of-the- art efficiency in online mask computation.
Because of this misalignment, GCD approaches either incur high online token-masking overhead (>l second per token), or high offtine preprocessing costs (> 30 minutes) to precom- pute lookup table that relates LLM tokens to terminals (Beurer- et al., 2024; Ugare et al., 2024). Thus, ex- isting GCD algorithms are impractical for domains where the constraining grammar frequently changes. Examples of such domains include program synthesis (Alur et al., 2019), where a grammar is provided for every program one may try to synthesize, and grammar prompting (Wang et al., 2024), where grammars are predicted from a given prompt to then guide the LLM towards a particular output structure.
In this paper, we introduce a new approach for grammar- constrained decoding that is both flexible-iee. handles di- verse grammars without incurring prohibitive offline prepro- cessing costs-and efficient-i.c i... maintains state-of-the-at efficiency in online token masking. The key innovation is a combined analysis of the LLM token vocabulary and set of CFG terminals. The analysis efficiently precomputes a lexer-state-depee -tee--dpededdentttt mapping between sequences of CFG tokens and individual L.M tokens. This precomputation al- lows the decoder efficiently identify valid LLM tokens decoding time while avoiding wasteful processing of token combinations that are not realizable within the given LLM vocabulary.
1. Introduction
Constrained decoding guides the output of Large Language Models (LLMs) by greedily enforcing user-given constraints in highly structured settings. Granmar-constraine ing (GCD) (Geng et al., 2023) refers to the specific case where the constraint is given as a formal grammar that the LLM's output must conform to. This is done by applying parsing algorithms to build automaton that interfaces with the LLM's decoding algorithm to mask away all tokens that will provably lead to outputs not in the grammar. For example, GCD can be used to ensure that an LLM generates programs that only use a specific set of function names.
decod-
We implement our approach in a tool, GREATGRAMMA, which compares favorably to existing GCD approaches. GREATGRAMMA achieves an average 17.71x speedup in of- fline preprocessing compared to related approaches (Ugare et al., 2024) while maintaining state-of-the-an online mask- ing efficiency (5-32ms per token). Furthermore, our evalua- tion reveals that GCD implementations from existing pub- lished papers contain soundness bugs (e.g., they mask tokens that should not be masked or do not terminate when pre- processing simple grammars), whereas our approach lends itself to an elegant implementation consisting of simple
Parsing algorithms for Context-Free Grammars (CFG) achieve efficiency by processing input strings in two phases. Terminals- e.g., variable names string literals-are are rec-
DDepartment of Computer Science and Engineering, UCSD, San Diego USA. Correspondence to: Kanghee park <kap022@ucsd.cdd
Proceedings of the 42nd International Conference Machine Learning. Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

Flexible and Efficient Grammer-Constrangg Decoding
modules.
2.2. Using Parsing for Constrained Decoding
This paper makes two contributions:
We recall the general structure of a constrained decoder. When given a sequence of tokens ti CONSTRAINEDDE: CODING (Alg. in Appendix A) uses a checker C' during the decoding process to mask out any next token f&+1 that would result in a prefix (1:k+1 for which no possible com- plction satisfies the constraint. Specifically, given a prefix f1:k and vocabulary V C Σt, a checker C' computes a Boolean mask C(t V) = m E {0. 10,1,, where a value of 1 denotes viable token (i.e., one for which there exists sentence completion that can lead to constraint satisfaction), and O denotes an invalid one (i.e., one for which no sen- tence completion can lead to constraint satisfaction). The mask is then applied to the logits (Deutsch et al., 2019) produced by the language model to exclude invalid tokens from consideration.
A flexible (low offline overhead) and efficient (low on- line token-masking overhead) algorithm for grammar- constrained decoding (Sec. 3-4).
A tool implementing our algorithm, called GREAT- GRAMMA, that is up to 17.71x faster than other tools in offline preprocessing while retaining low online token- masking overhead (Sec. 5).
2. Approach Overview
In this section, we give some brief background about parsing (Sec. 2.1) and grammar-constrained decoding (Sec. 2.2), overview the high-level structure of our decoding approach (Sec. 2.3), and discuss our improvements over prior work.
Going back grammars, parser either accepts or rejects string. A simple extension is to make this process online- the parser rejects as soon as it consumes a token that will ensure the imput string fails to parse. Intuitively, the key idea behind grammar-constnn constrained decoding is that the parser primitive for checking if a token will be allowed or not by the parser can be used build the checker C.
2.1. Lexing and Parsing
While it is possible to build parsers that operate directly on input text, practical parsing tools first perform prepro- cessing pass using a lexer for efficiency. A lexer is built from set of regular expressions which define terminals (e.g. identifiers, keywords, integer literals). Fig. la il- lustrates two regular expressions defining two terminals b (strings consisting of an a followed by a sequence of b's) and C (strings consisting of an a followed by a sequence of c's).
However, there is key problem with using parser checker for constrained decoding: parser reads language level tokens (which this paper calls terminals to avoid confu- sion), while an LLM outputs tokens according to its subword vocabulary. The LLM tokens may span multiple or only fragments of language terminals, complicating the decod- ing process. This problem known as token misalignment (Poesia al., 2022), and is the chief source of complexity for GCD implementations. For example some of the LLM tokens in Fig. Ic correspond to terminals whereas others can span multiple terminals.
The lexer then takes as input a string and tokenizes it so that substrings matching regular expressions for terminals are grouped together. Here, our terminals consist of an followed by either sequence of b or c. For instance, the string "abaccab" lexes as ab acc ab.
2.3. Our Approach
The pass by the lexer ensures that the parser can be de- fined directly over terminals instead of individual characters. This separation of concerns avoids mixing character-level processing with higher-level grammar rules, making both components easier to implement and maintain. In particular, the grammar for the language can be defined at the terminal level. In our example, the grammar shown in Fig. le accepts sequences of terminals of the form BCBCBC... (where B and C can be any strings matching those terminals).
Fig. 1 illustrates the overall structure of our approach, which is based on a data structure we introduce called token spanner table. Intuitively, the token spanner table stores what sequences of terminals could be emitted by the lexer if it reads an LLM token from a given state.
Our GCD approach is split into two parts: offline pre- processing phase in which the table is constructed and an online phase where the table is then used to generate token masks during decoding.
One way of defining a parser is as an automaton: takes as input sequence of terminals and either accepts rejects the sequence. To handle all context-free grammars the au- tomaton needs to be a pushdown automaton (PDA) that is equipped with a stack. In our example, the simple stack-free automaton shown in Fig. If is enough to describe all valid sequences of terminals.
The offline portion of our algorithm takes two inputs: the LLM vocabulary V (Fig. Ic) and the definitions (as regexes) for terminals (Fig. la). It then constructs finite state au- tomaton (FSA) with set of states Q representing the lexer (Fig. lb). For example, state d2 represents a state where the lexer has already read the substring ab and can (optionally)
2

---

Flexible and Efficient Grammar-Constrained Decoding
ab+
ac+
"a", "b", "c", "ab", "ac", "aba"
S BC BC.S
(a) Terminals and regular expressions.
(c) Subword vocabulary for the LLM.
(e) Grammar Gat-
9
a
q1
a
b
ab
So
B
B,C
Ø
Ø
B
C
BB, BC
S8
91
Ø
B
C
Ø
Ø
2
BB, BC
B
Ø
BB
BC
BBB, BBC
S
C
S2
(b) Lexing automaton obtained from terminal definitions Fig. la.
CB, CC
Ø
C
CB
CC
CBB, CBC
(d) Token spanner table computed from lexing automaton (Fig. 1b) and subword vocabulary (Fig. Ic).
(f) Automaton for the grammar in Fig. Ic.
Figure Illustrative example the approach implemented in GREATGRAMMA.
read more b's to emit B terminal. We use this automaton together with the LLM's vocabulary to build the token span- ner table (Fig. Id). The keys of the token spanner table are pairs (q, 2) where E Q is a state of the lexer automaton and v E V is an L.LM token. The (q, v) entry of the token spanner table contains the set of sequences of terminals that can eventually be produced if the lexer is in state q and is fed in one additional LLM token v. For example, given state 42 and LLM token aba we can either produce sequence of terminals BBB or BBC-this is because we are in a lexer state corresponding to having started B token, lex a complete B token from ab, and then start an arbitrary new token.
(i.e., grammar-level tokens). A lexer is function Lex that given an input string w E Σ", returns pair (Zi... Tk. w,), where Ti V....,, Th E - is a sequence of terminals and w, E I" is the suffix of w that has not been lexed (i.c., mapped to language terminals) yet.
Typically lexers resolve ambiguity by making some sim- plifying assumptions that also help improve efficiency and avoid backtracking. We use the same assumptions and de- scribe them next.
Maximal Munch Principle and Lookahead Consider a language that contains two different tokens for the increment operator ++ and the addition operator +. Although the input string ++ could be tokenized as two separate addition tokens, in practice lexers prioritize the longer valid token to resolve ambiguity (and which usually captures the intended syntax of the programming language). This behavior is called the maximal munch principle: the lexer matches the longest possible substring starting at the current position that aligns with a defined token pattern.
In the online portion, our algorithm uses the token spanner table together with the parser to construct masks stating which LLM tokens are valid at each step. During decoding, the algorithm tracks the state of the lexer (Fig. 1b) and the state the parser PDA (Fig. 1f) on the prefix the LLM has generated so far. The algorithm then analyzes the state the parser in determine the possible sequences of termi- nal the parser could consume next. Then, the algorithms consult the token spanner table using these sequences and the current state of the lexer to determine what LLM tokens should be masked and kept.
Under strict interpretation of the maximal munch princi- ple, if the lexer reaches the end of the input stream while processing partial triple-quoted Python string """a", the lexer should tokenize the input as two strings and "a". However, supporting such cases would require either wait- ing until the end of the input string to produce any tokens or allowing backtracking. As such, in practice many lexers (including Python's) 's) will raise an error and stop lexing if the scanned prefix cannot be tokenized This greedy behavior disallows some strings, but guarantees that the lexer can resolve all tokenization ambiguities by inspecting only the next character at each step.
3. Offline Token Preprocessing
Our approach starts by preprocessing the lexer efficiently construct lookup table that relates LLM tokens terminal sequences (Sec. 3.1) and vice versa (Sec. 3.2). The prepro- cessed lexer is then used to analyze the parser to determine what terminal sequences are actually possible sequences in the grammar (Sec. 3.3).
single terminal.
3.1. Lexer Preprocessing
Definition 3.1 (I-lookahead). A lexer Lex is 1-looahhead if for every string w E Σ* and valid continuation E Σ of w, whenever Lex(w) = (Ti... Tk. r) then Lex(we) is either T...T.TR+.. for some T E T or (TI...Te. rc).
Let Y denote the set of string characters, Vn denote the set of strings over this alphabet, and denote the set of terminals
3

---

Flexible and Efficient Grammar-Constrained Decoding
EOS:B$
bie
aba:a
EOS:S
a:B
Q2
aca, b:b, C:C
c:a
a:c
bie
c:b
Qu
Q1
q
4n
qab
c:e
ab:b, acic
a:C
L
Figure 3: Detokenizing transducer for vocabulary V {a, b, c, ab, ac, aba).
EOS:C$
Figure 2: A lexing transducer Ta derived from FSA A in Fig. 1.
E0S:B$
bte,
Terminals are specified as set of regular expressions. It is oftentimes convenient to work with a lexing automaton, which is the finite state automaton (FSA) that accepts strings matching any terminal definition (McNaughton & Yamada, 1960). We refer the reader to Sec. B.I for formal definitions of the semantics of FSA, but recall that an FSA is a tuple A (I, Q, qu 8, F) where E is the alphabet, Q is the set of states with initial state yJo E Q, 8 contains transitions of the form q S g', and F C Q is the set of final states.
ab:B
abic
a:B,
E0S:5
aba:BB
atf; aba:8
bie
ac:B
ab:C
Qo
Q1
cic
c:e.
ac:C
a:c,
4
act6
aba:CB
1-lookahead maximal munch lexer can be defined from a lexing automaton as follows: The input is processed character-by--carrcter by transitioning through the FSA's states. When no valid transition exists for the next character c, the lexer checks whether the current state corresponds to valid language token. If it does and the tokenizer has at this point produced a pair (Tr ......T ... w,), ) the not-yet tokenized string w,, is tokenized with token Tx+1 corresponding to the reached state, the FSA is reset to its initial state go (and the tokenizer state (Ti ...... TeTx++,8) with the empty string E), and the character e is consumed the starting character of valid token if cannot be
Lexing Transducer
E0S:C$
Figure 4: A determinized token-level lexing transducer TASY, which is formed by composing Ty from Fig. and Ta from Fig. 2.
detokenizing transducer simply maps LLM tokens their corresponding sequence of text characters (i.e., the input alphabet is V and the output alphabet is E). A detokenizing transducer is nondeterministic and can contain e-transitions that produce outputs without consuming inputs.
token To- If the current
Fig. 3 illustrates the detokenizing transducer Ty derived from the vocabulary V = {a. b, c, ab, ac, aba} Fig. 1. Note that as an optimization common prefixes of tokens form a trie-like structure (c.g.. state q. denotes the state reached when producing the first for all tokens that start with that character), reducing computational overhead by reusing shared prefix computation. Fig. 4 depicts the com- bined token-level lexing transducer TAoY = TA o Ty, which is the determinized FST capturing the sequential functional composition of the two transducers- the output of Tv is fed as input Ta- This token-to-terminal transducer enables efficient lookup of valid next tokens and produced terminal symbols in each state.
state does not correspond consumed at /o. then e is invalid. Invalid characters inform what tokens should be masked during constrained decoding.
This process can be formalized as a stntee-stae transducer (FST), an extension of finite-state automaton that can pro- duce output terminals when reading characters. Given the original lexing automaton A representing valid tokens, we write TA denote the lexing transducer, the FST corre- sponding to A. The construction of TA from A is formal- ized in Alg. 2 in Appendix A, but at a high level the process simply adds transitions to handle cases where no valid tran- sition exists for the current character c, outputting terminals and exiting final states. Fig. 2 shows the lexing transducer derived from the FSA in Fig. 1.
3.2. Realizable Terminal Sequences
Now that have defined the formal machinery behind lexing, we are ready explain how LLM tokens can be mapped to possible sequences of terminals.
LLM Token to Terminals Processing LLM tokens character-by-characce with the lexing transducer at runtime would incur significant overhead. To address this problem, we instead construct a ooken-to-termine transducer by com- posing the character-te ceteucee-to-terneee to-temninal lexing transducer with the detokenizing transducer introduced by Koo al. (2024). A
When the transducer TAOY in Fig. consumes the LLM token aba from the initial state qu, produces the terminal and moves state 91- inspect the grammar Gec in

---

Flexible and Efficient Grammar-Constranned Decoding
Algorithm 4 BUILDIIVERSSTOKESPPAANEELLL
Definition 3.4 (Inverse Token Spanner Table). Given E Re the try Timv [g, (q,TT ... T.T)" in the inverse token spanner table Tim is the set of tokens that generates Ti. . T from state q. Formally,
Input: Combined FST TAOY (V.r.Q.0o. Output: Realizable token sequences AoVo Inverse lookup table Timy Aov Q + 2 Aov := 0. Tim (..)
lexer state ? E QAoyV and
for q 1. o' E 6 do
T Tine (g, T.......1 TxT) =
for T recognized at q", that is reachable from q' do
{t (t1g ii of E and T E Prod(g))
Re ;= Ae U {Ti TrT (q. TTTT= == Tam (q. Ti TTT) {t}
return Re Aov. Tim
Note that, for a given state q'. the set of producible terminals T in the lexing transducer can be precomputed using reach- ability algorithm (Floyd, 1962). This table allows a decoder to determine which LLM tokens can result in a given realiz- able terminal sequence T ... T&T being produced from a specific lexer state.
Fig. 1c, we can deduce that the parser, which receives as in- put sequences of tokens, expects/reqirres the next language token to be Since TAsy in state qi does not immediately produce any output when consuming b, the generated termi- nal sequence so far (i.e.. B) is still valid prefix according to the grammar Gec. However, after transitioning to q2, no possible path can generate C next.
Going back the example in Fig. 1, the table in Fig. Id illustrates the terminal sequences produced by the lexing transducer for each pair of state and token. The set of all realizable terminal sequences, Re is obtained by taking the union of all entries in this table.
As illustrated by the above example, for each transition q I:Ti...Ty, of in the lexing transducer TAaY, we should check whether there is terminal T such that (i) T can be generated along some path from d', and (ii) Ti .....7 Ti...Ty7 T&T is accepted by the grammar. This observation leads to the following definition, which describes which terminal se- quences need to be considered by the parser.
Building on Fig. 1d, we can also derive an inverse token spanner table, Tim- For a given state y and terminal se- quences ax the table Tin provides the set of tokens that can generate the sequence a from the state q. For example, the terminal sequence BC is generated by the token aba in state go (i.e., aba E Time (4o, BC)). The same sequence is generated by the token ac in state Q2 (i.c., ac (in BC)).
Definition 3.2 (Producible Terminals). Given a state q, the set of producible terminals (r)d(q) is defined as the set
3.3. Parser Preprocessing
{Ti E l
w: Tr.....TK
o' E 8* for some of Q, E
We do not formally define context- free grammars (CFG) for brevity and refer the reader to Sec. B.2 for details. For the sake of this paper, the reader only needs to know that a CFG parser is typically formalized as a pushdown automa- ton (PDA), an extension of FSA with execution stack (Schützenberger, 1963). The definition of PDA is sim- ilar to that of an FSA, but transitions are also allowed to manipulate a stack over symbols IT via push and pop oper- ations. Therefore, a PDA, a configuration after reading sequence of input characters is a pair of automaton state q Q and execution stack 7 e II*
Definition 3.3 (Realizable Terminal Sequences). Given a token vocabulary V and FSA A. let 5 be the set of transi- tions in the token-level lexing transducer TAoY The set of realizable terminal sequences Ae is defined as
AoV = =tTi. ..T...ITTT
3q, d' l.q teT o' E and T E Prod(g'))
Note that the LLM vocabulary V contains all characters in E. ensuring that E' V* Therefore, any next terminal producible in TA is also producible in the combined trans- ducer TAoY and vice versa. This equivalence allows us to simplify producibility checks: instead of analyzing the large combined transducer TAo,, we need only compute reacha- bility to accepting states within TA to determine producible next terminals.
We refer the reader to Sec. B.4 for the formal definition of a PDA, but informally, each PDA transition g c|s-+'1, , g' can only be activated if the character being read is a c and the top of the current stack configuration 7 matches to sequence of stack symbols 3 E II. If the transitions is activated, the current state becomes g' and the top elements of the stack are replaced with new stack elements 3' E II..
As with lexer preprocessing, our goal is to also preprocess the parser to avoid iterating over every terminal sequence generated by the lexer at runtime. The challenge with push- down automata (PDAs), compared to lexers (NFAs), is their
Inverse Token Spanner Table Alg. 4 computes the set of realizable terminal sequences and constructs the key data structure we use to perform constrained decoding.
5

---

Flexible and Efficient Grammar-Constrangg Decoding
requirement for stack to parse context-free grammars. This reliance on the stack prevents us from fully determining at preprocessing time whether a given terminal sequence is ac- ceptable from particular state, as the stack's 's contents must be examined during execution. However, we can still iden- tify many terminal sequences that will always be accepted or always rejected, independent of the current stack.
Algorithm 6 COMPUTEVALIDTOKENNM.N
Input: PDA P. FSA A, Inverse token spanner table Tim A Always-accepted token table A, Context-dependent sequence table D, Lexer state q², Parser state q², Stack configuration 7 Output: Set of allowed tokens Valtowed
V Vallowed == AA( a²)
for a E DD )
To compute which terminal sequences will always be ac- cepted or always rejected, we directly compose the detok- enizing transducer Aoy (Definition 3.3), with the PDA P produced by a parser generator (and where transitions operate over single terminals) (Allauzen & Riley, 2012) to obtain a new pushdown automaton P TReAoV where transitions operate over terminal sequences.
if a is accepted by P in state qº with stack y then Vallowed == Vallowed U Tin (g)
return Vallowed
This last pushdown automaton can efficiently determine valid sequences of terminal symbols from each parser state. We note that preprocessing both the lexer and parser in tandem is a key feature that distinguishes our work from prior work Beeurer-Kellner et al., 2024; Ugare et al., 2024).
dependent sequences D.
Note that one key source of efficiency resulting from our ap- proach is that many transitions in the combined transducer TASY produce the same terminal sequence Ti... T.,,, mak- ing Revl smaller than [V] or 1ö). Thus, the set of real- izable terminal sequences Aoy enables efficient precom- putation of what sequences of terminals the parser should consider.
Stack invariance provides a sufficient condition for knowing when a sequence of terminals is accepted.
Proposition 3.5 (Stack Invariance). If a PDA P accepts an input sequence w in state q with stack configuration %, then w is also accepted in the same state q when the stack configuration is 7 "I for some Y (i.e., when y appears at the top of the stuck with additional symbols beneath it).
4. Online Token Masking
With preprocessed inverse token spanner table Tivv along with the table of always-accepted tokens A and context- dependent sequences D, we are now ready to describe the online part of our grammar-constnn constrained decoder (Alg. 6).
It follows that a terminal sequence accepted by the PDA starting with empty stack configuration is accepted under any stack configuration.
At each decoding step, Alg. 6 analyzes the lexer state q²1 parser state q², and the current stack configuration 7 to produce the set of exactly all LLM tokens Valtowed that can lead to a sequence accepted by the the grammar.
The following proposition shows how to construct a stack- free finite-state automaton that overapproximates the set of sequences accepted by a PDA.
Proposition 3.6 (Overapproximation via FSA). Consider an FSA Ap obtained by removing all stack operations from PDA P. If an input sequence w is not accepted by Ap in state 9, then w cannot be accepted by P in state q with any stack configuration.
Although we construct the combined PDA P o TRe for preprocessing what terminal sequences a token can result in, using the same automaton for checking at decoding time whether LLM tokens can lead to valid parsing sequences would be inefficient. PDAs cannot always be determinized and one would have to compute reachability for nodes in PoTRAAS under different stack configurations to determine valid language token sequences. This computation would ef- fectively involve testing all sequences in Re at decoding time, making the preprocessing of the parser meaningless. Therefore, Alg. uses the set of always-accepted tokens A whenever possible to avoid traversing the PDA and only analyzes what terminal the PDA can accept at decoding time for context-dependent sequences described by D. The set of next legal tokens is then obtained by looking up, for each sequence of terminals accepted by the grammar, the set of tokens that can lead to that sequence. This is done by consulting the inverse token spanner table Tax-
Following Proposition 3.6, terminal sequence is always rejected if it is rejected by the FSA obtained by removing all stack operations.
The above reasoning can be formalized by computing the set of always-uccepted tokens A and of context-dependent terminal sequences D. Given lexer state 4dd and parser state q", denote by A(g ,?P) the set of tokens that are accepted regardless of the stack configuration 7, and by D(g pP) the set of terminal sequences that may be accepted by some configuration
Alg. in Appendix A describes how to preprocess a parser to build table of always-accepted tokens A and context-
6

---

Flexible and Efficient Grammar-Constrained Decoding
5. Experiments
Measures. For each combination of tokenizer and gram- mar, we measured the time taken to preprocess the grammar for that tokenizer and the average time taken by each GCD implementation to produce a token at inference time. To fairly evaluate per-token computation time, we wanted to ensure that all three tools followed the same token selection process and recorded the time required to compute the mask at each step-i.e. the online overhead. We manually built programs in each grammar and used them decide what sequence of tokens the decoder was going to produce-i.e., for each example program, the decoder produced each token in the program in order and computed the token masks at each step. Following this setup, we could exactly measure the same online average per-token overhead across all GCD approaches.
We implemented our algorithms for computing token masks in a tool called GREATGRAMMA. A testament to the sim- plicity of our approach is that GREATGRAMMA is imple- mented in just 900 lines of Python code built on top of the LALR parser provided by the LARK library (Shinan et al.). Specifically, we used LARK to parse regular expressions and context-free grammars, and used LARK's LALR parser to generate a parse table representing& a deterministic PDA for parsing sequences of tokens given context-free gram- mar.
In this section, we evaluate GREATGRAMMA by answering the following two questions:
RQI: How does the offline preprocessing overhead of GREATGRAMMA compares to existing GCD ap- proaches?
Results. Tab. 1 reports the results. We do not include XGRAMMAR in Tab. 1 because it encountered errors during either preprocessing or decoding for all the grammars we considered-it failed to compile the Java grammar, and entered infinite loop encountered segmentation fault during decoding for Python and Go grammars.
RQ2: How does the online per-token decoding over- head of GREATGRAAMA compares to existing GCD approaches?
On average (geomean), GREATGRAMMA'S offline prepro- cessing is 17.71x faster than SYNCODE, but 30.01x slower than OUTLINES.
Because all GCD approaches in theory produce the same to- ken masks and only differ in execution time, we do not need to evaluate GREATGRAMMA'S 's performance on specific downstream tasks; the effectiveness of GCD has already been evaluated in prior work (Geng et al., 2023; Beurer- Kellner et al., 2024; Park et al., 2024).
For certain terminal sequences, SYNCODE incorrectly masked a valid token (we suspect the source of this im- precision is that SYNCODE only unrolls future terminal sequences up to fixed bound k). When considering the remaining data points, GREATGRAMMA'S 's online masking is on average (geomean) 2.73x faster than SYNCODE. and 550.57x faster than OUTLINES.
Models and Grammars. We conduct our experiments us- ing three different tokenizers: Llama (32K tokens), Llama-3 (128K), and Qwen-2 (151K). We consider simplified Go, Java, and Python grammars from prior work on GCD (Ugare et al., 2024). We choose these grammars for three reasons: they are large grammars (87-99 terminals, 109-145 nonter- minals, 353-520 production rules, 7,441-9.311 bytes), they capture real programming languages that are used in exist- ing applications of constrained decoding, and they illustrate well the trade-off between offline preprocessing and online masking times. While other smaller grammars appear in existing work on GCD, the tools we compare against all take slightly different grammar formats with various restrictions (e.g.. no left recursion was allowed in XGRAMMAR). and we had to manually translate all grammars we considered between these formats to perform our evaluation (a very time-consuming task).
Discussion. In summary, GREATGRAMMA emerges as the new state-of-the-art GCD approach. GREATGRAMMA is 17.71x faster at offline preprocessing than SYNCODE, the only other GCD tool with acceptable online overhead (RQ1), and exhibits the lowest online masking overhead than any other GCD tool (RQ2).
While OUTLINES has the lowest preprocessing offline over- head, its seconds-per-tokee online overhead does not meet the needs of most practical applications of L.MMs. OUT- LINES' online overhead is due to the fact that its CFG mod- ule verifies the acceptability of each token at runtime.
The improvement offline pre-processing over SYNCODE is expected as our new approach targets the inefficiency of SYNCODE's algorithm for token alignment. The slight improvement in online loken-mask computation over SYN- CODE is likely due to how GREATGRAMMA only consults the PDA for context-dependent sequences. while SYNCODE does so for all terminal sequences up to a bound.
Baselines. We compare GREATGRAMMA against OUT- LINES (Willard & Louf, SY (Ugare et al., 2024), and XGRAMMAR (Dong et al., 2024), the three state- of-the-art GCD tools that can nominally handle grammars of practical sizes.
7

---

Flexible and Efficient Grammar-Constrang Decoding
Table I: Offline and online processing times. denotes when SYNCODE masked incorrect tokens.
Offline preprocessing (seconds)
Online per-token overhead (milliseconds)
Model
Grammar
OUTLINES SYNCODE GREATGRAMMA
OUTLINES SYNCODE GREATGRAMMA
Go
2.51
556.10
24.76
3,213.05
X
5.08
Llama
32,000
Java
2.49
579.48
33.79
3,450.67
46.71
6.29
Python
4.89
768.33
35.40
3,245.10
62.40
7.11
Go
2.43
2,212.95
106.07
12,974.43
X
21.11
Llama-3 128,256
Java
2.46
2,294.26
166.87
13,725.58
49.03
24.69
Python
4.86
2,789.31
170.71
13,167.83
71.49
30.17
Go
2.38
2,635.00
132.27
14,756.47
X
21.32
Qwen-2 151.665
Java
2.39
2,734.27
260.80
15,235.25
50.32
25.12
Python
4.81
3,268.09
155.32
15,146.38
70.87
32.30
While of course we cannot guarantee that GREATGRAMMA free of bugs, the simplicity of our approach makes its implementation easier (just 900 lines of code).
LR(k) parser (Knuth. 1965). However, this approach can significantly increase the size of the resulting transducer.
While our implementation uses a deterministic PDA as its basis, our algorithm can be modified to handle nondetermin- ism by tracking multiple active states concurrently. This extension is applicable to nondeterministic PDAs without e-transition loops that push stack symbols. Handling multi- ple states involves calculating the possible next tokens for each state individually and then taking the union these allowed tokens.
Furthermore, GREATGRAMMA'S offline preprocessing times have allowed to heavily test implementation without incurring in multi-hour testing times.
Limitations. The current implementation of GREAT- GRAMMA works under the lexing assumptions described in Sec. 3.1: maximal munch principle and 1-lookahead lexing. It therefore does not support languages for which lexing requires more than I-lookahead or instances where the same input sequence must be lexed differently depending on the parsing context.
6. Related Work
There are many different implementations of grammar con- strained decoding (Geng et al., 2023; Willard & Louf, 2023; Lundberg et al.; Beurer-Kellner et al., 2024; Ugare et al., 2024; Dong et al., 2024; Gerganov, 2024), but we focus our comparison on the ones that can handle realistic grammars (e.g., those of modern programming languages).
For example, in Java, the end of the nested generic List<List<T>> is erroneously tokenized by lexer operating under maximal munch >>-ie.. the bitwise right-shift operator. However, in this context the parser instead ex- pects two consecutive > terminals denoting the closure a generic type. (The Java grammar we used in our evaluation, sourced from the SYNCODE benchmark, does not support generic types.)
SYNCODE (Ugare et al., 2024) is the only that can pro- vide low online overhead for the large grammars in our evaluation. SYNCODE speculatively unrolls future terminal sequences up to a fixed bound (i.e., every terminal sequence in 1n) and precomputes a table similar to our inverse token spanner table but for all sequences. Our evaluation shows that our table can be computed significantly faster since only contains the of realizable terminal sequences.
To resolve this type of lexing ambiguity, the lexer must sider the current state of the parser, task that for arbitrary regular expressions requires the lexer to perform unbounded lookahead. is possible to modify our approach to han- dle practically occuring ambiguities by allowing the lexing transducer to nondeterministically generate both possible tokenizations (e.g., single >> terminal or two separate terminals), specifically for such cases that do not require arbitrary lookahead, and enabling the parser to select the valid interpretation based grammatical constraints.
DOMINO Kellner et al., 2024) precomputes a tree of terminal sequences similar to our lexing transducer. How- ever, at decoding time, DOMINO must traverse the entire tree because the set of realizable terminal sequences varies for each lexer state. In contrast, our approach computes a single global set of realizable terminal sequences Re which then to preprocess the parser. DOMINO'S im- plementation is not publicly available, but their paper reports 20s for offline preprocessing and 22% online overhead for
For a lexer requires & > 1 lookahead, a k-lookahead lexing transducer can be implemented by encoding the state and its a-lookahead as single combined state, similar an
8

---

Flexible and Efficient Grammar-Constraine Decoding
an extremely simplified C grammar with approximately 70 rules when using the smaller Llama tokenizer. For the same tokenizer, GREATGRAMMA can preprocess much larger granmars (353-520 rules) with similar times (25-35s).
LLM tokens in a given lexer state. This data structure also speeds up online masking compared to similar approaches by further reducing the number of inputs the parser has to check during decoding.
GREATGRAMMA is built with simple primitives that are XGRAMMAR (Dong et al., 2024) reduces runtime checks by preprocessing contextinneependent tokens for character- based nondeterministic PDAs, but mentions the misalign- ment problem in their related work. By preprocessing the set of realizable terminal sequences and the inverse token span- ner table, we efficiently integrate their context-independen token caching approach with a parser that uses a separate lexer. Furthermore, our overapproximation via FSA can identify more always-rejected sequences compared to their expanded suffix analysis, as our method can also follow rule-reduction edges by treating them as e-transitions.
already supported by existing parsing libraries and lends itself to an easy implementation consisting of just 800 lines of Python. This simple implementation is easier test (we have identified that other tools often crash or produce incorrect outputs) and opens the door to many future possi- ble research directions- e.g. finding ways to leverage the PDA stack to perform more aggressive precomputation or implementing decoding directly on GPUs.
A Acknowledgments
Existing research on the effecttivnness of constrained decod- ing in structured generation shows mixed results. Some stud- ies (Geng et al., 2023; Beurer- et al., 2024) demon- strate that GCD can improve downstream task performance. However, other recent work (Tam et al., 2024; Park et al., 2024) highlights that GCD can also negatively impact the quality of generated outputs. Our approach is orthogonal to these methods and can be integrated with techniques proposed by Park et al. (2024) or Banerjee et al. (2025) to mitigate such negative effects.
Supported, in part, by a Microsoft Faculty Fellowship; UCSD JSOE Scholarship; and NSF under grants CCF. 2422214, CCF-2402833, and CCF-221 1968. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors, and do not nec- essarily reflect the views of the sponsoring entities. Loris Professor
D' Antoni holds concurrent appointments the University of California San Diego and as an Amazon Scholar. This paper describes work performed at the Uni- versity of California San Diego and is not associated with Amazon.
Comparison with LLGUIDANCE (Moskal et al., 2025) After we completed this paper, Moskal et al. (2025) released LLGUIDANCE, a fast GCD tool written in Rust that incorpo- rates a memory-optimizee tokenizer trie, a derivative-based lazy lexer, and highly optimized Earley parser. LLGUID- ANCE shares some similarities with our compositional ap- proach, but it relies on derivative-base based parsing instead of automata and transducers constructions.
Impact Statement
This paper presents work whose goal is to advance the field of Machine Learning. There are many potential societal consequences of our work, none which we feel must be specifically highlighted here.
References
The evaluation provided on LUIDANNNS'' website reports impressive performance (in the order of micro to millisec- onds for both offline pre-processing and online per-token overhead) on benchmarks like BeeNSchemaBench (Geng al., 2025). However, we could not compare this tool to our approach because LLGUIDANCE (v.0.7.27) reports the "ParserTToC "oorserrooCople"" error when applied to the grammars used in our experiments. However, we believe that some of the optimizations employed by LLGUIDANCE can be also beneficial for GREATGRAMMA.
Allauzen, C. and Riley, M. A pushdown transducer ex- tension for the openfst library. In Implementation and Application of Automata: 17th International Conference, CIAA 2012, Porto, Portugal, July 17-20, 2012. Proceed- ings 17, pp. 66-77. Springer, 2012.
Alur, R., Fisman, D., Padhi, S., Singh, R., and Udupa, A. Sygus-comp 2018: Results and analysis. 2019.
Banerjee, D., Suresh, T., Ugare, S., Misailovie, S., and
Singh, G. Crane: Reasoning with constrained IIm genera- tion, 2025. URL
7. Conclusion
We present GREATGRAMMA, a tool for grammar- constrained decoding that is both flexible (low offline over- head) and efficient (low online overhead). GREATGRAMME precomputes a succinct and easy-to- casy-to-generate generate data structure that only captures terminal sequences that are realizable by
Beurer-Kellner, L., Fischer, M., and Vechev, M. Guiding Ilms the right way: fast, non-invasive constrained genera- tion. 2024.
Deutsch, D.,, Upadhyay, S., and Roth, D. A general-purpose

---

Flexible and Efficient Grammar-Constraigg Decoding
algorithm for constrained sequential inference. In Pro- ceedings of the 23rd Conference on Computational Natu- ral Language Learning (CoNLL), pp. 482-492, 2019.
Thirty-eighth Annual Conference on Neural Information Processing Systems, 2024. URL https://ooeerreviev.
net/foruunid=-S77e8ELLLU
Dong, Y., Ruan, C. F., Cai, Y., Lai, R., Xu, Z., Zhao, Y., and Chen, T. Xgrammar: Flexible and efficient struc- tured generation engine for large language models. arXiv preprint arXiv:2411.15100, 2024.
Poesia, G., Polozov, A., Le, V., Tiwari, A., Soares, G., Meek, C., and Gulwani, S. Synchromesh: Reliable code genera- tion from pre-trained language models. In International Conference Learning Representations, 2022. URL https:///openreviee net/forummid
Floyd, R. W. Algorithm 97: Shortest path. Commun, ACM, 5(6):345, June 1962. ISSN 0001-0782. doi: 367766.368168 URL / 1145/337766 368168.
Schützenbergeer, M. On context-free languages and push- down automata. Information and control, 6(3):246-264, 1963.
Geng. S., Josifoski, M., Peyrard, M., and West, R. Grammar- constrained decoding for structured NLP tasks without finetuning. In Bouamor, H., Pino, J., and Bali, K. (eds.), Proceedings of the 2023 Conference on Empirical Meth- ods in Natural Language Processing, Singapore, De- cember 2023. Association for Computational Linguistics. URL https::/actanntoooog.ooom orm../...p................. main.674,
Shinan, E., Megalng, chanicpanic, Malard-Adam, J., Chil- amkurthy, S., Lamnigan, P., Emanuel, K., konstantin, evan- drocoan, Chang, Y., Schreiner, H., ThatXliner, Chammas, N., ornariece, Rogdham, Makukha, M., Lauer, K., K., M., Rose, R., decorator factory, orcharddweller, Grit- senko, D., Rydzewski, J., starwarswii, Y-M, J., Rackye, Wienemann, P., PJCampi, Idbo, and Latimer, K. lark- parser/lark. URL https://gittub.ce http://tttuub.om/rrrrreeee parpattuurrccco/tttapprrrrrr// parser/ lark.
Geng, S., Cooper, H., Moskal, M., Jenkins, S., Berman, J., Ranchin, N., West, R., Horvitz, E., and Nori, H. Json- schemabench: A rigorous benchmark of structured out- puts for language models, 2025. URL https://arxiv. /.0..
Tam, Z. R., Wu, C.-K., Tsai, Y.-L., Lin, C.-Y., Lee, H.-y.. and Chen, Y.-N. Let me speak freely? a study on the impact of format restrictions on large language model performance. In Demonncorr, F., Preofiuc-Pietro, D., and Shimorina, A. (eds.), Proceedings of the 2024 Confer- ence Empirical Methods in Natural Language Pro- cessing: Industry Track, pp. 1218-1236, Miami, Florida, US, November 2024. Association for Computational Lin- guistics. doi: 10. https://aclantthol.gg wwwp://ooogooooo2....e.. http:///w......./............ana itt.innduuttyy.////
Gerganov, G. llama.cpp, 2024. URL https://githubbcom
ggerganov/llana cpp.
Knuth, D. E. On the translation of languages from left to right. Information and control, 8(6):607-639, 1965.
URL
Koo, T., Liu, F., and He, I.. Automata-based constraints for language model decoding. 2024. URL https:// openreview.ro net www.:eett/oruunt.-dBddbbbblbb
Ugare, S., Suresh, T., Kang, H., Misailovic, S., and Singh, G. Syncode: Llm generatio with grammar augmentation, 2024. URL http::////aaavv.rraa//////0
Lundberg, S., Ribeiro, M. T. C., Edgar, R., Harsha-Nori, Cooper, H., Koch, P., King, N., Markus, Marawan, Moskal, M., Jenkins, S., cpcdoy, h-k nyosu, Chirculescu, M., Viggiano, D., X, H., Rafael, J., Bell, A. G., Zivontsis, S., sam rodriguez, Amemiya, R., SimFG, Peach, R., Heiner, N., JC1DA, Popan, F,, Nguyen, A. M., Anil- Turaga, Delaney, R., and Saibo-creator. guidance- ai/guidance. 1. URL httts:://gtthtii com/ http//uudaceeeeee aL/ guidance.
Wang. B., Wang. Z., Wang, X., Cao, Y., Saurous, R., and Kim, Y. Grammar prompting for domain-specific lan- guage generation with large language models. Advances in Neural Information Processing Systems, 36, 2024.
Willard, B. T. and Louf, R. Efficient guided generation for large language models. arXiv e-prints, pp. arXiv-2307, 2023.
McNaughton, R. and Yamada, H. Regular expressions and state graphs for automata. IRE transactions Electronic Computers, (1):39 47, 1960.
Moskal, M., Cooper, H., Pham, A., Lucato, D., Wolski, S., and Xiong, Y. guidance-ailllaiddann https://github http:://gggtuuuu.ooguuauaaaeee wwwpg/iiagcceeeee//oo//oooo..eea htt.hu/..c.ogguuddddeaaag/llleee ai/Llguidance.
2025. URL
Park, K., Wang. J., Kirk-aaik,,,,,c,, T., Polikarpova, N., and D' Antoni, L.. aligned decoding. In The
10

---

Flexible and Efficient Crasmar-Constranned Decoding
A. Algorithms
In this section we formalize several algorithms presented the paper. Alg. constrained decoding. describes how build the lexing transducer from a lexing automaton given as a FSA. Alg. describes the construction the detokenizing transducer, which converts sequences of tokens to sequences of the characters they contain. Alg. 5 describes the parser preprocessing and how the always-accepted token table and context-dependent sequence table are built.
describes the abstract algorithm for general
Algorithm 1 CONSTRAINEDDECODING
Input: Model M, Checker C, Tokenized prompt V := Mvvocabulary
repeat
m := C(a; V)
logits == (I)
beezt sample mask(m, logits))
a.appeed(tnext)
until next jf EOS
return æ
Algorithm 2 BUILDLEXINGFST
Input: FSA A = (E, Q, 90: 6, F), Output alphabet I' Output: FST T^ (2,1,, Q, 90. 8PST. FFST)
q' E 88. FIST := {go} for state q that recognizes language token T E I do for (c) s.t. 3q".q q S q" $ 5 and 90 g' E 5 do
JEST := :/- <6 o' 1 111050 S
8FST == öEST U {g =T o}}
SYST == ÖYST U {q
ES + go} U fgo
EOS
qu)
return TA = (E, r, Q, go, BUST, FIST)
Algorithm BUIIIDDDETKKENIIIGGSTT
Input: Vocabulary V Σ
Output: FST Ty = (V, E, Q qo: 6, F) Q: (1c) ). F == [4c). 90 == gc,
0
for c1 ... C E V do
Oprev 9e
for = 1 to k do
Q = Q U {sem.a 8 8 U {aprev eics
aon...
9prev Jcr..s
8 = U {yprev G...6 ge)
return Ty = E, Q 90 F)
B. Formal Definitions
B.1. Finite-State Automata
finite-state automaton (FSA) defined as tuple A (E,Q.ggo F) where is the input alphabet, Q is the set of states, Go Q is the initial state, 8 Q (E U {e)) is the set of transitions. and F C the set of accepting states. Each transition (q. c, q¹), also denoted by S d', indicates that, from state q, upon reading the input symbol c, the automaton transitions to state /'

---

Flexible and Efficient Grammer-Constraiin Decoding
Algorithm 5 PREPROCESSPARSER
Input: PDA P, Realizable sequences Ae
FSA A, Inverse token spannar table Tiw Output: Always-accepted token table A Context-dependent sequence table D
Ap == REMOVESSTAAKKOPERRTTINNPSS
for op E Qp do
A(gp) :- {a ReALv q with stack accepts a}
R(gr) = {a Re A(q) Ap rejects in q}
D(gp) = REAGV \ (A(q) R(g)
for E QA do
A(UA,97) == A(g Tim
D(gA, (P) {a E D(q) Tim (4A, * #0}
return A,
Given a transition relation å of automaton A, the extended transition 8* C C x X Q is the smallest relation defined by (i) (g. (, 8* and (ii) (q, we, w',d)) 8* whenever (q, w. 4²) E 8 and (q", c, E 8 for some q" Q. We also denote (g, (') E 8 by " q' A string E E" is accepted by automaton A when there exists o' E such that _ q E 8*.
However, in this paper, we use the term accepted a broader sense than its standard definition. Specifically, we say that string w is accepted in state if there exists y' such that " d' E 8", meaningthat a valid transition for w exists from q.
B.2. Context-Free Grammar
context-free grammar (CFG) G is a tuple (T, ,,,S R) where I is a finite set of terminal symbols (e.g. constants, variable names, and keywords), N a finite set of non- non-terminal symbols, S E is a start nonterminal, R. is a set of production rules A a....., Ch,, where A N and a, E Nur.
Formally, a grammar defines a single-step derivation relation sequences of symbols a, B, E (NUT)" aAy aBy if A + 3 E R. The reflexive transitive closure of this relation is called derivation and written = A sequence of terminals is a sentence if it is derivable from S; the set of all sentences is called the language of the grammar G, that is,
((g) = {w E I* S I==* ** w).
In addition, we define the prefix language of 9 as the set of all prefixes of sentences in L(g), that is, Cprefx = {w m* 3e E T* we E L(
B.3. Finite State Transducer
An FST is a tuple T= = (E, 1, Q, 9o, 8, F) where components are analogous to those of a FSA but each FST transition q TT...TTr of in 5 denotes that when reading character from state q, the FST moves to new state q' and also outputs the sequence Ti... T3 of elements over the output alphabet r.
B.4. Pushdown Automata
pushdown automaton tuple P (I, Zo, 5, F) where E, Q, go and F are as in their FSA definitions, IT
the stack alphabet, Zo 11 is the initial stack symbol, and d C Q x (E U (e)) x II x Q II the set of transitions. Each transition (q, q ()) specifies that, in state q, upon reading the input symbol and matching the top stack symbols to a, the PDA transitions to state g' and replaces with the sequence 3 on the stack.
C. Formalizations and Proofs
C.1. Lexer
lexer specification is given as finite set of pairs, each consisting of an automaton 4'' = -Q', 8', and terminal symbol T Given lexer specification {(A', T',,, a corresponding (1-lookahead) partial lexer a partial function
12

---

Flexible and Efficient Grammar-Constrained Decoding
Lex: Σx 1 Σx in which defined following:
Lex(e) = (c,
Given Lex(w) = Tk. wy), the value of Lex( we) is
(1) (Ti .... T.T.s, if = EOS and wr E [(A2) ) for some j
(2) (Ti .T,,,,,, c + EOS and W. E ppretix (At) for some
(3) VT...TTTT,. if # EOS and W, ((A") but w/C & Cprefix for all
(4) 1 otherwise
The lexing automaton A is defined as the product automaton of automata A' specified in the lexer definition (LA'TT))
Lemma C.I. Let TA (Q, E,T, qo, 6, F) be a lexing transducer for the lexer specification {(A', T*)}; Assume ((A))
for all i and each A' does not have any dead state. Then, for any string w E E", Lex(w) = (Ti Tr. wy) if and only if 40 w..ri d' E 8t and " g' E 8* for some q' E Q.
Proof. The proof proceeds by induction. For the base case, let w = c. Then Lex(c) = (c, and To S qo E E This the only possible transition for empty input, as [(A*) for each i.
Otherwise, consider the remaining cases in the definition of Lex. Cases (1)-(3 are by construction. Assume Lex(wr)
(Ti... ... Tk, wr), then by the induction hypothesis, go w:Ti... o' E 8 and yo _ o' E 5 for some o' Q. The final case applies when Lex(we) = I, indicating that valid tokenization of we can be produced. By assumption, our component automata constructed without dead states. This ensures that there doesn't 't exists o' Q such that 40 wr.Pi..TTk q' 8 when W, & Lprefix (A') for all i. Conversely, if there doesn't exist q' Q such that go w::Ti..Tk, of E 8", then by construction, cases (1)-(3 cannot hold so Lex(wc) must be T.
The correctness of the detokenizing transducer is proven in the Appendix of (Koo et al., 2024). The correctness of the token-level lexing transducer follows from the correctness transducer composition.
Theorem C.2. Let TAOV = =Q, (Q,V, qo, 5, F) be a token-level lexing transducer for the lexer specification (")", and
vocabulary V C -+ Then qo Tn. of E 8* if and only if Lex(w) = (Ti... .....TTe. W.) for some we E D* and q' E Q
such that qo d'
C.2. Inverse Token Spanner Table
By construction of inverse token spanner table, the following proposition holds.
Proposition C.3. Given a token sequence w E V such that qo mu:T g. any U V and T I, the token is in the inverse token spanner table entry [g (T441 TmT) if and only if wo. T, Tei..... I...TT,, q" and T E Prod(g"))
C.3. Parser
Given context-free grammar g ( S, R) with a separate lexer Lex Σ* - - x E', we say that token sequence V" is a sentence if there exists derivable sequence of terminals Ti... T3 such that Lex(w) = (Ti T2S. E). Formally,
CLax (g) = {w E V" 3T. TT. Lex(w) = (Ti T.S T.... T&S E L(g))
We also define the prefix language of G with separate lexer Lex as the set of all prefixes of sentences in (Lax(G), that is. preeti (g) = {w E" 3u E E" wv E (G)).
Lemma C.4. Consider a string w E V" with an extended transition 9 w: w:TT... d' through the lexing transducer, where TI T....2 Tg is incomplete prefix of L(G) (L.e. Ti T...Ty ...TT E Cprenx(()) \ L())). If E Cheen (9) then there must exist some terminal T Prod(g') such that T ... T&T Epretx(9))
13

---

Flexible and Efficient Crammar-Constrained Decoding
Proof. Suppose prefix (9). By definition of the prefix language, there exists non-empty suffix v V+ such that we E (g). Consequently, Lex( must yield a complete token sequence ending in a EOS token, say (Tr ... TrTK+1 ... 8. where Ti ..... TTTk+I.... S E (()).
Given assumption that ..... Te & L(G), it follows that Tk+1-.- ... Tm cannot be empty. Specifically, this means Tk+1 must exist and be producible from the state q', i.e..'' E Prod(d').
.. with the next token Tk+1, we form a valid prefix of complete token sequence Therefore, by combining Ti .i...Tk
T Tk+1 E Lepeffi
Theorem C.5 (Completeness). Ler
96 Zo.8 F be pushdown automaton such that L(P) Lg)).
Given a string w E Pepeeii (9) and a token v E V, the token u is not masked by Alg. 6 (i.e., v E Vallowea) if the concatenation we belongs to prefix (9).
Proof. By Theorem C.2, the lexing transducer emitted Ti ... .T and reached state o' such that Qo Write q. If ww wo:Ti...TT Tu 11 .T...Tm, q" for some state q", which implies d' Tki1...Tm, q"- By Lemma C.4, there exists T E Prod(a") such that . T.TT44 T'T E (g) Therefore, Timold' TK41 ... TmT), and hence
prefix (9), then @o
E Vallowed-
Lemma C.6. IfT E (q), then there exist q' E Q and v E y such that
w. o' E
Proof. Since T E (rod(g'), there exist q" Q and E V such that d' T:a d" E 8 Note that E S V. A key property of the lexing transducer is that it produces at most one terminal for each input character. Consequently, there must exist prefix Up of e and a state q" E Q such that q' Vp:iT q"d E 8*.
Lemma C.7. Assume that if there exists some U E V such that go M.N:T q. then for any terminal sequence a E I", there w..':T g' Consider a string w E VV with an extended transition q w:Tr..Tke o' Ta E Lerofix \ L())). If there
also exists some E V such that qo through the lexing transducer, where Ti Ti...Ty T is incomplete prefix of L(G) (i.e., Ti...Tk exists T Prod(q') such that Ti... TrT Spreftx (9) then w prefi (G).
Proof. Suppose there exists T E Prod(g') such that ..... T&T E Cprenx(g). By the definition of prefix language, there exists E T such that T L(g). Furthermore, by Lemma C.6, for such T, there exist some state q' E Q and a string V* such that of T.:T q" E 8*. Now, by the assumption, there also exists a string v' V* such that for some state qd E Q. g' ToT. 1" E 8* Here, since a must end with $, it implies that q" must be the initial state Yo by construction. Thus, we have Lex(we') (Ti T,Ta, e). Since Ti ... TTTTa E L(G), this final result implies that E Crefix (9).
Theorem C.8 (Soundness). Let p= I1, ; 20, Given a string w E Cprofix (9) and token v E V. the token v is not masked by Alg. 6 (i.e., v E Vallowed) only if the concatenation we belongs to ppretix (G).
be pushdown automaton such that L(P) = L(G).
Proof. By Theorem C.2, the lexing transducer emitted 7i... ... Ti and reached state o' such that 4o 2F,..0 q' If U E Vallowed- then there must exist some T I such that E Tam (g' Te+1 ... T). By the construction of inverse token spanner table, this implies that the concatenation Ti. TyTk+1 ... Tm is in the prefix language (grenx(9), Furthermore, this means that there exist some q" E Q such that q' Tetr...fim q" and T Prod(a"). Therefore, by Lemma C.7. the concatenation wv belongs Coea (9).
14


Reviews:
[{"review_id": "fRrYDy944q", "reviewer": "Reviewer_q1Dz", "summary": "This paper describes a flexible & efficient implementation of grammar-constrained decoding for LLMs. Grammar-constrained decoding uses a (usually deterministic) CFG to constrain the output space of LLM decoding. A main challenge in apply such a constraint is the mismatch between the alphabet of the constraint (usually characters for the lexer and terminals for the parser) and the LM (subword tokens). Existing implementations either require expensive offline grammar preprocessing ([Ugare et al, 2024]) or incur a large overhead during decoding ([Willard and Louf, 2023]).\n\nThe paper proposes to use a token spanner table (Figure 1(d)) to map each subword token to possible terminal sequences with 1 lookahead from each lexer state. After converting the CFG into a PDA, this table is then further partitioned into $A(q^{\\mathcal{A}}, q^{\\mathcal{D}})$ (the set of terminal sequences allowed by the PDA starting at lexer state $q^{\\mathcal{A}}$ and PDA state $q^{\\mathcal{D}}$ under any stack configuration) and $D(q^{\\mathcal{A}}, q^{\\mathcal{D}})$ (the set of terminal sequences allowed by the PDA starting at lexer state $q^{\\mathcal{A}}$ and PDA state $q^{\\mathcal{D}}$ only under certain stack configurations), which enables faster computation of token masks at decoding time (Algorithm 6).\n\nBenchmarks show that the proposed method is 17.71x the speed of SynCode ([Ugare et al, 2024]) during offline preprocessing and 2.73x the speed during decoding (Outline ([Willard and Louf, 2023]) while faster during offline preprocessing is inpractically slow during decoding).\n\n[Ugare et al, 2024]: https://arxiv.org/pdf/2403.01632\n[Willard and Louf, 2023]: https://arxiv.org/pdf/2307.09702", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their feedback, which will significantly improve the paper. We believe ICML is an appropriate venue as it has previously published similar work in constrained decoding (e.g., https://openreview.net/forum?id=pXaEYzrFae last year).\n\nBelow, we provide a detailed response to each comment and question.\n\n> Figure 2 does not appear to mark all the final states. With being the only final state, this FST only accepts $\\epsilon$. $q_2^B$ and $q_3^C$ should also be final each with a final output arc. \n\nThanks for bringing this to our attention. $q_0$ is the only final state, but the transducer appears incorrect because we omitted the transitions for EOS (from $q_2$​ and $q_3$​ back to $q_0$​). We had initially omitted them to simplify the lexing transducer, but we now realize this omission makes the figure imprecise. We will add the necessary EOS transitions.\n\n> The machine in Figure 4 is called $T_{\\mathcal{A} \\circ \\mathcal{V}}$ in most places, but other also sometimes $T_{\\mathcal{A}} \\circ T_{\\mathcal{V}}$ (Algorithm 4; 245-246, left column). \n\n> (267, left column) , $T_{inv}(q, \\alpha)$, it appears that $\\alpha$ should really be $T_1 \\ldots T_k T$ instead. \n\nThanks, we will resolve the conflicting notation in the revised version of the paper.\n\n> Overall, I had a really hard time understanding Section 3.3 before seeing Algorithm 5. Perhaps there is a better way to present the ideas? \n\nThanks for the feedback. The primary role of Section 3.3 is to explain how to compute the always-accepted token table $A$ and context-dependent sequence table $D$. The detokenizing transducer is mostly an implementation detail used to avoid having to iterate over terminal sequences at runtime.\n\nWe will update the structure of Section 3.3 to be clearer: we will first introduce the definitions of always-accepted/rejected tokens and context-dependent terminal sequences, and then briefly mention the detokenizing transducer as an implementation detail.\n\n> Does the PDA need to be deterministic? If so, could you mention this explicitly early in the paper? \n\nWe assumed a deterministic PDA for simplicity of implementation, but determinism is *not* strictly necessary. To handle non-deterministic PDAs, one can track multiple non-deterministic states simultaneously (similar to Thompson’s construction for NFA determinization), compute masks separately for each state, and then take the union of these individual masks. This extension allows the algorithm to accommodate non-deterministic PDAs without affecting performance in deterministic cases. We will clarify this point in the revised version of the paper.", "claims_and_evidence": "The main claims of this paper is the correctness and speed of the proposed method. The high level algorithms are correct although proofs were not given in the paper. The claim on speed is well supported by the experimental results.", "methods_and_evaluation_criteria": "Yes.", "theoretical_claims": "N/A.", "experimental_designs_or_analyses": "The main experiment involves speed benchmarking for offline preprocessing and decoding. Grammars for 3 programming languages are used (Go, Python, and Java). For decoding benchmarks, a set of 5 programs for each language (367, left column) is used for computing token masks. The programs are available in the supplementary material, and they are small programs (< 100 lines). Grammar complexity is the main factor that determines the decoding speed (the grammars are all deterministic PDAs if I am not mistaken), thus the small size of the programs should not be a main problem.", "relation_to_broader_scientific_literature": "Most recent work on constrained-decoding using CFGs are all cited in this paper, in particular, Outline ([Willard and Louf, 2023]), XGrammar ([Dong et al, 2024]), and SynCode ([Ugare et al, 2024]). Formally, these and this paper itself are all incremental parsing methods under the hood that also involves a composition with the subword-character detokenizing FST. However, the exact techniques employed in implementing the parsing & composition have significant impacts on speed. Benchmarks show that the proposed solution in this paper is faster than SynCode and Outline during decoding (XGrammar appears to have issues that prevented the benchmarks from being conducted). Additionally this paper in my opinion presents the more elegant solution compared to the existing ones.\n\n[Dong et al, 2024]: https://arxiv.org/pdf/2411.15100\n[Ugare et al, 2024]: https://arxiv.org/pdf/2403.01632\n[Willard and Louf, 2023]: https://arxiv.org/pdf/2307.09702", "essential_references_not_discussed": "None.", "other_strengths_and_weaknesses": "Strengths\n-   Most parts of this paper is well written (except Section 3.3 which I took me quite a while to fully understand)\n-   The prosposed solution are both simple and effective\n\nWeaknesses\n-   ICML may not be the best venue for this paper given there is nothing about machine learning in this paper. NLP conferences such as ACL are definitely more appropriate where a larger body of conference attendees can appreciate this paper. **However, I did not take this into consideration in my \"Overall Recommendation\" (i.e. I gave the rating that I would give if I were reviewing for ACL)**. The area chairs should be the judge of this.", "other_comments_or_suggestions": "-   Figure 2 does not appear to mark all the final states. With $q_0$ being the only final state, this FST only accepts $\\epsilon$. $q_2^B$ and $q_3^C$ should also be final each with a final output arc.\n-   The machine in Figure 4 is called $\\mathcal{T}_{\\mathcal{A} \\circ \\mathcal{V}}$ in most places, but other also sometimes \n\n    $\\mathcal{T}_{\\mathcal{A}} \\circ\\mathcal{T}_V$ (Algorithm 4; 245-246, left column).\n-   Algorithm 4 operates on $\\mathcal{T}_{\\mathcal{A} \\circ \\mathcal{V}}$ but in lines 257-259, left column, the text says\n\n    $\\mathcal{T}_{\\mathcal{A}}$. Indeed the table can be built on\n\n    $\\mathcal{T}_{\\mathcal{A}}$ alone, but the description should be more consistent.\n-   (267, left column) $T_{\\mathrm{inv}}(q, \\alpha)$, it appears that $\\alpha$ should really be $T_1 \\ldots T_kT$ instead.\n-   (251, right column) \"we directly compose the detokenizing transducer $Re_{\\mathcal{A}\\circ\\mathcal{V}}$\": I think starting from here this subsection is trying to motivate Algorithm 5, but $Re_{\\mathcal{A}\\circ\\mathcal{V}}$ is not the detokenizing transducer, and the composition is done implicitly in Algorithm 5.\n\n    Later, in (256, left column), $\\mathcal{T}{Re_{\\mathcal{A}\\circ\\mathcal{V}}}$ occured without being defined. Overall, I had a really hard time understanding Section 3.3 before seeing Algorithm 5. Perhaps there is a better way to present the ideas?", "questions_for_authors": "Does the PDA $\\mathcal{P}$ need to be deterministic? If so, could you mention this explicitly early in the paper?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "4IlKKqpIbR", "reviewer": "Reviewer_apti", "summary": "Given a language model and a certain grammar, grammar-constrained decoding (GCD) aims to ensure the output of the language model adheres to the grammar. However, this is challenging because, typically, the token vocabulary for a language model does not align with that of the grammar. In this paper, the authors aim to overcome this challenge by suggesting a novel algorithm for GCD which involves an offline stage and an online stage, the latter being more efficient than current GCD algorithms. Through pre-processing, the online token masking process becomes much more efficient. The authors also provide GreatGramma, a tool for implementing their method.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their insightful feedback. Below, we provide a detailed response to each comment and question.\n\n> is this method masking out other tokens that might also be allowed?\n\nThe masking algorithm of GreatGramma is sound and complete under the assumptions on the lexer stated in the paper. We will include a proof sketch in the body of the revised paper based on the following key lemmas, and include detailed proofs in the appendix.\n\nLemma 1. Let $T_{A \\circ V} = (Q, V, \\Gamma, q_0, \\delta, F)$ be a token-level lexing transducer for the vocabulary $V \\subseteq \\Sigma^+$. Then $q_0 \\xrightarrow{w:T_1 \\ldots T_k}^{\\ast} q' \\in \\delta^\\ast$\nif and only if $Lex(w) = (T_1 \\ldots T_k, w_r)$ for some $w_r \\in \\Sigma^\\ast$ and $q' \\in Q$ such that $q_0 \\xrightarrow{w_r:\\epsilon}^\\ast q' \\in \\delta^\\ast$.\n\nThe proof proceeds by induction on $|w|$. The base case holds since each terminal is not nullable, and the inductive step follows directly from the construction of the lexing transducer.\n\nLemma 2. If $q \\xrightarrow{w: T_1 \\ldots T_k}^\\ast q'$ via the token-level lexing transducer for some incomplete token prefix $w$ of $L(G)$, then there exists a terminal $T$ producible along some path from $q'$ such that $T_1 \\ldots T_k T$ is terminal prefix of $L(G)$.\n\nProof sketch. By assumption, there exists a string $v$ such that $wv$ is in the language. Let $T_1 \\ldots T_k T_{k+1} \\ldots T_m $ be the lexed terminal sequence corresponding to $wv$, which is a sentence in the CFG $G$.\nSince $T_1 \\ldots T_k$ itself is not a complete sentence, the sequence $T_{k+1} \\ldots T_m$ must be non-empty, and in particular, terminal $T_{k+1}$ can be generated.\nThus, we conclude that $T_1 \\ldots T_k T_{k+1}$ is a terminal prefix of $L(G)$.\n\nTheorem 1. (Completeness) Given a prefix $w$ of $L(G)$, a token $v$ is not masked by Algorithm 6 (i.e., $v \\in V_{allowed}$) if the concatenation $wv$ is a prefix of $L(G)$.\n\nProof sketch. By Lemma 1, the lexing transducer produces $T_1 \\ldots T_k$ and reaches a state $q'$ such that $q_0 \\xrightarrow{w_r: \\epsilon}^\\ast q'$.\nSince $wv$ is a prefix of $L(G)$, again by Lemma 1, $q_0 \\xrightarrow{wv:T_1 \\ldots T_k T_{k+1} \\ldots T_m} q''$ for some state $q''$, which implies $q' \\xrightarrow{T_{k+1} \\ldots T_m} q''$.\nThen, by Lemma 2, there exists a terminal $T$ producible along some path from $q’$ such that $T_1 \\ldots T_k T_{k+1} \\ldots T_m T$ is a prefix of $L(G)$.\nTherefore, we have $v \\in T_{inv}(q', T_{k+1} \\ldots T_m T)$, which implies $v \\in V_{allowed}$.\n\nTheorem 2. (Soundness) Given a prefix $w$ of $L(G)$, a token $v$ is masked by Algorithm 6 (i.e., $v \\in V_{allowed}$) if the concatenation $wv$ is not a prefix of $L(G)$.\n\nThe detailed soundness proof (which we do not include here due to space limits) is similar in overall structure to the proof of Theorem 1. The proof also requires the additional fact that every sequence of terminals corresponds to the lex of a sequence of tokens in  $V^\\ast$. \n\n> Neither one of Propositions 3.4 and 3.5 have accompanying proofs. \n\nBoth propositions follow directly from the definition of PDAs and FSMs. We will provide formal proofs in the appendix. As a quick reference, a proof can also be found in Theorem 6.5 of [NewRef1]. Additionally, Theorem 6.17 provides intuition about how to construct an FSM that over-approximates the given PDA.\n\n[NewRef1] Hopcroft, John E. et al., \"Introduction to automata theory, languages, and computation.\"\n\n> … What is the precise difference between these two, and if they are not the same, what is the point of Figure 1(d)?\n\nWhile the token spanner table maps pairs of (state, token) to terminal sequences, the inverse token spanner table reverses this mapping for faster lookup in Algorithms 5–6, mapping each (state, terminal sequence) pair to the set of tokens capable of generating that sequence in that state. The token spanner table is used to compute $Re_{A \\circ V}$ and the inverse token spanner table. We will clarify this relationship in the revised paper.\n\n> Furthermore, in places where definitions are provided, they are not rigorous. For example, Definition 3.2 is lacking in clarity: what are q and q’? \n\nq and q’ are (existentially quantified) source and destination states, respectively, in the transition set of the token-level lexing transducer. We will clarify the meaning of the notation and provide more rigorous definitions in the revised paper.\n\n> What is the point of the second paragraph regarding “Maximal Munch Principle” (lines 145-156)?\n\nThis paragraph introduces the informal idea behind 1-lookahead lexing. This is an additional specification (beyond just maximal munch) on how the lexer should behave. Our lexing transducer is designed to satisfy both specifications. In the revised paper, we will clarify explicitly that these specifications are our design choice. Additionally, we will provide a formal proof in the appendix to demonstrate that the transducer indeed satisfies both specifications.", "claims_and_evidence": "It appears the claims are supported by clear and convincing evidence. The majority of the paper describes the new algorithm. For the online procedure, there is a bit of confusion, and a rigorous definition of the functions $A$ and $D$ would help the reader understand. For the reviewer’s understanding, is this method masking out other tokens that might also be allowed? The experiment section is strong and shows significant improvement over other methods. For the sake of completeness, it would be useful also to also report some sort of metric as regards to quality of the output using GreatGramma as well as other methods.", "methods_and_evaluation_criteria": "The methods appear to make sense for the problem at hand. The method mostly consists of an offline processing procedure in order to create an inverse token spanner table, which is then used at inference time.", "theoretical_claims": "Neither one of Propositions 3.4 and 3.5 have accompanying proofs. This would be useful in order to verify the claims, or to point the reader to another source proving the same result.", "experimental_designs_or_analyses": "The experimental design and analysis appears to be complete. As mentioned earlier though, the method would be even further motivated by reporting on the quality of the outputs via GreatGramma.", "relation_to_broader_scientific_literature": "Methods like verifiers and grammars are in general becoming more popular for language models. It appears as though some sort of supervision may be useful. Hence, methods to improve efficiency for such methods should allow the literature to continue to explore these directions with a more scalable approach.", "essential_references_not_discussed": "n/a", "other_strengths_and_weaknesses": "This paper appears to have a strong result. Yet, the paper is not particularly straightforward to follow. The reviewer suggests that, in order to improve clarity, the authors provide clear definitions in the beginning of sections and attempt to make Section 3 more concise and clear. For example, one point of confusion is what the “token spanner table” is, as mentioned in Figure 1. Later on, there is mention of an “inverse token spanner table.” What is the precise difference between these two, and if they are not the same, what is the point of Figure 1(d)? Furthermore, in places where definitions are provided, they are not rigorous. For example, Definition 3.2 is lacking in clarity: what are $q$ and $q’$? What is the point of the second paragraph regarding “Maximal Munch Principle” (lines 145-156)? It is unclear if the strict interpretation is being assumed or not.", "other_comments_or_suggestions": "See above", "questions_for_authors": "See above", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "SrK3IicC9U", "reviewer": "Reviewer_nQQ5", "summary": "The authors provide a more computationally efficient method, called GREATGRAMMA, for computing token masks for CFG-constrained decoding from LLMs. In particular, they address the misalignment between CFG terminals and the LLM token vocabulary, and tricks for speeding up online mask computation during decoding using relatively cheap preprocessing. Their method assumes that the constraint is expressed as a CFG whose terminal symbols are *chunks* of characters; these chunks are referred to as the \"terminals.\" Their preprocessing step builds a FST that maps LLM token sequences to character strings and another FST that maps character strings to terminal sequences. They compose them to form a single FST that maps LLM token sequences to terminal sequences. They precompute a table that maps FST states and terminal sequences to valid LLM tokens. Their method is limited to grammars with certain properties (for one, they must be deterministic). They show through experiments that GREATGRAMMA's preprocessing is a little slower than the competing OUTLINES, but its online mask computation is much, much faster.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their insightful feedback. In the revised paper, we will correct all typos, clarify the notation pointed out by the reviewer, and provide rigorous definitions and proofs in the appendix. Below, we provide a detailed response to each comment and question.\n\n> the method is limited to deterministic CFLs that satisfy certain properties\n\nAlthough we assumed a deterministic PDA for simplicity of implementation, determinism is not strictly necessary for our method. For more detail, please see our response to a similar question by reviewer q1Dz.\n\n> 227:How is this loop implemented?\n\nThis line is precomputed by a reachability algorithm (e.g., Floyd-Warshall Algorithm [NewRef2]) in the lexing transducer.\n\n[NewRef2] Floyd, Robert W. \"Algorithm 97: shortest path.\" Communications of the ACM 5.6 (1962)\n\n> no proofs of correctness or time/space complexity analyses\n> the reason why this approach is correct and necessary is a particularly weak part of the exposition\n\nComputing the set of realizable terminal sequences allows us to do exactly the amount of necessary work during parser preprocessing. We will improve the presentation to make this point clearer.\n\nFor proof sketches regarding correctness, please refer to our response addressing a similar point raised by Reviewer apti. Regarding complexity, the most computationally expensive procedures are Algorithms 4 and 5.\n\nAlgorithm 4 runs in time $O(|\\delta||\\Gamma|)$, in addition to the precomputation for line 227 which runs in $O(|Q_A|^3)$ time and $O(|Q_A|^2)$ space. Both $|Re_{A \\circ V}|$ and $|T_{inv}|$ are at most $|Q_A||V||\\Gamma|$, though empirically they tend to be much smaller since most combinations are infeasible.\nCFG parsing has time complexity $O(n^3)$ for general CFGs and $O(n)$ for deterministic CFGs. Consequently, computing $\\bar{A}$ and $\\bar{D}$ in Algorithm 5 takes $O(|Re_{A \\circ V}| \\cdot n^3)$ time for general CFGs and $O(|Re_{A \\circ V}| \\cdot n)$ time for deterministic CFGs, where $n$ denotes the length of the longest terminal sequence plus length of the current prefix.\nThe computation of sets $A$ and $D$ in Algorithm 5 runs in $O(|Q_A||Q_P||V||\\Gamma|)$ time and requires $O(|Q_A||Q_P||V|)$ space. In practice, time/space usage is often significantly smaller due to the sparsity in $T_{inv}$.\nIn practice, we observe that $|Q_A|, |Q_P| < 1000$, $|\\Gamma| < 100$ even for large grammars, including the Go, Java, and Python grammars used in our experiments.\n\n> Can you formally express what the mathematically correct solution to the token alignment problem is?\n\nFormally, given a context-free grammar $G$ and a lexer $Lex$, the token-aligned language $L^{Lex}(G)$ is defined as the set of $w \\in V^\\ast$ s.t. $\\exists T_1 \\dots T_k. Lex(w) = T_1 \\dots T_k \\wedge T_1 \\dots T_k \\in L(G)$. Correct token-aligned constrained decoding thus requires that any partial output is always a prefix of some sentence in $L^{Lex}(G)$.\n\n> it's not clear what the meaning of a cell in the token spanner table is\n> It's confusing that Fig 1(b) does not show an inverse table, but a table that maps states and single tokens to sequences of terminals.\n\nPlease see our response to a similar question by Reviewer apti.\n\n> 520: What does it mean for state q to recognize T? How do you determine what T is?\n\nThe lexing automaton recognizes the union of all the languages for each terminal. It is built via a product construction where each component automaton recognizes a specific terminal T. Thus, each final state of the product automaton corresponds to a terminal T. If multiple terminals T correspond to a single final state, one can either assign priorities or nondeterministically produce all possible tokens to support contextual lexing.\n\n> 250: When you say T can be generated along some path, do you mean a path ending in an accept state?\n\nWe say T can be generated along some path from q, when $q \\xrightarrow{w:T T_1 \\ldots T_k}^\\ast q’ \\in \\delta^\\ast$ for some $q’$ and $T_1 \\ldots T_k$.\n\n> Why is there a separation between characters and CFG terminals that is mediated by the lexer?\n\nLexers usually operate via finite automata, which efficiently match tokens at linear time with minimal lookahead. In contrast, CFG parsers incur higher overhead. Moreover, lexers effectively handle non-grammatical constructs, such as whitespace and comments. This separation ensures that the parser grammar remains concise.\n\n> How is EOS masking handled in your method?\n\nThe EOS symbol is treated as a token in the vocabulary, which generates a special end-of-parsing terminal. It behaves similarly to other tokens, except that it has transitions leading back to state $q_0$, which produce the end-of-parsing terminal in the lexing transducer.\n\n> What are the inputs/outputs of $T_{Re_{A \\circ V}}$?\n\nThe input alphabet is $Re_{A \\circ V}$, and the output alphabet is $\\Gamma$. This is similar to Figure 3, except that here the input alphabet consists of a sequence of terminals rather than characters.", "claims_and_evidence": "The empirical claims about runtime are well-supported by experiments.\n\nOn the other hand, the authors do not prove the correctness of their algorithms and do not provide asymptotic time/space complexity analysis, which I think is sorely needed.", "methods_and_evaluation_criteria": "Yes.", "theoretical_claims": "This paper does not provide proofs for its theoretical claims, but I think it should prove the correctness of its algorithms and give a time/space complexity analysis.", "experimental_designs_or_analyses": "To an extent, yes, but I would like the authors to follow up with proofs of correctness.", "relation_to_broader_scientific_literature": "They provide a faster, more practical method for CFG-constrained decoding than previous work, namely OUTLINES and SYNCODE. See their Section 6 for details.", "essential_references_not_discussed": "Not to my knowledge.\n\nAlthough light on detail, I believe this concurrent work uses a similar approach for token-character alignment by composing FSTs and CFGs: https://openreview.net/forum?id=xoXn62FzD0", "other_strengths_and_weaknesses": "**Strengths**\n\n1. The authors clearly state the limitations of their method.\n2. The paper is generally well-written, although I have issues with aspects of the exposition.\n3. The empirical results are very good.\n4. Good benchmarks.\n\n**Weaknesses**\n\n1. As the authors state, the method is limited to *deterministic* CFLs that satisfy certain properties.\n2. There are no proofs of correctness or time/space complexity analyses.\n3. The exposition of the method is a bit unclear at times. In particular, their method hinges upon their concept of the set of realizable tokens, but the reason why this approach is correct and necessary is a particularly weak part of the exposition. See also Comments or Suggestions.", "other_comments_or_suggestions": "1. The correctness of token alignment is a major issue. Can you formally express what the mathematically correct solution to the token alignment problem is?\n2. 047 right: Interesting!\n3. 087: Does this do things like strip whitespace and comments, as is done in a typical compiler? Or is the transformation bijective?\n4. 511: This should check for t_next = EOS. Also, I don't think you want to append EOS to x.\n5. 130: From this description, it's not clear what the meaning of a cell in the token spanner table is, much less how to construct it. It would be helpful to give a formal definition of what the value of each cell is supposed to be.\n6. 204: Is $q_0$ a typo?\n7. 520: What does it mean for state $q$ to recognize $T$? How do you determine what $T$ is?\n8. 250: When you say $T$ can be generated along some path, do you mean a path ending in an accept state?\n9. For some reason, the inputs and outputs of $\\mathcal{T}\\_{\\mathcal{A}}$, $\\mathcal{T}\\_\\mathcal{V}$, and $\\mathcal{T}\\_{\\mathcal{A} \\circ \\mathcal{V}}$ are a bit unclear from reading the text, partly because $\\mathcal{A} \\circ \\mathcal{V}$ is written in the reverse order of the inputs and outputs. It would be useful to spell this out in the text more explicitly. It took a while to figure out that $\\mathcal{T}\\_{\\mathcal{A} \\circ \\mathcal{V}}$ maps sequences of LLM tokens to sequences of CFG terminals.\n10. 249: There are some $\\exists$ quantifiers missing.\n11. 227: How is this loop implemented?\n12. 251 right: Is $Re\\_{\\mathcal{A} \\circ \\mathcal{V}}$ a typo?\n13. The wording of Proposition 3.4 is unclear. Do you mean if the PDA *starts* in state $q$ with stack $\\gamma$?\n14. The concepts of push and pop computations in PDAs from this paper may be useful to you: https://arxiv.org/abs/2210.06884\n15. It's confusing that Fig 1(b) does not show an *inverse* table, but a table that maps states and *single tokens* to *sequences of terminals*. This causes a lot of confusion later on.\n16. It wasn't clear until later in the paper that there are bounds on the size of the set of realizable tokens. This is important because otherwise it seems like the method requires exponential time/space.", "questions_for_authors": "1. Why is there a separation between characters and CFG terminals that is mediated by the lexer? It's always possible to implement the lexer directly within the CFG by modifying its rules and making its terminal symbols single characters. Is there some computational efficiency advantage to treating them separately?\n2. 058: Shouldn't it also include a mask for EOS? How is EOS masking handled in your method?\n3. What are the inputs and outputs of $\\mathcal{T}\\_{Re\\_{\\mathcal{A} \\circ \\mathcal{V}}}$?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "x40Dt6UKXh", "reviewer": "Reviewer_EMYM", "summary": "- The paper presents a new algorithm for grammar-constrained decoding (GCD) that significantly improves the efficiency of both offline preprocessing and online token masking. The key innovation is a combined analysis of the LLM token vocabulary and set of CFG terminals, which precomputes a lexer-state-dependent mapping between sequences of CFG tokens and individual LLM tokens.\n- The proposed method, implemented in a tool called GREATGRAMMA, achieves an average 17.71x speedup in offline preprocessing compared to related approaches while maintaining state-of-the-art online masking efficiency (5-32ms per token).\n- The approach is flexible, handling diverse grammars without prohibitive offline preprocessing costs, and efficient, maintaining low online token-masking overhead.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their insightful feedback. Below, we provide a detailed response to each comment and question.\n\n> The paper does not present detailed proofs for their theoretical claims\n> a more in-depth analysis of the properties of the realizable terminal sequences and their impact on the overall decoding process could be beneficial\n\nWe will provide a more rigorous formalization, correctness proofs, and time/space analysis in the appendix of the revised paper. For proof sketches regarding correctness, please refer to our response addressing a similar point raised by Reviewer apti and Reviewer nQQ5.\n\n>could you elaborate on how you plan to extend the approach to support more complex language constructs that require more than 1 - lookahead or context-dependent lexing?\n> You mentioned that the current implementation works under certain lexing assumptions. How would you evaluate the potential benefits and challenges of relaxing these assumptions to handle a broader range of language grammars?\n\nTo be clear, maximal munch and 1-lookahead are specifications about how a lexer is expected to behave, not limitations of our system. Lexers for real-world languages usually have these properties (including the ones we evaluated on: Python, Java, and Go). That being said, our lexing transducer can also be adapted to accommodate alternative lexer specifications. For instance, the lexing transducer can nondeterministically produce all possible tokenizations, enabling contextual lexing. However, this nondeterminism may increase the size of $Re_{A \\circ V}$ and the inverse token spanner table.\n\nIf the lexer requires more than one-token lookahead, a k-token lookahead can be implemented by encoding each pair (state, lookahead) as a single combined state in the lexing transducer, similar to an LR(k) parser [NewRef3]. However, this approach can significantly increase the size of the lexing transducer.\n\nWe will include this discussion in the revised version of the paper.\n\n[NewRef3] Knuth, Donald E. \"On the translation of languages from left to right.\" Information and control 8.6 (1965): 607-639.\n\n> In the experimental evaluation, you mentioned that XGRAMMAR encountered errors during preprocessing or decoding for all the grammars considered. Could you provide more details about these errors and how they might affect the comparison with GREATGRAMMA?\n\nXGrammar encountered a segmentation fault when decoding with the Go grammar, aborted without displaying a detailed error message after compiling the Java grammar for several minutes, and entered an infinite loop during the initial token generation step for the Python grammar. While we have not investigated the exact cause of these errors in XGrammar, we conjecture that they arise because XGrammar operates on byte-level pushdown automaton, which are significantly more complex than terminal-level pushdown automaton.\nSimilar problems in XGrammar have also been observed with other grammars: https://github.com/mlc-ai/xgrammar/issues/127. According to the github issue, the runtime overhead increases significantly due to nondeterminism caused by the overlap between identifier and keyword terminals. Note that in GreatGramma the terminal-level PDA in this example is still deterministic: the nondeterminism is purely at the terminal-level, which is resolved by the separate lexer.\n\n> However, it does not discuss other relevant works such as Grammar-Aligned Decoding (Park et al., 2024) or Synchromesh (Poesia et al., 2022)\n\nThe paper briefly mentions GAD in the context of evaluating the effectiveness of GCD (lines 330–333). While existing studies (Geng et al., 2023; Beurer-Kellner et al., 2024) demonstrate that GCD can improve downstream task performance, other recent work (Tam et al., 2024 [NewRef4]; Park et al., 2024) highlights that GCD can also negatively impact the quality of generated outputs. Our approach is orthogonal to these methods and can be integrated with techniques proposed by Park et al. (2024) or Banerjee et al. (2025) [NewRef5] to mitigate such negative effects. We will include this discussion on the effectiveness of GCD in Section 6. \n\nSyncromesh emphasizes checking semantic constraints beyond grammatical correctness, we will briefly discuss this extension as well.\n\n[NewRef4] Tam, Zhi Rui, et al. \"Let Me Speak Freely? A Study On The Impact Of Format Restrictions On Large Language Model Performance.\" EMNLP 2024: Industry Track.\n\n[NewRef5] Banerjee, Debangshu, et al. \"CRANE: Reasoning with constrained LLM generation.\" arXiv (2025).\n\n> The paper also does not mention the work on constrained decoding using FSTs by Koo et al. (2024)\n\nThe paper briefly introduces the work of Koo et al. when presenting the detokenizing transducer in Section 3.1. However, we agree that this relevant work deserves further discussion. We extended their work to accommodate a structure consisting of a separate lexer and parser and will include this discussion in Section 6.", "claims_and_evidence": "- The claims made in the paper are generally supported by clear and convincing evidence. The authors provide detailed algorithm descriptions, theoretical analysis, and experimental results.\n- They demonstrate the effectiveness of their approach through comparisons with existing GCD tools (OUTLINES, SYNCODE, and XGRAMMAR) on several benchmarks.\n- For instance, Table 1 shows that GREATGRAMMA's offline preprocessing is significantly faster than SYNCODE and its online masking is faster than both SYNCODE and OUTLINES.", "methods_and_evaluation_criteria": "- The proposed methods make sense for the problem at hand. The approach addresses the key challenge of token misalignment between LLMs and CFGs by preprocessing the lexer and parser in tandem.\n- The evaluation criteria, including offline preprocessing time and online per-token overhead, are appropriate for assessing the performance of GCD tools.", "theoretical_claims": "- The paper does not present detailed proofs for their theoretical claims, but the algorithms and concepts are well-founded.\n- The authors provide references to existing literature for some of the theoretical foundations, such as finite-state automata and pushdown automata.\n- The correctness of the algorithms is mostly supported by the experimental results.", "experimental_designs_or_analyses": "- The experimental designs are sound and valid. The authors conducted experiments using three different tokenizers and several programming language grammars.\n- They measured both offline preprocessing time and online per-token overhead, which are critical metrics for evaluating GCD tools.\n- The results are presented in a clear and organized manner, with tables and figures that effectively communicate the findings.", "relation_to_broader_scientific_literature": "- The key contributions of the paper are related to several prior works in the field of grammar-constrained decoding. The authors build upon existing approaches such as SYNCODE and DOMINO.\n- Compared to SYNCODE, GREATGRAMMA offers faster offline preprocessing and similar or better online masking efficiency.\n- The approach also integrates ideas from XGRAMMAR, such as preprocessing context-independent tokens, but with improved efficiency and scalability.", "essential_references_not_discussed": "- The paper references several related works on grammar-constrained decoding (GCD), including SYNCODE, DOMINO, and XGRAMMAR. However, it does not discuss other relevant works such as Grammar-Aligned Decoding (Park et al., 2024) or Synchromesh (Poesia et al., 2022), which also address the problem of aligning LLM outputs with grammatical constraints. These works provide additional context and comparisons that could enhance the understanding of GREATGRAMMA's contributions.\n   - The paper also does not mention the work on constrained decoding using finite-state transducers (FSTs) by Koo et al. (2024), which is directly relevant to the preprocessing and token masking techniques used in GREATGRAMMA.", "other_strengths_and_weaknesses": "- **Strengths:**\n    - **Originality:** The approach proposed in the paper, particularly the combined analysis of the LLM token vocabulary and CFG terminals, as well as the introduction of the token spanner table, is novel. This innovation addresses a significant challenge in the field of grammar-constrained decoding.\n    - **Significance:** The results are important for improving the efficiency of constrained decoding in large language models, which has practical implications for applications like code generation and structured data formatting.\n    - **Clarity:** The paper is well-written and well-organized. The authors provide a clear explanation of the problem, their approach, algorithms, and experimental results. The use of figures to illustrate the lexing transducer, detokenizing transducer, and token spanner table helps in understanding the complex concepts.\n- **Weaknesses:**\n    - **Limitations:** As mentioned in the paper, the current implementation has some limitations. For example, it works under the maximal munch principle and 1-lookahead lexing, which may not support all language constructs. Additionally, the approach may not handle cases where the same input sequence must be lexed differently depending on the parsing context.\n    - **Theoretical Depth:** While the paper provides an algorithmic and conceptual description of the proposed method, some theoretical aspects could be explored further. For example, a more in-depth analysis of the properties of the realizable terminal sequences and their impact on the overall decoding process could be beneficial.\n    - **Application Scope:** The paper primarily focuses on grammar-constrained decoding for structured outputs like code snippets. However, the approach could be extended to other domains, such as natural language generation with specific syntax requirements, which is not discussed in detail.", "other_comments_or_suggestions": "No obvious typographical errors were observed in the provided text.", "questions_for_authors": "1. Regarding the limitations in handling lexing ambiguities, could you elaborate on how you plan to extend the approach to support more complex language constructs that require more than 1 - lookahead or context - dependent lexing? How would a successful extension impact the performance and applicability of GREATGRAMMA?\n    - If the authors have a clear plan and potential solutions for handling these cases, it would strengthen the paper's future work section and indicate a better understanding of the problem domain.\n2. In the experimental evaluation, you mentioned that XGRAMMAR encountered errors during preprocessing or decoding for all the grammars considered. Could you provide more details about these errors and how they might affect the comparison with GREATGRAMMA?\n    - Understanding the specific issues with XGRAMMAR would help in assessing the fairness of the comparison and determining whether GREATGRAMMA's advantages are as significant as reported.\n3. You mentioned that the current implementation works under certain lexing assumptions. How would you evaluate the potential benefits and challenges of relaxing these assumptions to handle a broader range of language grammars?\n    - The authors' perspective on this could provide insight into the scalability and generalizability of their approach.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: The paper proposes an efficient method for gammar-constrained decoding (GCD) that aims to facilitate structured output generation (e.g., json formats). All the reviewers appreciated that the proposed method is simple and effective, with strong empirical results. Several reviewers mentioned presentation clarity issues, and the authors were able to provide satisfactory responses during the rebuttal. Due to the unanimous positive support from the reviewers, we recommend acceptance.
Decision: Accept (poster)