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

• Local prefix masking prevents immediate syntax violations but does not quantify progress toward acceptance.Source: §1 · p. 1
• 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.Source: §1 · pp. 1–2
• 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.Source: §1 · p. 2, Figure 1 · p. 2
• 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.Source: §1 · p. 2
• Experiments on JSON, SQL, and LTL show consistent syntactic correctness and improved completion quality over existing baselines.Source: §1 · p. 2

• 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.Source: §2 · p. 2, Table 1 · p. 3

Grammar masking

• Local masking keeps prefixes feasible but does not indicate whether acceptance is reachable within the remaining budget.Source: §2 · p. 3

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.Source: §2 · p. 3

Reachability analysis

• Pushdown reachability work supplies finite stack summaries, saturation procedures, and weighted path quantities that inform SWYB’s decoding design.Source: §2 · p. 3

Program constraints

• SWYB complements type-, program-, and diffusion-oriented approaches by adding sound distance-guided lookahead to CFG/PDA decoding.Source: §2 · p. 3

Budget saturation problem

• Local methods can saturate as budgets increase because valid actions may expand complex structures without guiding closure toward global constraints.Source: §2 · p. 3

• Context-free grammars and pushdown automata define the same class of languages, enabling the constraint to be represented by a PDA.Source: §3 · p. 4
• A PDA is specified by control states, input and stack alphabets, transitions, an initial state and stack symbol, and accepting states.Source: §3 · p. 4

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.Source: §3 · p. 4

Reachability and token distance

• Under stack-height bound H, bounded pushdown summaries use saturation-style reachability analysis to label summarized configurations.Source: §3 · p. 4
• 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.Source: §3 · p. 4

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.Source: §3 · p. 4

Objective

• SWYB optimizes an approximate highest-probability PDA-accepted sequence within token budget T because exact autoregressive MAP decoding is generally intractable.Source: §3 · p. 4

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.Source: §4.1 · pp. 4–5

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.Source: §4.1 · p. 5

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.Source: §4.2 · p. 5

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.Source: §4.3 · pp. 5–6, §4.4 · p. 6

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.Source: §4.5 · p. 6
• 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.Source: §4.5 · p. 6

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.Source: §5 · pp. 6–7

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.Source: §5 · p. 8

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.Source: §5 · p. 9, §5.1 · p. 9

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.Source: §5 · p. 9

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.Source: §5.2 · p. 9

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.Source: §5.3 · p. 9

• SWYB provides guaranteed context-free grammar compliance through distance-guided decoding.Source: §6 · p. 9
• 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.Source: §6 · p. 9
• Configurations estimated to exceed the remaining token horizon are discarded, while structurally progressive tokens receive soft promotion.Source: §6 · p. 9
• 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.Source: §6 · p. 9
• SWYB maintained competitive perplexity and decoding time, offering a favorable trade-off between guarantee and efficiency.Source: §6 · p. 9

• 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.Source: Limitations · p. 10
• The exploration budget B controls how many intermediate PDA configurations are examined.Larger B increases runtime but enables more detailed lookahead.Source: Limitations · p. 10
• For small grammars such as LTL, exhaustive exploration is feasible and incurs little overhead.Source: Limitations · p. 10
• 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.Source: Limitations · p. 10

• LLMs suggested alternative phrasings for a few sentences and generated LaTeX code for tables and formatting.Source: Ethics Statement · p. 10
• LLMs were not used for research design, analysis, or interpretation of results.Source: Ethics Statement · p. 10
• The authors reviewed and verified all generated output and assumed full responsibility for the final content.Source: Ethics Statement · p. 10

• Experiments used an Intel Xeon Silver 4416+ CPU with 20 cores, 40 threads, and 2.00/3.90 GHz frequency.Source: A System specifications · p. 11
• 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.Source: A System specifications · p. 11

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.Source: B Ablation studies · p. 11
• 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.Source: B Ablation studies · pp. 11–12
• 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.Source: B Ablation studies · p. 12

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.Source: C Budget saturation problem · p. 12

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.Source: §D.2 · p. 12, §D.3.2 · p. 13, §D.3.3 · p. 13

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.Source: §D.4 · p. 13
• 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.Source: §D.4 · p. 13

Budget study

• The budget study evaluates Max New Tokens values of 512, 1024, 2048, and 4096.These values are represented in Tables 7–10.Source: Table 7 · p. 14, Table 8 · p. 14, Table 9 · p. 14

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.Source: Table 11 · p. 14