Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

AI summary

Overview

Research area: AI for mathematics — specifically statement autoformalization, the task of translating informal mathematical statements written in natural language into formal Lean 4 declarations. The paper sits at the intersection of formal verification, LLM evaluation, and mathematical benchmark design.

Technical level: Advanced. It assumes familiarity with Lean 4 / Mathlib, LLM-as-judge evaluation paradigms, factorial experimental design, and statistical measures such as Wilson confidence intervals, Cohen's κ, and McNemar tests.

Scope (one sentence): The paper measures how much Lean compilation overstates true semantic faithfulness in natural-language-to-Lean statement translation across eight systems on a 227-statement benchmark, validates a reference-free LLM-judge criterion against blinded human review, and decomposes each system's compile–acceptance gap into real translation errors versus judge errors and defective source statements.

What This Paper Is About

When a language model translates a natural-language theorem into Lean 4, the compiler only checks that the resulting declaration is well typed — not that it says what the original statement meant. A model can silently drop a hypothesis, change a domain, or weaken a conclusion and still produce code that compiles cleanly. Because these benchmark statements come from LaTeX textbooks with no canonical Lean target, exact-match and reference-based scoring are unavailable, so the paper asks: how large is the gap between "it compiles" and "it faithfully states the theorem," and how much of that gap is actually the system's fault?

Key Contributions

1. A validated reference-free acceptance criterion. An output is accepted only if it compiles in Lean 4 with Mathlib and two LLM judges from different model families (GPT-5.2 and Gemini-2.5-Pro) both assign a faithfulness grade of at least 9 out of 10. The authors audit this criterion against blinded human reviewers on both sides of its decision boundary, compare it same-sample against the public LeanScorer rule, test a third-family judge (Claude Sonnet 5), sweep the grade threshold from 7 to 10, and add a formal BEq cross-check.

2. A 227-statement benchmark with no canonical Lean targets. University-level statements drawn from four open-source LaTeX textbooks: Lebl's Basic Analysis (Real Analysis, 48 statements), Lebl's Guide to Cultivating Complex Analysis (19), McKay's Notes on Topology (63), and Doty's Abstract Algebra (97). Source imprecisions are preserved as written, and 18 statements that are false as written or lost context during extraction are flagged in the release.

3. A decomposition of the compile–faithfulness gap into error types. Rejections are classified as translation errors (T), judge misjudgments (J), or defective/ambiguous benchmark statements (B), using human labels for the tool-augmented agent and a validated two-stage LLM review (Claude Opus 5.5 with Lean access, checked by GPT-6.1 Sol) for systems with no human audit. All 268 reviewed rejections are released with their Lean checks.

4. A full 2³ factorial tool ablation of the agent. The agent's three tools — Expert Drafting (T, a draft from the fine-tuned Herald model), Knowledge Search (S, Mathlib symbol lookup plus web search), and Compiler Feedback (F, Lean REPL elaboration) — are toggled in all eight combinations over all 227 statements, separating effects on validity, faithfulness, and tool cost.

Main Findings

• Compilation systematically overstates faithfulness, but by very different amounts. Every one of the eight systems has a gap; across systems it ranges from 1.3 to 29.5 percentage points. The gap is 1.3–21.2 points for the seven one-shot systems and 29.5 points for the tool-augmented agent.

• The agent compiles far more than it faithfully states. The GPT-5.2 agent produces 198/227 compiling outputs (87.2%) but only 131/227 (57.7%) accepted. Acceptance rates are 19.8–27.3% for general-purpose one-shot LLMs, 10.1–13.8% for specialized formalizers, and 4.6–6.2% for prover-oriented models.

• The criterion is conservative and asymmetric. On an independent 59-case audit it agrees with the human majority on 54/59 = 91.5% (95% CI 81.6–96.3%); on the 53 compiling outputs where only judges decide, 48 (90.6%, CI 79.7–95.9%). Precision is high — 44/46 = 95.7% in Batch B and 67/70 = 95.7% in the positive audit — while negative confirmation is lower (10/13 = 76.9% in Batch B; 54/67 = 80.6% in Batch A). The criterion rarely accepts an unfaithful output but rejects some faithful ones.

• It beats LeanScorer on the same sample. 54/59 versus 45/59 human agreement (paired: 43 both correct, 11 criterion-only, 2 LeanScorer-only, 3 both wrong; exact McNemar p = 0.0225).

• Most of the gap is real translation error for seven of eight systems. Human review of all the agent's rejections confirms 23.8 of its 29.5 points. For the seven one-shot systems, 132 of 145 rejections are classified as translation errors (138 counting either review stage); the share of the gap that is translation error is 100% (Kimina-Prover), 97% (Goedel-Prover), 96% (Kimina-Autoformalizer), 88% (Herald), 79% (StepFun), 78% (GPT-5.2), 81% (agent), and 33% (Gemini-2.5-Pro, one of whose three rejections is a translation error). Errors include tautologies, True placeholders, vacuous hypotheses, and unrelated algebraic structures.

• For two newer models, most of the measured gap is the judge's fault, not the system's. GPT-6 Astra and Claude Opus 5.5 compile 94.3% and 96.0% without tools; GPT-5.2 alone accepts 83.3% for each (versus 20.7% for one-shot GPT-5.2), leaving gaps of 11.0 and 12.8 points. The review flags only 1 of GPT-6 Astra's 25 and 3 of Opus 5.5's 29 rejections as translation errors (4 each counting either stage), bounding real errors at roughly 1.2 and 3.6 points. Lean independently proves 9 pairs of differently graded outputs equivalent.

• This produces a counterintuitive share effect. The share of rejections that are real errors follows the positive predictive value e(1−m)/(e(1−m)+(1−e)f) of a rejection, which falls below one half once e < f/(1−m+f). The better a system is, the smaller the fraction of its rejections that are genuine translation errors.

• Lean feedback drives the agent's gains — and most of its gap. Elaboration feedback (F) raises compilation by +49.3 points [44.5, 54.0] and faithfulness by +27.2 points [22.7, 31.8], but 22.1 points [18.0, 26.3] of that compile gain fails the semantic criterion. The jump from configuration 000 to 010 takes compiled outputs from 54 to 203 and faithful outputs from 45 to 127, while the compile-pass gap grows from 9 to 76.

• Search helps faithfulness only without feedback. Grounding search (S) adds +8.5 points of faithfulness [5.4, 11.6] overall with no measurable gap change (+1.2 [−1.8, 4.3]). Its effect without feedback is +13.9 points [9.3, 18.3]; with feedback it is +3.1 [−1.3, 7.7] on faithfulness, −5.1 on compilation, and −8.1 on the gap, while REPL calls fall 28.7% (010→011) and 32.2% (110→111).

• The translation prior barely moves faithfulness. Expert Drafting (T) adds +4.0 points of compilation [1.3, 6.6] but only +1.0 of faithfulness [−1.9, 3.7], and grows the gap by +3.0 [0.2, 5.7].

• Domain matters. Feedback's faithfulness gain is +47.4 points in Complex Analysis (76.7% of compiling outputs faithful at F=1) versus +35.9 in Real Analysis (58.7%), +23.4 in Topology (64.8%), and +21.4 in Algebra (64.0%).

• Net effects hide large per-item churn. Adding search under feedback makes 30 statements faithful and 25 unfaithful, a net of only +5. The all-tools configuration misses 44 statements that some other configuration formalizes faithfully, 34 of which compile under 111 but fail the criterion. Across all eight configurations, 175/227 (77.1%) are faithful at least once and 27/227 (11.9%) every time.

• Long trajectories are a warning sign. With feedback enabled, faithfulness falls from 82.9% for runs of 1–2 steps to 11.5% for runs of 19–24 steps.

Methodology in Plain English

The authors pick 227 university-level theorem statements from four open textbooks and ask eight systems to translate each one into Lean 4 in a statement-only setting — the output must be a theorem declaration ending in := by sorry, with no proof attempt. Each output is then compiled in Lean with Mathlib.

Since no canonical Lean code exists for these statements, they cannot be scored by exact match. Instead, the authors compile the output and then have two LLM judges from different families read the original statement and the generated Lean side by side and grade faithfulness 0–10. Only outputs that compile and get at least 9 from both judges count as accepted.

To check whether this automated rule can be trusted, they run blinded human audits: a domain-proportional random sample of outputs the rule accepts, a complete review of every compiling output the rule rejects for their agent, and a full human evaluation of an external system (Aristotle, Harmonic's Lean-based reasoning system) on 60 randomly sampled statements. They also compare against an existing scoring method on the same sample, swap in a third judge family, move the threshold around, and use a bounded proof-search tool (BEq) to formally check whether accepted outputs for the same statement are logically equivalent to one another.

For the systems without human labels, they build a two-stage reviewer: Claude Opus 5.5 agents with Lean REPL and textbook access label each rejection as a translation error, a judge error, or a defective statement, and GPT-6.1 Sol reviews each label. They first validate this reviewer on the 69 rejections that humans already labeled, showing it agrees with the human majority (79.7%, κ = 0.41) at least as well as human reviewers agree with each other (69.6–74.6%, κ = 0.12–0.27), then apply it to the rest.

Finally, they strip the agent down: they toggle its three tools (drafting prior, search, compiler feedback) in all eight on/off combinations, run every statement under every combination, and compute standard factorial main effects and interactions with bootstrap confidence intervals.

Why This Matters

Research impact. Much of the autoformalization literature uses compilation, back-translation, or reference matching as a proxy for correctness. This paper shows that proxy can be off by up to 29.5 percentage points, and — more importantly — that the interpretation of a gap depends on how good the system is. A weak system's rejections are mostly its own errors; a strong system's rejections are mostly the judge's. That distinction is invisible in aggregate accuracy numbers and has direct consequences for how benchmarks should be reported.

Practical applications:

• Autoformalization benchmark design — provides a validated, reference-free scoring recipe for settings where multiple Lean encodings can all be faithful, plus a released benchmark with flagged defective items.
• Agentic formalization pipelines — the ablation identifies compiler feedback as the dominant driver of validity gains and quantifies how much of that gain is semantically empty, giving pipeline designers a concrete trade-off to manage.
• Judge and reward-model engineering — the analysis of GPT-5.2 rejecting equivalent but non-standard encodings (with 9 Lean-proven equivalences among differently graded outputs) is a direct failure catalogue for LLM-as-judge systems in formal mathematics.
• Training data curation for Lean models — the finding that prover-oriented models frequently emit tactic bodies or unextractable declarations despite an explicit statement-only prompt warns against reusing prover checkpoints as formalizers.

Industry relevance. Any organization building verification-backed LLM tooling — proof assistants in software verification, formal specification of safety requirements, or math-education systems that check student answers — depends on the guarantee that the formal artifact means what the user asked for. This paper quantifies precisely how much that guarantee cannot be inferred from a green compiler checkmark, and offers a cheaper audited alternative to full human review.

Future Directions

• Judge error is now the bottleneck for strong systems. With only 4 of 54 rejections for GPT-6 Astra and Claude Opus 5.5 classified as real translation errors, the paper's own criterion is the limiting factor. The authors note their audit does not estimate these models' overall error rates because accepted outputs were not reviewed — closing that loop

Authors’ abstract

Lean verifies that a generated declaration is well typed, but cannot check whether it states what the user intended. We measure how far compilation overstates faithfulness in statement autoformalization without canonical Lean targets. Our criterion requires Lean compilation and agreement of two LLM judges from different model families. On an independent random audit, it agrees with the human majority on 91.5% of cases; it rarely accepts an unfaithful output but rejects some faithful ones. Across eight systems on 227 university-level statements, the gap between compiling and accepted outputs ranges from 1.3 to 29.5 percentage points: our tool-augmented agent compiles 87.2% of the statements, but only 57.7% are accepted. Human review of all the agent's rejections confirms that 23.8 of its 29.5 points are real translation errors. For the gaps of the seven one-shot systems, a two-stage review by Claude Opus 5.5 with Lean and GPT-6.1 Sol, validated on these human labels, finds that 78-100% are real translation errors for six of them. When GPT-5.2, one of the two judges, grades the translations of two models released after it, GPT-6 Astra and Claude Opus 5.5, it accepts 83% of the statements for each, against 21% for one-shot GPT-5.2. For these two models, the same review classifies only 4 of their 54 rejections (7%) as translation errors, so most of their measured gap is judge errors rather than translation errors. This is consistent with these systems erring less while the judge does not: the fewer errors a system makes, the smaller the share of its rejections that are translation errors. Finally, a 2^3 tool ablation of the agent shows that Lean feedback drives most of its compilation gain, and that nearly half of this gain fails the semantic criterion. Code and data are available at https://github.com/grenadeComing/beyond-compilation.