Flexible and Efficient Grammar-Constrained Decoding

We thank the reviewer for their insightful feedback. Below, we provide a detailed response to each comment and question.

The paper does not present detailed proofs for their theoretical claims a more in-depth analysis of the properties of the realizable terminal sequences and their impact on the overall decoding process could be beneficial

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

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? 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?

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

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

We will include this discussion in the revised version of the paper.

[NewRef3] Knuth, Donald E. "On the translation of languages from left to right." Information and control 8.6 (1965): 607-639.

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?

XGrammar 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. Similar 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.

However, it does not discuss other relevant works such as Grammar-Aligned Decoding (Park et al., 2024) or Synchromesh (Poesia et al., 2022)

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

Syncromesh emphasizes checking semantic constraints beyond grammatical correctness, we will briefly discuss this extension as well.

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

[NewRef5] Banerjee, Debangshu, et al. "CRANE: Reasoning with constrained LLM generation." arXiv (2025).

The paper also does not mention the work on constrained decoding using FSTs by Koo et al. (2024)

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

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.

the method is limited to deterministic CFLs that satisfy certain properties

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

227:How is this loop implemented?

This line is precomputed by a reachability algorithm (e.g., Floyd-Warshall Algorithm [NewRef2]) in the lexing transducer.

[NewRef2] Floyd, Robert W. "Algorithm 97: shortest path." Communications of the ACM 5.6 (1962)

no proofs of correctness or time/space complexity analyses the reason why this approach is correct and necessary is a particularly weak part of the exposition

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

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

Algorithm 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. CFG 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. The 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}$. In 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.

Can you formally express what the mathematically correct solution to the token alignment problem is?

Formally, 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)$.

it's not clear what the meaning of a cell in the token spanner table is 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.

Please see our response to a similar question by Reviewer apti.

520: What does it mean for state q to recognize T? How do you determine what T is?

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

250: When you say T can be generated along some path, do you mean a path ending in an accept state?

We 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$.

Why is there a separation between characters and CFG terminals that is mediated by the lexer?

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

How is EOS masking handled in your method?

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

What are the inputs/outputs of $T_{Re_{A \circ V}}$?

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

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

Below, we provide a detailed response to each comment and question.

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.

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

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

(267, left column) , $T_{inv}(q, \alpha)$, it appears that $\alpha$ should really be $T_1 \ldots T_k T$ instead.

Thanks, we will resolve the conflicting notation in the revised version of the paper.

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?

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

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

Does the PDA need to be deterministic? If so, could you mention this explicitly early in the paper?

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

We thank the reviewer for their insightful feedback. Below, we provide a detailed response to each comment and question.

is this method masking out other tokens that might also be allowed?

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

Lemma 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$ if 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$.

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

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

Proof 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$. Since $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. Thus, we conclude that $T_1 \ldots T_k T_{k+1}$ is a terminal prefix of $L(G)$.

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

Proof 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'$. Since $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''$. Then, 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)$. Therefore, we have $v \in T_{inv}(q', T_{k+1} \ldots T_m T)$, which implies $v \in V_{allowed}$.

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

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

Neither one of Propositions 3.4 and 3.5 have accompanying proofs.

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

[NewRef1] Hopcroft, John E. et al., "Introduction to automata theory, languages, and computation."

… What is the precise difference between these two, and if they are not the same, what is the point of Figure 1(d)?

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

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’?

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

What is the point of the second paragraph regarding “Maximal Munch Principle” (lines 145-156)?

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