Provably Tractable NFA-Constrained Language Generation via HMMs

• Regex constraints can be represented by NFAs with a linear number of states, supporting applications including detoxification, function calling, and structured SQL generation.Source: §1 · p. 1
• Exact #NFA counting is #P-complete, while existing methods either distort the conditional distribution or lack polynomial-time accuracy guarantees for general constraints.HMM-based methods handle DFAs and basic constraints, but general Regex may require exponentially many DFA states.Source: §1 · p. 1
• NFA-LM distills an HMM from the base LM and adapts the #NFA FPRAS to estimate HMM completion weights for reweighting next-token probabilities.Source: §1 · p. 2

• An LM assigns sequence probabilities autoregressively, while an HMM models token sequences jointly with hidden states using initial, transition, and emission distributions.Source: §2 · p. 2
• An NFA accepts sequences through runs from an initial state to a final state, and its length-n slice contains accepted sequences of exactly length n.Source: §2 · p. 2
• For a Regex with k symbol occurrences, Glushkov’s construction yields an NFA with k + 1 states; an #NFA FPRAS runs in time polynomial in state count, length, ε^-1, and log(δ^-1).Source: §2 · p. 2
• Constrained generation reweights each LM next-token probability by an HMM estimate of constraint completion, and the paper states that the resulting distribution is provably close to its approximate version.Source: §2 · p. 2

• Unrolling an NFA for length n creates a layered DAG whose accepted language equals the original automaton’s length-n slice.Source: §3 · pp. 2–3
• A fixed state order selects a canonical successor for each accepted suffix, assigning it one run even when the NFA admits multiple accepting runs.Source: §3 · p. 3
• The convergence state of two canonical runs is the state reached by their longest common suffix, a construct used to characterize their shared suffix structure.Source: §3 · p. 3
• Pairing unrolled NFA states with HMM hidden states gives product states whose suffix-atom weights sum to HMM completion probabilities; canonical product runs control dependence among reused samples.Source: §3 · pp. 3–4

4 Method

• The overall pipeline distills an HMM from base-LM responses, precomputes reusable suffix information, and then generates constrained outputs.Source: §4 · p. 4

4.1 Precomputation

• Precomputation expands weighted suffix samples and uses a canonical union to avoid counting the same atom through multiple NFA successors.The resulting sample-size estimate is unbiased; median-of-means and capped core repetitions support concentration and bounded precomputation.Source: §4.1 · p. 5

4.2 Constrained Generation

• At each generation step, NFA-LM estimates HMM constraint-completion probabilities for candidate tokens and samples proportionally to their LM probabilities times those estimates.Source: §4.2 · p. 5

5 Theoretical Guarantees

• Each core repetition can fail through excessive approximation error or sample overflow; an outer median across independent repetitions makes overall failure probability arbitrarily small.Overflow would violate the time-complexity guarantee without the cap.Source: §5 · p. 6
• For each j ∈ [nu], the probability of Aj is at most 1/16, and the probability of Bj ∩ (Aj)c is at most 1/16.Source: §5 · p. 6
• For each prefix, ξ_j is the relative error in the HMM completion score, while Δ_j accumulates weighted squared error; I_j tracks whether the repetition stays within its error budget given C_j.The probability that I_j fails is at most 3/16.Source: §5 · p. 6
• Theorem 1 gives a simultaneous guarantee across all generation steps for sequences with positive HMM probability.The supplied statement does not include the bound itself.Source: §5 · p. 6
• Theorem 2 bounds total variation distance under the condition that Γ(x1:ℓ−1) is positive whenever the constrained prefix has positive probability.The supplied statement does not include the bound itself.Source: §5 · p. 6
• Theorem 3 states a time-complexity guarantee for Algorithm 1 in terms of NFA size, maximum length, HMM size, alphabet size, and ε and δ.The supplied statement omits the complexity expression.Source: §5 · p. 6

6 Evaluation

• Evaluation uses 500 CommonGen instances, Regex families with up to 20 tracked keywords, sequences of 1–64 tokens, and (ε, δ)=(0.1, 0.1).CommonGen instances provide three to five key concepts to incorporate into the generated sequence.Source: §6 · pp. 6–7

6.1 RQ1: Scalability

• 500/500 instances: NFA-LM satisfies every constraint, averaging 28.5 seconds with Gemma-4-E2B; Ctrl-G succeeds on fewer than half.LLM-only baselines are faster but satisfy only 38.0–61.2% of constraints.Source: Table 2 · p. 7, §6.1 · p. 7

6.3 RQ3: Generation Quality

• NFA-LM substantially exceeds XGrammar in average quality, while Ctrl-G scores slightly higher than NFA-LM on their respective successful subsets.The reported CommonGen example scores 3.0 for NFA-LM and 1.5 for XGrammar; XGrammar repeats “end” 46 times.Source: Table 2 · p. 7, §6.3 · p. 8

6.2 RQ2: Approximation Accuracy

• 0.00315: the worst observed maximum relative error, below ε=0.1 for all 232 exact-computable Gemma-4-E2B instances.Exact brute-force computation completed within the timeout for 232 of 500 instances.Source: §6.2 · pp. 7–8, Figure 3 · p. 8

• NFA-LM adapts the #NFA FPRAS to estimate HMM-weighted accepting completions and guide LM generation with theoretical guarantees.The conclusion characterizes it as a polynomial-time approach that generates high-quality outputs with provably bounded approximation error for NFA constraints at scale.Source: §7 · p. 8

Limitations

• NFA-LM handles Regex constraints represented by NFAs, while context-free languages and Regex backreferences remain challenges; the best-known #CFG FPRAS runtime remains impractical.The work is motivated by the efficient #NFA FPRAS (Meel and de Colnet, 2025).Source: Limitations · p. 9
• The guarantees bound weighted-#NFA approximation error relative to exact HMM-guided decoding, but do not bound the HMM-to-LM completion-probability approximation.Future work includes extending guarantees to context-free constraints and reducing or eliminating reliance on the HMM.Source: Limitations · p. 9

A Cached Membership

• Incremental per-layer caching reduces canonical-union membership checks from O(|Qu|) time to constant time with respect to |Qu|.The implementation uses two Boolean matrices for each layer and independent repetition.Source: A Cached Membership · p. 11

B.1 Canonical Product Runs

• Canonical product runs map each atom to a unique accepting run, and convergence states mark where two runs begin sharing the same suffix through the terminal state.The definition supports grouping atoms by their convergence state.Source: §B.1 · p. 12

B.3 Correctness

• With probability at least 1−δ, Theorem 1 guarantees relative-error ε estimates of HMM completion probabilities simultaneously for all prefixes, when the sequence has positive HMM probability.The estimate is formed as the median of repetition-level estimates.Source: §B.3 · pp. 14–15

B.4 Oracle-Corrected Auxiliary Process

• The oracle correction keeps productive-state probabilities within (1 ± κ)W(q, b)^−1, preserves legal reductions, and supports a coupling of three executions on Cj.The coupling ensures the budgeted execution does not fail and that all three executions have the same stored samples and rates on Cj.Source: §B.4 · pp. 17–18

B.4.1 Probabilistic Environment

• The probabilistic-environment analysis formalizes the sampling invariant and shows that normalized atom variables have expectation one in both Nj and N∗,j.The invariant is stated in the supplied passage as an intuitive explanation, while Lemma 12 provides the expectation-one result.Source: §B.4.1 · pp. 19, 21

B.4.2 Proof of Lemma 1

• The parameter choice for the number of samples bounds the probability that a block mean falls outside the target interval.The deviation threshold is κW/(1 + κ), with η = κ/(1 + κ).Source: §B.4.2 · p. 22
• The proof bounds the median block estimate by showing that a deviation requires at least half the blocks to deviate, then applying probability bounds.The argument uses Lemma 11, Markov’s inequality, and Fact 3.Source: §B.4.2 · p. 22
• A median estimate inside the inverse interval, combined with the lower bound on ρ, places the tentative value inside (1 ± κ)W(v)^−1.The tentative value is the minimum of ρj(v) and the inverse median estimate.Source: §B.4.2 · p. 22
• The resulting bound uses |V| ≤ h|Qu| to complete the proof of Lemma 1.Source: §B.4.2 · p. 22

B.4.3 Proof of Lemma 2

• The argument uses a unit-expectation proposition as the basis for bounding the number of samples.Source: §B.4.3 · p. 22
• When the event Aj does not occur, the proof establishes a bound for every productive state.Source: §B.4.3 · p. 22
• Summing sample sets across layers, hidden states, and sample indices, then applying Markov’s inequality, yields the sample-count bound.Source: §B.4.3 · p. 22
• These steps complete the proof of Lemma 2.Source: §B.4.3 · p. 22

B.4.4 Proof of Lemma 3

• For n = 1, the error term is zero; for n ≥ 2, the proof defines an oracle-corrected relative error for each supported prefix.Source: §B.4.4 · p. 22
• For positive-weight hidden states, the oracle-corrected estimate is bounded using the state estimate and the relation WR(b) ≥ W(q, b).Source: §B.4.4 · p. 23
• The proof combines block means, Jensen’s inequality, finite sums, and linearity of expectation to bound the accumulated error.Source: §B.4.4 · p. 23
• On Cj, the budgeted and oracle-corrected estimates agree for ℓ ∈ [n − 1], yielding the stated conclusion for Lemma 3.The proof notes that the terminal contribution to ∆j is zero.Source: §B.4.4 · p. 23

B.4.5 Proof of Lemma 4

• The proof of Lemma 4 bounds deviations of block means from WR(b) using Lemma 11, Markov’s inequality, Fact 3, and the parameter choices.Source: §B.4.5 · p. 24
• On Cj, Lemma 7 makes the ordinary and oracle-corrected estimates agree simultaneously across ℓ ∈ [n − 1], proving Lemma 4.Source: §B.4.5 · p. 24

B.4.6 Proof of Lemma 11

• For identical atoms, the corrected-pair term preserves mass WR(b) throughout the run.The correction for z1 = z2 is defined to preserve this mass at every layer.Source: §B.4.6 · p. 26
• The proof transports corrected and centered terms across blocks using conditional independence, then bounds the remaining terminal expression to establish the claim for compute.The final combination of bounds proves the remaining claim for compute in Lemma 11.Source: §B.4.6 · pp. 25, 27, 28
• Replacing a common tail may change first(R, x), but the resulting atom still has an accepting run from a state in R and remains in the union Z+(R(b)).This supports the injection argument used to bound the terminal expression.Source: §B.4.6 · p. 27
• Grouping unequal atoms by their canonical runs’ convergence states yields at most n − ℓ + 1 classes, which bounds the terminal contribution.The proof combines this class count with the bound on each grouped contribution.Source: §B.4.6 · p. 28

C Time Complexity

• Canonical unions dominate the other operations, determining the cost of one outer precomputation repetition.The analysis accounts for cache computations, reductions, block means and medians, and canonical unions.Source: C Time Complexity · p. 28

D Constraint Satisfaction

• Every returned length-n sequence satisfies the NFA constraint when the next-token distribution has a positive normalizing constant at every step.The guarantee does not depend on the accuracy of the completion-probability estimates.Source: D Constraint Satisfaction · p. 29

E Prompt Templates

• The LM baseline prompt states the Regex constraint and length bounds, while constrained-generation methods receive the constraint through the engine interface rather than the prompt.Both prompts ask for natural, coherent outputs using supplied concepts.Source: E Prompt Templates · p. 30