Arnav Dandu

Info | Research | Other

UMass

I’m currently working with ASTRAL: Automated Synthetic Theorem-Proving by Reasonining with Language Models, a team funded by DARPA’s expMath program.

More information will be added Soon™

UCSD

Formal Verification of Grammar-Constrained Decoding

A Lean 4 formalization of the paper Flexible and Efficient Grammar-Constrained Decoding. This project proves correctness of a grammar-constrained decoding algorithm that composes a detokenizing lexer FST with a pushdown parser to compute valid next-token masks during LLM inference.

Grammar-constrained decoding ensures that language model outputs conform to a given formal grammar (e.g., JSON, SQL, code). The core algorithm works by:

1. Lexing — An FST maps token sequences to character sequences, handling the mismatch between an LLM’s token vocabulary and the grammar’s character-level rules.
2. Parsing — A pushdown automaton (PDA) checks whether character sequences belong to the target language.
3. Composition — The lexer FST and parser are composed so that, at each decoding step, the system can determine which tokens lead to strings still accepted by the grammar.

This formalization verifies that the composed system correctly computes the set of valid next tokens, establishing both soundness (every token in the mask extends to a valid parse) and completeness (no valid token is excluded).

Formalization Structure

Key Theorems

• Step-level soundness (Soundness) — If a token’s mask bit is true, then there exists a continuation where the composed FST+parser accepts. (Paper Theorem C.4)
• Step-level completeness (Completeness, EOSCompleteness) — If a viable continuation exists through the composed system, the token’s mask bit is true. (Paper Theorem C.5)
• accept_if_ComputedValidTokenMask — Tokens in the computed mask extend to valid FST runs through the parser.
• mem_ComputeValidTokenMask_preprocess_iff — Semantic characterization of the valid-token mask: a token is in the mask iff it is realizable and the resulting output is accepted by the parser from the current state.
• computeSingleProducible_correct — The executable DFS for singleton-producible outputs matches the semantic specification.
• Cumulative checker correctness (GCDChecker_sound, GCDChecker_complete) — The step-level theorems lift to the full token-sequence checker interface, establishing that the checker’s accepted language equals the target grammar-constrained language. These take two explicit assumptions as hypotheses (see Assumptions).

Building

Requires Lean 4 (toolchain leanprover/lean4:v4.29.0-rc6).

# Download prebuilt mathlib oleans (recommended before first build)
lake exe cache get

# Build the full project
lake build

Dependency Visualizer

An interactive declaration dependency graph is available at:

ucsd-formal.github.io/constrained-decoding-formalization

To run locally:

./lean-dep-viz serve          # Serve at localhost:3000
./lean-dep-viz build --output-dir site  # Generate static site

Paper-to-Formalization Reference

This table maps definitions, algorithms, and theorems from the paper to their Lean 4 counterparts.

Structures and Definitions

Algorithms

Propositions and Theorems

Type Parameters

Throughout the codebase, these type variables recur:

Most require FinEnum, DecidableEq, or BEq/LawfulBEq instances.

Assumptions

The formalization relies on four explicit assumptions. The first two are hypotheses on the lexer specification used by the step-level completeness proofs. The latter two are hypotheses on the cumulative checker theorems that lift step-level results to full token sequences.

Lexer assumptions

These are properties of the lexer automaton that hold for all practical lexer specifications. They are required by the step-level completeness proofs (Completeness, EOSCompleteness).

Non-empty-string lexing (hempty). The lexer automaton’s start state is not an accepting state—i.e., the empty string is not a valid token.

A.start ∉ A.accept

Lexer restartability (hrestart). Every accepting state of the character automaton has at least one character that does not extend the current lexeme but can start a new lexeme from the start state:

∀ s ∈ A.accept, ∃ c, A.step s c = none ∧ (A.step A.start c).isSome

This is needed because the lexing FST has two emission patterns: a single-symbol [char t] (when completing a token and restarting) and a two-symbol [char t, eos] (when completing at end-of-stream). The completeness argument requires that the head of any nonempty output is singleton-producible—i.e., there exists an input that produces exactly that one symbol. For the EOS case, the two-symbol emission [char t, eos] cannot directly witness singleton producibility, so we need the restart path to produce just [char t]. The hrestart hypothesis guarantees such a restart character exists.

Both hempty and hrestart are trivially satisfied by standard lexers for programming languages, JSON, etc.: the empty string is never a valid token, and different token types (identifiers, operators, literals) use disjoint character classes so every accepting state has characters that cannot extend it but can start a new token.

Cumulative checker assumptions

The cumulative checker theorems (GCDChecker_sound, GCDChecker_complete) connect the step-level soundness and completeness results to the full checkerAllows/checkerAccepts interface over token sequences. They take two additional hypotheses:

Productivity (checkerAllowsTermination). Every token prefix that the checker incrementally allows can be extended to a complete accepted sequence:

∀ w, checkerAllows c w → ∃ w', checkerAccepts c w' ∧ w.isPrefixOf w'

This is a liveness property of the composed FST+parser system: from any reachable viable state, there exists a path to acceptance. It cannot be proved from the algorithm alone—it depends on the grammar being productive (no infinite derivations or dead-end nonterminals from reachable states). The paper assumes this implicitly. In practice, any well-formed context-free grammar used for constrained decoding (JSON schemas, SQL grammars, etc.) satisfies this property.

Path independence (checkerPathIndependent). The checker’s incremental decisions depend only on the flattened character content of the token prefix, not on the particular tokenization:

∀ w₁ w₂, w₁.flatMap flatten = w₂.flatMap flatten → checkerAllows c w₁ = checkerAllows c w₂

We prove that each individual mask check depends only on the FST state, which in turn depends only on the character content (MaskChecker_eq_of_eval_eq + BuildDetokLexer_eval_flatMap_eq). However, lifting this to the full conjunction checkerAllows is harder: different tokenizations of the same string create checker calls at different character boundaries, so the proof requires showing consistency across retokenization. This is a property of the tokenizer vocabulary rather than the constrained decoding algorithm itself, and is left as an explicit hypothesis. In practice, this holds because LLM tokenizers use deterministic tokenization (e.g., BPE), so each character string has a unique tokenization.

License

This project is licensed under the Apache License 2.0. See LICENSE for details.