A Quarter of Your Prover's Tokens Never Reach the Judge

The setup nobody argues about

If you train or run an LLM theorem prover against Lean, you have exactly one source of ground truth: the kernel. Everything else — the model's confidence, a reward model's opinion, your own intuition about whether simp [foo_lt] looks right — is provisional. The kernel is where correctness gets decided.

But the kernel is also deaf to certain inputs. It evaluates tactic terms, and before it can evaluate a tactic, that tactic has to parse. A generation like:

The first step is to induct on the structure of n.

is not a wrong proof. It is not a partially-right proof. It produces no information at all. It never reaches the judge. Whatever compute went into emitting those tokens — and whatever sampling budget they consumed inside an RL group — is spent outside earshot of the only oracle you have.

This suggests the wrong question and the right question. The wrong question is "does constraining decoding make the model smarter?" — of course it doesn't; masking logits changes nothing about what the model believes. The right question is: what fraction of generated tokens actually reach the kernel? Because every token that does is a token that gets back precise, machine-readable, per-step feedback — unknown identifiers with exact positions, unsolved goal states, type mismatches — and every token that doesn't is waste.

We ran a small, clean experiment to measure that fraction, and to see what a grammar constraint does to it.

What we did

• Task: given a real Mathlib theorem statement, generate one first proof step (tactic line). This is the granularity at which kernel-in-the-loop provers actually work.
• Problems: 80 statements sampled mechanically (seeded) from a fresh clone of current Mathlib (~8,900 files). No cherry-picking; the same sample validates externally — the top-20 leading-keyword share of real Mathlib tactic lines came out at 82.4%, in line with three earlier independent measurements (~83–85%), so the corpus wasn't weird.
• Models: Qwen2.5-Coder-7B-Instruct (a generalist coder) and Goedel-Prover-V2-8B (a model explicitly trained to emit Lean proofs).
• Constraint: a hand-written CFG for the Lean tactic sublanguage (53 keyword-dispatched productions plus a permissive arguments catch-all). Its construction and comprehensiveness — 99.86% structural coverage across all of Mathlib, cross-validated on Rocq and Isabelle — are the subject of the companion post; this one treats it as a given. Served through vLLM's structured-output backend backed by llguidance — genuine logit masking, not prompting.
• Scoring: every generation parsed post-hoc against the same CFG; leading keywords checked against the corpus frequency table; referenced identifiers checked against 163,731 real declaration names extracted from Mathlib + Batteries source.
• 8 samples per problem, temperature 0.8, both conditions identical except for the mask.

Result one: the constraint does its job perfectly

Three things worth noticing. First, the constraint works completely: zero invalid generations out of 640. Second, it's free — no measurable latency overhead, which surprises people who assume grammar masking is expensive. Third — and this was genuinely unexpected — diversity doesn't collapse. We feared a constrained decoder would fall into a narrow band of simp/ring boilerplate. It doesn't: essentially the same spread of distinct tactics per problem. A grammar that admits a permissive arguments slot after any recognized keyword preserves most of the model's exploration space while closing the syntax door.

Result two: hallucination didn't move — and that's the point

Roughly half of all generations cited at least one identifier that does not exist anywhere in Mathlib or Batteries — plausible-sounding fabrications like ZMod.sub_eq_add_neg or T1Space_def. The grammar constraint did nothing about this. Of course it did nothing: simp [T1Space_def] is perfectly grammatical. Whether the name between the brackets resolves is invisible to any context-free machinery.

Read this the right way, though. The constraint was never supposed to fix hallucination. It was supposed to guarantee that hallucinations become signal instead of silence. An unconstrained generation fails in two ways: sometimes semantically (name doesn't exist — but at least the kernel will tell you exactly that, with a categorized error and a token position), and sometimes syntactically (the line can't even be submitted — and then nothing tells you anything). The grammar eliminates the second failure class entirely. Every remaining error is now one the oracle knows how to talk about. That's what "coupling the generator to the verifier" means operationally: not fewer errors, but errors that are all speakable.

For training, this is the difference between a labeled example and a discarded one.

Result three: even specialists bleed half their output

Goedel-Prover-V2-8B generating in its native full-proof format gives the sharpest version of the yield story. Counting every tactic-looking line it emits across whole proofs:

Even a model trained specifically on Lean proofs wastes about half its emitted proof lines on content that cannot be evaluated — prose scaffolding, malformed steps, truncated fragments. Under a constraint, every emitted line crosses the syntactic gate by construction.

Do the training-loop arithmetic. In a GRPO-style setup sampling groups of k rollouts, the number of rollouts that can contribute gradient is p_syntax · k. At p = 0.65 you're paying for a third of your GPU-hours to hear silence. At p = 1 the same budget buys ~50% more effective rollouts — before any improvement in the model itself, at zero measured latency cost. This compounds over every step of a training run. It's the same logic as a data flywheel spinning against friction: the wheel doesn't get stronger when you remove friction, it just stops losing torque — and distance traveled is torque × revolutions.

The fine print, aka the two bugs that found us

None of this survived contact with reality without corrections, and both corrections generalize.

1. Your constraint may be silently off. Our first "constrained" runs contained markdown fences and English prose — impossible under the grammar. Cause: vLLM drops grammar enforcement for parallel-sampling requests (n > 1), and separately can silently fall back to unconstrained decoding when the backend hits a per-request error (disable_fallback=False is the default). Nothing errors; you just get unmasked tokens wearing a constrained label. The Goedel row above carries an asterisk precisely because of this — it's a partial-enforcement run, honestly degraded. If you do this yourself: request n=1, pin the backend server-side, and assert enforcement post-hoc (zero fences in constrained output is a cheap smoke test). A verifier layer that can fail toward false confidence will, given time — this is the same lesson we've hit before, now confirmed from the serving side too.

2. Permissive grammars quietly un-forbid. We deliberately left sorry out of the grammar. It showed up anyway: 2.5% of constrained generations contained it (vs 0.3% unconstrained), because the generic IDENT ARGS catch-all re-admits any keyword-shaped string as an argument — exact sorry parses fine. If you want hard guarantees ("never emit sorry"), a catch-all is a soft guarantee at best. Hardening means excluding reserved words from the ident terminal, and auditing what your fallback admits, not just what your named productions accept.

Also worth stating plainly: "reaches the kernel" here means crosses the syntactic gate — guaranteed parseable as a tactic application, hence submittable for evaluation. It is not a promise the proof succeeds, nor that our CFG's permissive argument slots match Lean's own parser exactly. And the hallucination checker is a name-table lookup with known edge cases; it's the same oracle for both arms, so the comparison stands, but individual percentages carry ±few-point uncertainty.

Where this leaves us

Grammar-constrained decoding for Lean tactics remains unpublished territory as of this writing — we could find no prior work applying token-level masking to tactic generation, which still surprises us given how little it costs and how cleanly it addresses the least interesting failure mode (syntax) in service of the most important resource (kernel contact).

The architecture this points at has three parts, each doing one job: the grammar maximizes contact between generator and oracle; the kernel converts contact into graded, per-step truth; and an interaction layer (Pantograph-style state DAG) turns each contact into step-level rewards rather than pass/fail verdicts. None of the three makes the model smarter. Together they decide how much of what the model already knows can be converted into learning signal per GPU-hour.

The next experiment is obvious and cheap: wire the same constrained decoder into a closed loop against a real kernel and measure pass@k on core-Lean goals — feedback quality, not just contact rate. But the yield result alone justifies the machinery: if you're training a prover and a quarter to half of your sampled tokens die at the parser, the cheapest capability gain available isn't a bigger model. It's making sure every token gets to speak to the judge.

Artifacts: raw generations, scoring code, the grammar, the sampled goal set, and the name table are bundled for reproduction. Stack: vLLM 0.10.2 + llguidance on a single RTX A5000; total compute ≈ 2.5 GPU-hours.

This is the companion to Lean's Tactic Language Is Smaller Than It Looks, which covers how the grammar was built and measured.

If you build on this, I'd love to hear about it — sngugi.research@gmail.com.