Source-linked AI summary
Stay Within Your Bounds: Distance-Guided Decoding for Guaranteed Context-Free Grammar Compliance
Vincenzo Collura, Karim Tit, Eleonora Giunchiglia, Mike Papadakis, Maxime Cordy
TL;DR
Local prefix feasibility can leave context-free grammar decoding unable to reach acceptance within tokenizer and budget constraints. SWYB uses bounded pushdown summaries and distance-guided beam search to prune and rank continuations. Across JSON, SQL, and LTL, it reports perfect syntactic validity with improved task-specific performance, subject to stack-height and exploration-budget limits.
Problem
Local prefix feasibility does not ensure that a context-free grammar continuation reaches acceptance within the remaining token budget.
Method
SWYB computes bounded pushdown reachability summaries and token-distance estimates offline, then uses them for tokenizer-aware pruning and beam-search reranking.
Results
Across JSON, SQL, and LTL, SWYB consistently achieves perfect syntactic validity and improves task-specific accuracy over existing methods.
Takeaways & Limitations
The decoder provides guaranteed context-free grammar compliance while maintaining competitive perplexity and decoding time.
Takeaways & Limitations
Performance and coverage depend on the stack-height bound H and exploration budget B, which can require slower online computation or increase runtime.
Abstract
from arXiv · showhide
Grammar-constrained decoding helps large language models produce syntactically valid structured outputs, such as code, JSON, and SQL. For context-free grammars, many practical decoders enforce local prefix feasibility: each token must keep the current prefix extendable to some valid completion. Yet, under tokenizer-grammar mismatch and finite token budgets, feasible prefixes may still fail to reach acceptance. We propose a lookahead-guided decoding framework for context-free grammars based on pushdown automata. Offline, we compute bounded pushdown summaries with reachability labels and upper-bound distances to acceptance. Online, these estimates guide horizon-aware pruning and beam search. The resulting decoder is syntactically sound: every output is accepted by the target grammar. Experiments on JSON, SQL, and Linear Temporal Logic (LTL) show both consistent syntactic validity and improved completion quality over existing baselines.
1 Introduction
SWYB addresses the gap between locally feasible prefixes and guaranteed acceptance under tokenizer mismatch and finite budgets. It combines tokenizer-aware PDA validation, bounded lookahead, distance estimates, and beam search to produce syntactically sound structured outputs.
- Local prefix masking prevents immediate syntax violations but does not quantify progress toward acceptance.
- SWYB computes bounded pushdown summaries with reachability labels and token-level upper-bound distances to acceptance.These estimates guide online pruning and reranking during beam search.
- Tokenizer-aware consumption matches subword tokens against PDA transitions, while automaton-proposed candidates supplement model top-k tokens.Candidates are validated through budgeted successor exploration before beam updates.
- SWYB is designed as a sound decoding framework for context-free grammar-constrained LLM generation.Its contributions include combining model top-k tokens, automaton proposals, and budgeted PDA exploration.
- Experiments on JSON, SQL, and LTL show consistent syntactic correctness and improved completion quality over existing baselines.
2 Related Work
Related work spans grammar masking, global control, pushdown reachability, and program constraints. SWYB targets the missing combination of CFG/PDA prefix safety with budget-aware acceptance guidance.
- Constrained decoding methods differ by constraint class, prefix feasibility, and use of lookahead or remaining-budget information.Table 1 positions methods along these three axes.
- Grammar masking: Local masking keeps prefixes feasible but does not indicate whether acceptance is reachable within the remaining budget.
- Global control: Global-control methods use automata, dynamic programming, probabilistic steering, or sampling-based inference to reason about future completions.Direct finite-state value computation is inapplicable to PDAs because their configurations include unbounded stacks.
- Reachability analysis: Pushdown reachability work supplies finite stack summaries, saturation procedures, and weighted path quantities that inform SWYB’s decoding design.
- Program constraints: SWYB complements type-, program-, and diffusion-oriented approaches by adding sound distance-guided lookahead to CFG/PDA decoding.
- Budget saturation problem: Local methods can saturate as budgets increase because valid actions may expand complex structures without guiding closure toward global constraints.
3 CFG-Constrained Decoding as a PDA Reachability Problem
The paper formulates CFG-constrained decoding through an equivalent PDA and extends configurations to represent partially consumed tokenizer strings. It then computes bounded reachability and token-cost estimates for budget-aware search.
- Context-free grammars and pushdown automata define the same class of languages, enabling the constraint to be represented by a PDA.
- A PDA is specified by control states, input and stack alphabets, transitions, an initial state and stack symbol, and accepting states.
- Token-level configurations: Tokenizer-aware configurations add an open terminal prefix so tokens can represent terminals, terminal prefixes, or strings crossing terminal boundaries.The Consume function maps a token and extended configuration to reachable extended configurations.
- Reachability and token distance: Under stack-height bound H, bounded pushdown summaries use saturation-style reachability analysis to label summarized configurations.
- Reachability and token distance: Terminal transitions receive weights equal to minimum required LLM-token counts, while epsilon transitions receive weight zero.Weighted Pre* computes minimum accumulated token cost to acceptance under the bound.
- Budget-aware pruning: If the remaining budget K is below the estimated distance dH(q, γ), the decoder prunes the configuration because no bounded accepting continuation fits.
- Objective: SWYB optimizes an approximate highest-probability PDA-accepted sequence within token budget T because exact autoregressive MAP decoding is generally intractable.
4 Proposed Method
SWYB combines tokenizer-aware candidate generation with bounded pushdown reachability and distance estimates to guide beam search toward accepted outputs within the token budget. It guarantees syntactic soundness and preserves a certified completion when the initial distance bound fits the budget, but is not search-complete.
- Overview: SWYB is a two-phase decoder for CFG constraints represented as pushdown automata, with offline summaries and online beam search.The offline phase computes bounded summaries; the online phase validates, prunes, and ranks candidate continuations.
- Offline computation: Offline, SWYB computes bounded summaries with reachability labels and token-distance estimates, caching them for reuse across prompts.Unseen configurations can be computed on the fly, while out-of-bounds or unreachable configurations are discarded.
- Candidate generation: At each step, SWYB combines model top-k tokens with tokenizer-aware automaton proposals compatible with admissible PDA continuations.Automaton proposals can recover structurally useful tokens outside the model’s top-M candidates.
- Horizon-aware search: Successor exploration retains only candidates whose distance estimates certify completion within the remaining horizon, discarding tokens with dH(q′, γ′) > K −1.Distance estimates also promote tokens that make progress toward acceptance.
- Guarantees: SWYB is not search-complete because bounded successor exploration and finite beam width may omit valid completions.Its completion guarantee applies when the initial configuration has a certified continuation within the available budget and bound.
- Guarantees: Every returned output is accepted by the target PDA, and dH(e0) ≤T guarantees that SWYB returns at least one accepted output.The proof maintains a witnessing beam through decoding and returns an accepting beam at the token limit.
5 Experiments
SWYB is evaluated on JSON, SQL, and LTL across three instruction-tuned models using constraint-satisfaction and generation-quality metrics. Across domains and architectures, it provides consistent syntax guarantees and stronger task quality, with moderate decoding overhead and grammar-dependent preprocessing costs.
- Setup: Experiments cover JSON, SQL, and LTL using LLAMA-3.1-8B-INSTRUCT, LLAMA-3.2-3B-INSTRUCT, and QWEN2.5-7B-INSTRUCT.Using three model families and sizes assesses robustness across base architectures.
- Metrics: The evaluation measures both constraint satisfaction and generation quality, including validity, schema or task accuracy, perplexity, and decoding time.JSON reports syntactic validity and schema validity; SQL reports syntactic correctness and execution accuracy; LTL reports syntactic correctness and task accuracy.
- Main findings: SWYB is the only method achieving 100% syntactic correctness in every setting and 100% JSON schema validity across all models.Other constrained decoders show less consistent gains, particularly on Qwen2.5-7B where the unconstrained model is already strong.
- Ablations: Beam Search provides the largest ablation gains, while Distance-Guided Scoring adds smaller consistent accuracy improvements with negligible decoding overhead.Combining both components yields the best efficiency-quality trade-off while preserving 100% syntactic correctness.
- SQL: On SQL, SWYB achieves perfect syntax and the highest execution accuracy across all three base models.Sample-Verify can achieve perfect or near-perfect syntax but does not improve execution accuracy to the same extent.
- LTL: On LTL, SWYB consistently achieves 100% syntactic correctness and the highest task accuracy across all three models.The strongest combination of syntax guarantees and task accuracy carries moderate decoding-time overhead.
6 Conclusion
SWYB combines bounded pushdown lookahead with distance-guided decoding to provide grammar compliance under context-free constraints. It achieves perfect syntactic validity across diverse evaluations while improving task-specific accuracy and maintaining competitive efficiency.
- SWYB provides guaranteed context-free grammar compliance through distance-guided decoding.
- SWYB augments token-level validation with bounded pushdown summaries and upper-bound distance estimates to acceptance.These estimates support budget-aware pruning and reranking during beam search.
- Configurations estimated to exceed the remaining token horizon are discarded, while structurally progressive tokens receive soft promotion.
- Perfect syntactic validity across three diverse base models was achieved on JSON, SQL, and LTL generation.SWYB also improved task-specific accuracy over Sample-Verify, SynCode, XGrammar, and GenLM.
- SWYB maintained competitive perplexity and decoding time, offering a favorable trade-off between guarantee and efficiency.
Limitations
SWYB's bounded lookahead is limited by the stack-height bound H and exploration budget B. These parameters trade precomputation coverage and lookahead detail against runtime, while soundness remains preserved under the stated conditions.
- The stack-height bound H limits the configurations included in offline precomputation.If H is too low, missing configurations may require slower online distance computation.
- The exploration budget B controls how many intermediate PDA configurations are examined.Larger B increases runtime but enables more detailed lookahead.
- For small grammars such as LTL, exhaustive exploration is feasible and incurs little overhead.
- With minimal budget B = 1 and sufficiently large H, the algorithm remains sound because soundness only requires one valid completion within the remaining token budget.
Ethics Statement
LLMs were used only for limited copy-editing and LaTeX formatting tasks. The authors state that they reviewed and verified the generated output and retained responsibility for the final content.
- LLMs suggested alternative phrasings for a few sentences and generated LaTeX code for tables and formatting.
- LLMs were not used for research design, analysis, or interpretation of results.
- The authors reviewed and verified all generated output and assumed full responsibility for the final content.
A System specifications
The experiments ran on a machine equipped with an Intel Xeon Silver 4416+ CPU and an Nvidia L40S GPU. The listed system provides 20 CPU cores, 40 threads, and 48 GB of GPU memory.
- Experiments used an Intel Xeon Silver 4416+ CPU with 20 cores, 40 threads, and 2.00/3.90 GHz frequency.
- The machine included an Nvidia L40S GPU with 48 GB GDDR6 and 18176 CUDA cores.It also had 142 RT cores and 568 Tensor Cores.
B Ablation studies
The ablations show that beam search substantially improves task quality, while Distance-Guided Scoring adds smaller gains; syntax correctness remains guaranteed. Increasing the JSON token budget alone does not materially improve schema satisfaction.
- Ablation findings: Four beams increase Llama-3.2-3B SQL execution accuracy from 26.0% to 50.9%, with similar improvements across models and LTL.Beam Search provides the largest ablation gains.
- Ablation findings: 100% syntactic correctness is preserved across every SQL and LTL ablation configuration, including settings without Beam Search or DGS.The guarantee is independent of these components.
- Ablation findings: DGS consistently improves execution accuracy by smaller amounts, while α trades off language-model fluency against faster constraint satisfaction.Lower α favors model fluency; higher α favors satisfying constraints more quickly.
- Budget study: Larger JSON budgets from 512 to 4096 tokens do not materially improve schema satisfaction, which remains substantially below 100% across methods and models.The experiment extends the budget to as much as 40× the default.
- Running example: The running example uses a beam width of M = 2 and distance function dH to prune continuations that cannot reach acceptance within the remaining budget.The example sets T = 3, α = 0.25, and stack-height bound H = 5.
D.4 Final Result
The final example selects the highest-scoring accepting sequence after distance-guided beam search. The procedure illustrates budget-aware pruning, while the referenced tables vary the available token budget up to 4096.
- Final selection: The final beam contains two accepting sequences, and the method selects the one with the highest score.The example therefore combines acceptance filtering with score-based selection.
- Final selection: The example outputs the string ()x after discarding candidates that cannot reach a valid string within the token budget.Distance-guided beam search explores derivations while retaining plausible accepting solutions.
- Budget study: The budget study evaluates Max New Tokens values of 512, 1024, 2048, and 4096.These values are represented in Tables 7–10.
- PDA example: The running example’s PDA transition specification is presented in Table 11.The table supplies the transitions for the balanced-parentheses language followed by x.