Adaptable Logical Control for Large Language Models

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

purpose and architecture

Ctrl-G controls an autoregressive LLM with logical constraints through a white-box Hidden Markov Model (HMM) and a deterministic finite automaton (DFA). The paper’s three steps are distillation, constraint specification, and inference: “we distill a Hidden Markov Model as its white-box approximation; (2) constraint specification: we construct a deterministic finite automaton (DFA) to (compactly) represent the desired logical constraint; (3) inference: we condition the HMM on the DFA-specified constraint and compute this conditional probability to guide LLM generation towards satisfying the constraint.” (Section 1, p. 2). The paper lists as an advantage that “the desired logical constraints are guaranteed to be satisfied [47]” (Section 1, p. 2); the guarantee is attributed to the earlier GeLaTo work, and the paper gives no separate proof of it. Inference: this separates a trusted constraint checker from probabilistic code generation; a Verus implementation could specify DFA transition and acceptance as spec fns and prove that every emitted bounded sequence is accepted, while treating the HMM/LLM scores as an explicitly trusted heuristic.

technique: HMM distillation and guided sampling

What it is: train an HMM on unconditional LLM samples to approximate the LLM joint distribution. The HMM has hidden states, emissions, and transitions; its Markov property permits dynamic programming (Section 2, p. 3). At each token, Ctrl-G samples proportional to the LLM next-token probability times the HMM’s estimated probability that the constraint will be satisfied given that token and the prefix. The paper gives the exact rule: “pctrl-g (xt | x<t , α) ∝ plm (xt | x<t ) · phmm (α | xt , x<t )” (Eq. 1, Section 3, p. 4).

How done: (1) sample sequences unconditionally from the frozen LLM and train the HMM to minimize KL divergence (Section 3, p. 4; the paper defers the distillation procedure to GeLaTo [47]); (2) assume sequences are bounded by a length n (Section 2, p. 2); (3) before generation, precompute the table p(S_n in F | z_t, s_t) for every position t, HMM state z_t, and DFA state s_t with the backward recurrence of Eq. 4; (4) at each step t, compute the HMM forward probabilities for the prefix and combine them with that table (Eq. 3) to get the acceptance probability of each candidate token; (5) sample the token proportional to the LLM probability times that acceptance probability; (6) update the DFA state. Algorithm 1 specifies these loops (Section 3.2, p. 5). The recurrence sums over next HMM states, DFA successor states, and tokens on the edge between the two DFA states. Theorem 3.2 gives O(nmh²) time for sampling n tokens, with m DFA edges and h HMM hidden states. Inference: Verus can prove recurrence soundness and DFA-state updates, but probability normalization and neural logits require a real-number or trusted numerical model absent from ordinary integer verification.

technique: DFA representation and composition

A DFA is a tuple (Q, Σ, δ, q0, F): finite state set, token alphabet, transition function, initial state, accept states (Definition 3.1, p. 4). A DFA that checks that a string of n tokens appears can be built with size O(n) by adapting the Knuth–Morris–Pratt (KMP) algorithm. Constraints compose by intersection (and), union (or), complement (negation), and concatenation. The authors state: “For many common families of logical constraints, we can efficiently construct their DFA representations by leveraging existing algorithms.” (Section 3.1, p. 4). Inference: in Verus, define a finite enum state and a total transition spec fn; prove that acceptance is equivalent to the intended predicate by induction over the token sequence. Composition proofs should preserve each component’s invariant and need no probabilistic assumptions.

The paper’s CommonGen construction tokenizes each keyword’s inflections, uses Aho–Corasick to recognize any inflection, then intersects one DFA per keyword (Section 4.1, p. 6). For ordered text infilling, it builds one DFA per unmasked text fragment with KMP and concatenates them. In general, concatenating two DFAs “could result in exponentially many states”, so the paper identifies a special case (Proposition 4.1): if every accept state of the first DFA transitions only to a dead state, the accept states can be merged with the initial state of the second DFA (Section 4.2, p. 7). Because the benchmark also provides the granularity of each mask, additional DFAs enforce, for example, exactly one word between two fragments (Section 4.2, p. 7). For interactive editing, a word-length constraint is a DFA composed with the keyphrase DFAs by logical and (Fig. 2, p. 2; Section 5.1, p. 8). Inference: these are concrete reusable algorithms, not suggestions to prompt an LLM.

technique: probabilistic versus pure logical control

Regex and DFA filtering (the paper’s “guidance” example) only discards next tokens that would make the constraint unsatisfiable and leaves the probabilities of the other tokens unchanged. Ctrl-G instead estimates how likely each next token is to lead to the constraint being satisfied. The paper illustrates, for a sentence that must end with “ in the park”, that guidance produces an unrelated text with the phrase appended, whereas Ctrl-G produces a coherent sentence (Section 3.3, p. 5). It also states that setting phmm(α | xt, x<t) = 1 for all non-zero values degenerates Ctrl-G to pure logical reasoning. Inference: for a verified pipeline the proof obligation would remain the DFA acceptance theorem, not fluency or HMM approximation quality.

evidence and measured limits

On GPT2-large CommonGen, Ctrl-G achieved test constraint satisfaction 100.0% and BLEU-4 31.5, ROUGE-L 44.8, CIDEr 16.2, and SPICE 31.2 (Table 1, p. 6; the benchmark test set, with no count stated in the table). The same HMM had 32768 hidden states. Text infilling used GPT2-small and reported BLEU-4 85.4, 77.5, 66.5, 57.2 at 13%, 21%, 32%, 40% masking, respectively, against ROUGE-L 90.6, 85.2, 77.0, 69.8 (Table 2, p. 8; each is a benchmark test set; the supervised ILM baseline’s means and standard deviations are over 10 sampled runs). Ctrl-G was below ILM on ROUGE-L at 13% masking (90.6 vs 90.9).

Interactive editing used 800 test examples: eight settings (insertion vs continuation, keyphrase or not, word length or not) with 100 examples each, using TULU2-7B plus a 32768-state HMM (Section 5.1, p. 8). For generation, Ctrl-G sampled 128 outputs at temperature 0.7 and kept the one with the highest base-model likelihood; the baselines also generated 128 samples and kept the highest-probability one (Section 5.1, pp. 8–9). Ctrl-G had 100% constraint success in every constrained continuation and insertion setting. Its overall satisfaction (constraint met and quality score above 3) averaged 92% for continuation and 79% for insertion (Table 3, p. 9; each percentage denominator is 100 examples per setting, with three annotators per example who rated only fluency and coherence and were not told the constraints). GPT4’s best constraint success rate in continuation was 59% and its averages were 57% (continuation) and 36% (insertion). Annotator agreement (Kendall’s coefficient of concordance) averaged 0.449, which the paper calls moderate (Appendix B, p. 16).

Runtime was measured on an NVIDIA A100 80GB with TULU2-7B and, in the paper’s words, a “current naive implementation” (Section 5.3, p. 10). Per-token time scaled roughly linearly with DFA size at fixed maximum sequence length. At a fixed DFA of size about 900, the extra Ctrl-G cost stayed constant as the maximum sequence length grew, while the base model’s per-token time grew linearly with it, so the base model dominates for long sequences (Section 5.3, p. 10). In a GSM proof of concept, for 293 of 1,319 test examples TULU2-7B did not use all numbers given in the problem statement; accuracy on those 293 was 14.6% versus 34.6% on the full test set. With Ctrl-G encouraging use of the numbers, 16 sampled outputs and a majority vote, accuracy on those 293 was 28.3%, “3.4% higher than the accuracy without Ctrl-G” (Section 6, pp. 10–11; the paper does not say whether this is percentage points or relative, nor give the baseline’s sampling setup). The paper does not claim formal correctness of generated reasoning.

trusted boundary and relevance to Verus

The paper assumes sequences are bounded by some n (Section 2, p. 2) and relies on the HMM approximating the LLM; it notes it was unclear whether this approximation holds for larger LLMs and claims strong positive answers (Section 2, p. 3). The rest of this section is inference. The LLM, distilled HMM, tokenization, floating-point probabilities, and sampling randomness remain trusted or empirical. DFA construction and acceptance are the cleanest formal-verification target. Generated Rust could use a verified DFA monitor to reject or halt before unsafe output, while Verus proves bounded transition/acceptance properties and leaves model quality and distribution matching outside the theorem. The paper’s 100% constraint rates show enforcement in the tested settings, not arbitrary-length guarantees. Agent-written verified Rust therefore faces threat from incorrect DFA compilation, tokenizer mismatch, and unchecked numerical code. VL should reuse KMP/Aho–Corasick and DFA composition rather than redo them, and should report denominators and exact constraint predicates.

techniques for the catalog

• HMM distillation — fit a tractable Markov model to LLM samples and use it for future-constraint probabilities
• DFA constraint compilation — compile token predicates with KMP, Aho–Corasick, and finite-state composition
• dynamic-programming guided decoding — combine LLM next-token scores with HMM/DFA acceptance probabilities in O(nmh²)
• DFA concatenation for infilling — merge ordered fragment automata and add granularity (length) automata
• verified constraint monitor (Inference, not in the paper) — prove transition and acceptance properties while treating neural fluency as empirical Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Note that the performance gap between Ctrl-G and ILM improves almost monotonically as the masking ratio increases, illustrating the strong generalizability of Ctrl-G.”): read the paper text from first line to last; checked every quotation, number in Tables 1-3, section and page reference, the Eq. 1/3/4 and Algorithm 1 steps, Theorem 3.2, Proposition 4.1, the runtime and GSM claims, and the arXiv link (id 2406.13892v2 appears in the paper text); changed the step order (the backward table is precomputed before generation), the tables’ page references, “800 stories” to 800 test examples, the GSM wording (the model did not use all numbers; “3.4%” is not stated as points), the quotation punctuation of Eq. 1, the infilling and length-DFA description, and added the sampling/reranking setup, annotator agreement and ROUGE-L exception; marked own conclusions as Inference. Not checked: the cited prior work (GeLaTo, ILM, etc.), the appendix figures, the GitHub code, and how constraint success was measured (the paper does not say).

Last edited: 2026-10-17