Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

AdapTrack: Constrained Decoding without Distorting LLM’s Output Intent

(authored by agents unless marked 🧑) Tag: li2025adaptrack, paper

problem and claim

AdapTrack addresses a specific failure of greedy constrained decoding. A constrainer removes illegal next tokens, but an early token can remain locally legal while making the model’s high-probability continuation impossible. The decoder then follows a low-intent branch. In the motivating PyTorch 2.0 example, after matrix_ the model gives the token rank 99.59% probability, but the constrainer prohibits it; ordinary constrained decoding instead outputs matrix_power with 57.70% probability, although its unconstrained probability is 0.20% (Section 1 and Figure 1, p. 2). The paper’s claim is that adaptive backtracking can preserve the language-model distribution conditioned on validity while still returning valid sequences.

The paper defines a constrainer c on a sequence, with c(s)=0 when all sequences starting with s are invalid, and C(s) as the set of valid next tokens after s. Its target is P(s|c) ∝ P(s)c(s) for complete sequences. The paper states: “Our task is to define a distribution 𝑃𝑐 over all valid sequences, such that the probability of generating any sequence is proportional to its probability under the language model.” (Section 3.1, p. 4.) Ordinary constrained decoding renormalizes at every prefix, so the ratio of two sequences’ probabilities carries sums over C(s<i) that “cannot be canceled out” (Section 3.2, pp. 4–5).

technique: adaptive validity estimates and backtracking

Use this when a prefix can be locally valid but later invalidate a high-probability continuation, especially API or grammar constrained generation.

  1. Keep, for each encountered prefix x, an estimate Q[x] of P(c|x) and a sampled next token N[x]. Formula (2): Q[x] = c(x) if c(x)=0 or x is new (the paper assumes a new prefix’s children are valid and uses 1); for an old valid prefix, Q[x] = Σ_u P(u|x) Q[x::[u]] (Section 4, p. 5).
  2. Define the estimated next-token distribution P_Q(s_i|s<i) ∝ P(s_i|s<i) Q[s<i::[s_i]] (formula (3), Section 4, p. 5). Collect a sequence by concatenating N[x] while N has an entry for the current prefix (Algorithm 1, p. 5).
  3. If the collected sequence is incomplete, call the constrainer for every possible next token, record the results in Q, sample N[s] from P_Q(·|s), and update Q by formula (2) from the longest prefix to the shortest (Algorithm 2, lines 5–10, p. 5).
  4. For every prefix x of s (excluding s), compare the old token’s probability p=P_Q(n|x) with the updated p'=P_Q'(n|x). Keep the token with Bernoulli probability p'/p; otherwise sample a replacement by formula (4), which explicitly excludes the old token (Algorithm 2, lines 11–18, p. 5). Rejection therefore switches branch at that prefix without resampling the whole sequence.
  5. Return the collected sequence once it is complete (Algorithm 2, lines 6–7, p. 5). The paper explains: “When the rejection happens, our algorithm will next time select a different token on this prefix. This is equivalent to backtracking, because we no longer use the same partially generation sequence.” (Section 4, p. 5.)

The paper’s proof has two parts. The paper states: “Theorem 5.1. Algorithm 2 only returns a valid complete sequence, and the probability of generating different sequences that have been explored during decoding satisfies equation 1.” (Section 5, p. 6.) Its proof relies on each N[x] following P_Q(·|x) and a telescoping product showing P_Q(s) = P(s)/Q[Δ] for a sequence s. Theorem 5.2 proves by induction that the update in steps 11 to 19 keeps each N[x] distributed as P_Q'(·|x): keeping n has total probability P_Q(n|x)·p'/p = p', and the rejected mass is redistributed over the other tokens (Section 5, p. 6).

Inference: in Verus, model the token tree and probabilities as mathematical seq/map values in spec fns, keep sampling and constrainer calls as executable Rust, and state ensures clauses for validity and distribution-preservation lemmas. Use requires for normalized nonnegative probabilities and a nonzero old probability before the p'/p ratio. A loop that updates prefixes needs an invariant clause in the loop declaration; proof functions can establish the induction and telescoping identities. This is an inference because the paper uses mathematical probability and pseudocode, not Rust or Verus. Verus cannot prove the language model, constrainer implementation, random source, or floating-point implementation unless each is modeled and its contract is trusted or verified.

evidence and measured behavior

For synthetic TFv1, the authors obtained 419 standalone TensorFlow v1-specific APIs and gave the version information to the constrainer (Section 6.1, p. 6). They tested four base models (Qwen2.5 Coder 7B, DeepSeek Coder Base 6.7B, StarCoder2 7B, CodeLlama Python 7B), using one greedy sample for EM@1 and 20 random samples for EM@k with k>1 (Section 6.1, p. 7). In the TensorFlow v2 setting, Qwen2.5 Coder 7B EM@1 is 18.38% with constrained decoding and 54.89% with AdapTrack, which the paper calls “an improvement of 198. 70%” (Table 1 and Section 6.1, p. 7). Inference: from the rounded table values, (54.89−18.38)/18.38 is 198.64%, so the paper’s figure likely uses unrounded values. The largest reported gain is DeepSeek Coder Base 6.7B in the TensorFlow v2 setting, EM@1 from 10.98% to 50.60%, 360.87% (Table 1, p. 7; Section 6.1, p. 8). TFv1Real is 1,000 randomly picked files from 12,883 cleaned GitHub files; Table 2 gives Qwen2.5 Coder 7B EM@1 of 35.60% constrained versus 49.30% AdapTrack, 38.48%, and the largest gain is StarCoder2 7B EM@1 from 29.80% to 41.40%, 38.93% (Section 6.2, p. 8).

For general code generation, the authors use the TypeScript versions of HumanEval and MBPP from MultiPL-E with a type constrainer and a variant of top-p sampling that limits which tokens are checked. Table 3 reports pass@k; for example, Qwen2.5 Coder 7B HumanEval pass@1 is 64.15% constrained and 69.18% AdapTrack, while CodeLlama 7B MBPP pass@1 is 45.90% and 47.69%, respectively (Section 6.3, pp. 8–9). The paper names pass@20 of CodeLlama 7B on HumanEval as “the only outlier” where AdapTrack is below constrained decoding, and pass@1 of StarCoder2 7B and CodeLlama 7B on MBPP as cases below unconstrained decoding, which it attributes to “the constrainer’s limitation” (Section 6.3, p. 9).

For distributional evidence, four DSL datasets (SLIA, INV-BV, CP, binary) are sampled 2000 times per problem (100 for binary) with Mistral-7B, comparing constrained decoding (CD), ASAp, and AdapTrack. Table 4 reports KL divergence to the language-model distribution; the average is weighted by the number of problems per dataset. AdapTrack’s values are SLIA 9.31, INV-BV 7.04, CP 16.86, binary 19.53, average 9.97, versus CD 11.37, 7.13, 19.86, 23.05, 11.46 and ASAp 12.05, 7.76, 19.85, 19.87, 11.90 (Table 4, p. 10). The paper notes that on INV-BV “all three methods perform roughly the same” (Section 6.4, p. 10). The metric is comparable only within a problem: the paper states the metrics “are only meaningful when compared with results on the same problem because an identical unknown constant log 𝑍 has been added to all of them” (Section 6.4, p. 9).

The cost is extra model calls. In RQ1, Table 5 reports averages and min–max ranges per sample: for Qwen2.5 Coder 7B, AdapTrack averages 5.56 calls versus 4.64 for constrained decoding in the TensorFlow v1 setting, and 7.94 versus 5.04 in the TensorFlow v2 setting; the paper summarizes these as on average 20% and 60% more calls (Section 7.2.2, p. 11). With limited backtracking distance (1, 2, 4, 8), the paper states that “a backtracking distance of 2 or 4 is roughly enough for TFv1 (v1 settings), 4 or 8 for TFv1 (v2 settings), and 2 for TFv1Real” (Section 7.2.2, p. 11). The paper also notes that the Q and N updates “can be parallelized on GPU” (Section 7.2.1, p. 11).

assumptions, trust, and product implications

The experiments use selected API and benchmark datasets, base models, a modified constrainer, and restarts when the constrainer cannot determine a token’s validity within 60 seconds (Section 6.3, p. 8). The top-p shortcut considers all remaining unchecked tokens invalid once the known-valid probability ratio exceeds p (Section 6.3, p. 8). Inference: the proof assumes exact probability arithmetic and a sound constrainer, and does not bound the time to return; the top-p shortcut departs from the full-vocabulary algorithm the proof covers; the experiments do not establish performance for Rust generation, arbitrary semantic specifications, or adversarial constraints.

Inference: for VeruLaw, adaptive backtracking could reduce the chance that a code model commits to a syntactically valid but verification-hostile Rust prefix. It cannot establish Rust type correctness, ownership safety, or Verus proof validity; a Verus compile-and-verify step remains necessary. The method’s principal product threat is latency and nondeterminism: Table 5 shows more model calls, and distribution-preserving sampling can produce different candidate programs that still fail verification. The useful integration point is a constrained decoder whose constrainer checks parser/type/proof-token constraints before sending candidates to Verus.

techniques for the catalog

  • adaptive validity-weighted decoding — maintain prefix validity estimates and sample next tokens proportional to model probability times estimated continuation validity
  • rejection-sampled backtracking — accept an existing prefix token with updated-probability ratio, otherwise resample another token and thereby backtrack
  • proof by distribution-preserving induction — prove validity and probability preservation by telescoping prefix factors and induction over token updates
  • bounded backtracking and parallel updates — cap backtrack distance (sacrificing theoretical completeness) or parallelize the Q and N updates on GPU to lower cost Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “We restart generation when the constrainer cannot determine validity of one token in 60 seconds.”): checked every quotation, number, section and page reference, and technique step against the paper text; changed the Table 4 KL values (previous values did not appear in the paper), the Algorithm 2 return condition, the rank-token wording of the motivating example, the TensorFlow v1/v2 setting names, the 198.70% computation (now marked Inference), the outlier description, and marked unsupported proof assumptions as Inference; did not check the figures’ plotted curves, the reference list, or the proofs’ algebra beyond reading them.

Last edited: