Stay Within Your Bounds: Distance-Guided Decoding for Guaranteed Context-Free Grammar Compliance

AI summary

Overview

• Research area: Artificial intelligence / large language model generation, specifically grammar-constrained decoding with formal-language guarantees.
• Technical level: Advanced. The paper assumes familiarity with context-free grammars (CFGs), pushdown automata (PDA), weighted pushdown systems, beam search, and subword tokenization.
• Scope: The paper introduces SWYB, a decoding framework that adds bounded pushdown reachability summaries and token-distance-to-acceptance estimates to CFG-constrained LLM decoding, and evaluates it on JSON, SQL, and Linear Temporal Logic (LTL) generation across three instruction-tuned models.

What This Paper Is About

Grammar-constrained decoders typically check only local prefix feasibility: whether the current prefix can still be extended into some valid completion. Under tokenizer–grammar mismatch and a finite token budget, a prefix can remain locally feasible while drifting into configurations that cannot be completed within the remaining tokens, so the final output may still be syntactically invalid. The paper's goal is to guarantee that every returned output is accepted by the target CFG while also improving completion quality, by guiding decoding with estimates of how many tokens are still needed to reach acceptance.

Key Contributions

1. A sound pushdown lookahead mechanism built on bounded reachability summaries and token-level distance-to-acceptance estimates.
2. A tokenizer-aware decoding algorithm that combines model top-k tokens, automaton-proposed "backup" tokens, and budgeted PDA successor exploration.
3. A distance-guided scoring rule that softly promotes tokens making measurable structural progress toward acceptance, plus budget-aware pruning of configurations whose estimated completion cost exceeds the remaining horizon.
4. Experiments on JSON, SQL, and LTL grammars across three base models, showing consistent syntactic correctness and improved completion quality over existing baselines.

Main Findings

• Perfect syntactic validity across all settings: SWYB is the only method that achieves 100% syntactic correctness on all three domains and all three base models (Llama-3.1-8B-Instruct, Llama-3.2-3B-Instruct, Qwen2.5-7B-Instruct). On JSON this also corresponds to 100% schema validity in every setting.
• JSON (json-mode-eval, 100 examples): SWYB reaches 100.0 syntactic and 100.0 schema validity with decoding times of 3.96 s, 3.46 s, and 4.05 s, and perplexities of 1.13, 1.14, and 1.11. For comparison, the Base LM scores 63.7 / 57.1 (Llama-3.1-8B), 56.4 / 49.4 (Llama-3.2-3B), and 93.6 / 87.4 (Qwen2.5-7B); Guidance 96.0 / 89.0, Outlines 94.0 / 90.0, XGrammar 93.0 / 85.0, and SynCode 88.0 / 79.0 on Llama-3.1-8B. SWYB uses α = 0.25 and 2 beams on this task.
• SQL (Spider validation split, 1,034 examples): SWYB achieves 100.0 syntactic correctness and the highest execution accuracy in every setting: 61.1, 51.5, and 62.8 for Llama-3.1-8B, Llama-3.2-3B, and Qwen2.5-7B. Base LM execution accuracy is 53.8, 46.3, and 61.4; Sample-Verify 57.5, 47.8, and 61.5; SynCode 43.2, 39.6, and 43.2; GenLM 59.2, 49.4, and 51.9. SWYB uses beam width 4 and α of 0.25, 0.75, and 0.50 respectively.
• LTL (drone planning task, 6,185 examples): SWYB achieves 100.0 syntactic correctness and the highest task accuracy across all three models: 29.6, 22.1, and 31.6, versus 22.1, 9.6, and 30.9 for the Base LM, 22.2, 9.3, and 30.6 for Sample-Verify, and 24.4, 15.2, and 31.0 for SynCode. SynCode reaches 100% syntax only for Qwen2.5-7B (99.9, 99.9, 100.0). SWYB uses beam width 4 and α of 0.75, 0.50, and 0.50.
• Budget saturation is real: Existing local constrained decoders largely saturate for token budgets above T = 512; raising the budget from T = 120 to T = 4096 (up to 40×) yields little or no improvement in JSON schema satisfaction, even when syntax validity reaches 100%.
• Cost profile: SWYB is slower than lightweight masking methods but faster than Sample-Verify and competitive with GenLM at higher particle counts on the Llama models, while being slower on Qwen. Its perplexity is the best or second-best in all settings.
• Precomputation cost varies sharply by grammar: CFG-to-PDA conversion is linear in grammar size (0.67 s for SQL). Summary precomputation required 3 h 40 min for SQL with H = 13 (supporting up to three nested queries) but only 0.42 s for LTL with H = 50 (supporting up to 50 nested parentheses); schema-specific JSON grammars took 0.29 s on average (± 0.11 s). These steps are grammar-dependent, not dataset-dependent, and are reused across prompts.
• Ablations: Beam Search provides the largest gains, substantially improving SQL execution accuracy and LTL semantic accuracy while reducing perplexity; Distance-Guided Scoring adds smaller but consistent task-accuracy improvements at negligible decoding overhead. Syntactic correctness stays at 100% in every ablation configuration.
• Theory: Theorem 4.1 establishes syntactic soundness — every output returned by SWYB is accepted by the PDA — and completion: if the initial configuration satisfies d_H(e_0) ≤ T, SWYB returns at least one accepted output. The method is not search-complete because of bounded successor exploration and finite beam width.

Methodology in Plain English

Any context-free grammar can be represented as a pushdown automaton, a machine with a finite set of states plus an unbounded stack. Because the stack is unbounded, the configuration space is infinite and direct finite-state lookahead does not apply.

SWYB works in two phases. Offline, the grammar is converted to a pushdown automaton, and the method builds a bounded summary of configurations (with stack height capped at H). Each summarized configuration gets two labels: whether it can still reach an accepting configuration, and an upper-bound estimate of the minimum number of LLM tokens needed to get there. To compute token costs, each terminal-consuming transition is weighted by the minimum number of model tokens needed to produce that terminal — for terminals defined by a regular expression, the shortest string in the language is found and tokenized, and epsilon transitions get weight zero. A weighted predecessor-saturation algorithm then computes the minimum accumulated token cost to acceptance.

Online, the decoder runs a beam search that keeps, for each beam, the generated prefix, a score, and an extended configuration consisting of the PDA state, the stack, and any partially matched terminal. At each step it forms a candidate set from the model's top-k tokens plus automaton-proposed tokens (the first token of the remaining suffix of any grammar transition compatible with the current partial terminal). Each candidate is executed through the PDA, explored up to a bound of B successors, and filtered: successors whose estimated distance to acceptance exceeds the remaining token budget are discarded. Surviving tokens are scored using a ramping coefficient that blends the model logit with the best viable logit, pushing tokens with more favorable distance estimates toward the top. The best M beams are kept, and the algorithm returns the best accepting beam. If the offline estimate says acceptance cannot be certified within the budget and the stack bound H, the method reports this rather than returning an invalid output.

Why This Matters

This work closes a gap between two research lines: practical grammar-masking decoders, which enforce prefix feasibility but not completed-output validity, and global-control methods, which use lookahead but have largely been restricted to regular grammars or deterministic CFGs. SWYB targets general CFG/PDA constraints with both prefix safety and budget-aware acceptance guidance — a combination the authors identify as missing from existing practical systems. It also shows that more tokens alone do not fix local decoding's myopia.

Real-world applications:

• Structured data generation: producing JSON records that conform to a required schema, for API responses, configuration files, or tool-calling payloads.
• Text-to-SQL systems: generating SQL queries that are guaranteed to parse and that execute correctly against a target database.
• Formal specification synthesis: generating LTL formulas for planning tasks, where outputs must be both syntactically well-formed and semantically equivalent to a ground-truth specification.
• Any parser-fronted pipeline where invalid output would be rejected downstream, violate an interface contract, or fail to execute.

Industry relevance: the guarantee that every returned output is grammar-valid is directly useful wherever LLM outputs must be consumed by a parser or compiler. The cost model is also relevant to deployment — grammar precomputation is paid once and reused across prompts, though it can be expensive for complex grammars (3 h 40 min for SQL at H = 13), while per-token decoding overhead is moderate.

Future Directions

• Reducing the offline precomputation cost, which reached 3 h 40 min for SQL with H = 13, and understanding how the stack bound H trades off against certified completion.
• Extending the approach beyond context-free languages, since the paper notes that global control is much harder for CFGs than for regular constraints and other constraint classes remain unaddressed.
• Tightening the distance estimates so they better reflect the true minimum token cost, which could sharpen the reranking signal given that DGS produced smaller gains than beam search.
• Comparing against a broader set of baselines: DOMINO, GreatGramma, and SEM-CTRL were excluded for lack of runnable public code, and no public implementation natively supported the LTL grammar.
• Investigating adaptive beam widths or horizons, since SWYB is not search-complete and its performance depends on the bounded successor exploration budget B and beam width M.

Target Audience

Researchers and practitioners in natural language processing, formal methods, and program synthesis working on constrained or structured generation, especially those concerned with guarantees rather than heuristics. It is also relevant to engineers building LLM systems that emit JSON, SQL, or other grammar-governed artifacts, and to readers interested in adapting pushdown-system reachability analysis to decoding. A background in automata theory and probabilistic decoding is needed to follow the method and the soundness proof.

Authors’ abstract

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.