Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
06:00 · July 1, 2026 · arXiv cs.AI RSS
Theorem-proving benchmarks evaluate proof search against fixed formal statements, but natural-language-to-Lean formalization must generate the formal statement itself. In this setting, compilation is only a validity check: a Lean declaration may type-check while omitting hypotheses, changing domains, or expressing a vacuous claim. We study faithful statement formalization as both an evaluation problem and a bottleneck-attribution problem. On a 400-entry graduate-level benchmark spanning real analysis, complex analysis, topology, and algebra, our protocol combines Lean compilation, cross-model semantic judging, and human expert calibration. The resulting picture is different from compile-rate evaluation: a full tool-augmented agent reaches 89.5% compilation but only 60.5% consensus faithfulness, exposing a 29.0-point compile-pass but consensus-unfaithful gap. Targeted human audits support the metric as a conservative decision boundary: across available case-level audits, 96.0% of consensus-positive outputs are human-confirmed faithful, while 82.4% of compile-pass consensus-negative outputs are human-confirmed semantic failures. Under this metric, existing one-shot formalizer models and prover-oriented Lean models remain low, suggesting that formal validity, proof-oriented Lean competence, and faithful statement generation should be reported separately. We then use a full $2^3$ factorial design to decompose three recurring interventions in formalization pipelines: parametric expert drafting, Mathlib/context search, and Lean elaboration feedback. Elaboration feedback is the largest validity intervention, but it also exposes a larger compile-pass semantic-failure bucket; search mainly improves grounding and selectivity; and fine-tuned drafting is largely substitutable in this tool stack once feedback and grounding are available.
Summary
Theorem-proving benchmarks have traditionally fixed the target formal statements and measured only an automated prover’s ability to find a proof. When the task shifts to translating natural-language mathematics into Lean, however, the model must first produce a declaration that both compiles and preserves the intended meaning. The authors show that successful compilation is merely a syntactic validity check: a Lean statement may type-check while silently dropping hypotheses, altering the mathematical domain, or stating a vacuous claim.
To expose this gap they introduce a 400-problem graduate-level benchmark drawn from real analysis, complex analysis, topology, and algebra. Their evaluation protocol combines Lean compilation, cross-model semantic adjudication, and targeted human calibration. Under this regime a fully tool-augmented agent reaches 89.5 % compilation success yet only 60.5 % consensus faithfulness, leaving a 29-point “compile-pass but unfaithful” residue. Human audits confirm the metric’s conservatism: 96 % of consensus-positive outputs are judged faithful by experts, while 82.4 % of compile-pass yet consensus-negative outputs are confirmed semantic failures.
The same protocol reveals that existing one-shot formalization models and prover-oriented Lean models remain weak on faithfulness, indicating that formal validity, proof-search competence, and semantic fidelity must be tracked separately. A 2³ factorial experiment then isolates three common pipeline interventions—parametric expert drafting, Mathlib/context retrieval, and Lean elaboration feedback. Elaboration feedback yields the largest validity gain but simultaneously enlarges the compile-pass semantic-failure bucket; retrieval chiefly improves grounding and selectivity; once feedback and retrieval are present, fine-tuned drafting adds little incremental value.
Why it matters
This research is highly relevant for AI researchers and advanced readers focusing on formal methods, automated theorem proving, and LLM reliability. It provides a rigorous evaluation framework that aligns with the Dutch and EU focus on creating trustworthy, verifiable, and transparent AI systems.
