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

Summary (Overview)

• Core problem: Natural-language-to-Lean formalization requires generating the formal statement itself, not just proving against fixed statements. Compilation alone is insufficient—a Lean declaration can type-check while omitting hypotheses, changing domains, or expressing vacuous claims.

• Key finding: 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. Human audits confirm this gap represents genuine semantic failures in most cases.

• Methodological contribution: A human-calibrated consensus LLM-as-Judge protocol combining Lean compilation with GPT-5.2/Gemini-2.5-Pro semantic scoring, validated by human expert audits (96.0% precision on consensus-positive outputs; 82.4% confirmation of semantic failures on consensus-negative compile-pass outputs).

• Bottleneck decomposition: A full $2^3$ factorial design reveals that elaboration feedback (F) is the largest validity intervention (+32.3 points), search (S) mainly improves grounding and selectivity (+6.8 points), and fine-tuned drafting (T) is largely substitutable (+0.9 points, not statistically significant).

• Key implication: Formal validity, proof-oriented Lean competence, and faithful statement generation should be reported separately—prover-oriented models (Goedel-Prover, Kimina-Prover) achieve only 4.0–5.0% consensus faithfulness despite 19.2% compilation rates.

Introduction and Theoretical Foundation

Background and Motivation

Large language models (LLMs) have demonstrated strong mathematical problem-solving ability, while proof assistants such as Lean 4 provide a trusted kernel for checking formal syntax, types, and proofs. However, the existing literature focuses predominantly on theorem proving: given a fixed formal statement, generate a proof the checker accepts. This setting has a clean success criterion—checker acceptance is a strong evaluation signal when the statement is fixed and trusted.

Statement formalization has a fundamentally different failure mode: the model generates the formal statement itself. Lean can verify that a declaration is well-typed, but it cannot verify that the declaration expresses the same mathematical meaning as the original natural-language theorem. A compiling statement may:

• Omit a hypothesis
• Change the domain
• Strengthen or weaken the claim
• Encode a vacuous version of the result

Related Work

Prior work has partially addressed this through:

• ProofNet (Azerbayev et al., 2023): reference-pair benchmarks pairing natural-language theorems with Lean statements
• Lean Workbook (Ying et al., 2024): filtering pipelines using compilation, back-translation, NLI, and human checks
• Herald (Gao et al., 2025): compiler/back-translation checks for Lean 4 translators
• FormalAlign (Lu et al., 2025): alignment evaluators for informal–formal semantic alignment
• BEq (Liu et al., 2025): faithful equivalence metrics using neuro-symbolic approaches

The authors position their work as complementary to reference-based equivalence metrics: their benchmark consists of natural-language textbook statements without gold Lean declarations, requiring genuine translation rather than retrieval.

Methodology

Task Definition

Formally, let $\mathcal{X}$ be the space of informal mathematical statements and $\mathcal{V}$ be the space of valid Lean 4 declarations. Given an input $x \in \mathcal{X}$, the system must generate a statement $y \in \mathcal{V}$ satisfying three criteria:

1. Syntactic validity: It compiles in Lean 4 with Mathlib
2. Statement-centricity: It omits proofs via := by sorry
3. Semantic faithfulness: It expresses the same mathematical claim as $x$

Dataset Construction

A curated benchmark of 400 graduate-level statement entries drawn evenly from four domains:

Sources were selected as open-source LaTeX lecture notes providing natural-language statements without accompanying formal code.

Evaluation Protocol

The two-stage Consensus LLM-as-Judge protocol:

1. Compiler Verification filter: Any code that fails to compile is not faithful.
2. Semantic judging: Two independent LLM judges (GPT-5.2 in Medium Thinking mode and Gemini-2.5-Pro) compare the generated Lean declaration against the original natural-language input, assigning statement-level faithfulness scores on a 0–10 scale.

The success metric defines a translation $y$ for input $x$ as Faithful if and only if:

$$\text{Compiles}(y) = \text{True} \quad \text{AND} \quad \min\{\text{Score}_{\text{GPT}}(x, y), \text{Score}_{\text{Gemini}}(x, y)\} \geq 9$$

Cross-judge consensus: Gemini-2.5-Pro consistently accepts more outputs than GPT-5.2, and most GPT-5.2 positives are also accepted by Gemini:

$$\operatorname{Pass}_{\text{Consensus}} = \operatorname{Pass}_{\text{GPT}} \cap \operatorname{Pass}_{\text{Gemini}}, \quad \frac{|\operatorname{Pass}_{\text{GPT}} \cap \operatorname{Pass}_{\text{Gemini}}|}{|\operatorname{Pass}_{\text{GPT}}|} \text{ is high empirically}$$

The empirical GPT-to-Gemini coverage is 97.6–98.9% across system groups.

Agent Architecture and Tool Factors

The agent uses a central LLM orchestrator (GPT-5.2) interacting with the Lean 4 environment via a defined API, structured as a controlled implementation of three common remedies:

Each tool setting is a bit vector:

$$c = (t, f, s) \in \{0, 1\}^3, \quad \mathcal{C} = \{000, 001, 010, 011, 100, 101, 110, 111\}$$

Main effects are high-minus-low averages over the other factors:

$$\Delta_F(m) = \frac{1}{4} \sum_{t, s \in \{0,1\}} \left[ m(t, 1, s) - m(t, 0, s) \right]$$

All configurations use identical role definitions, output requirements (:= by sorry), and anti-hallucination instructions—only the tool-availability block varies.

Empirical Validation / Results

Human Expert Validation

Human audits establish the metric as a conservative, high-precision operating point:

• 96.0% human-confirmed precision on consensus-positive outputs (194/202 cases)
• 82.4% of compile-pass consensus-negative outputs confirmed as genuine semantic failures (112/136 cases)
• 24/136 (17.6%) audited compile-pass negative-bucket cases were human-rescued faithful cases

Main Results

Key observations:

• Goedel-Prover compiles 19.2% but is consensus-faithful on only 5.0%—compilation alone substantially overstates progress
• Prover-oriented models frequently emit proof-oriented reasoning despite explicit statement-only prompts
• The full agent's 89.5% compile rate might suggest the task is nearly solved under compiler-only evaluation, but 116/400 entries compile without being accepted as faithful

Cross-Configuration Outcomes

Factorial Decomposition Results

Main effects on Faithful accuracy (bootstrap 95% CIs, B=10,000):

Full $2^3$ configuration results (N=400):

Domain-wise feedback effects:

Per-Item Transition Ledger

Trajectory Length as Warning Signal

Pooling the four F=1 configurations, faithfulness falls from 81.3% for 1–2 step runs to 12.0% for 19–24 step runs. Across nonempty no-feedback configurations, the corresponding drop is only 32.0% to 17.0%. This makes trajectory length a useful warning signal specifically when feedback is enabled.

Theoretical and Practical Implications

Moving Beyond Compilation as Success

The central lesson is that execution feedback can make many more declarations type-check, but it does not decide whether the checked object is the intended theorem. This has profound implications for how the field should evaluate autoformalization systems:

1. Compilation is a necessary but insufficient filter: The 29.0-point gap between compile rate (89.5%) and consensus faithfulness (60.5%) demonstrates that compiler-only evaluation dramatically overstates progress.

2. Proof-oriented competence ≠ statement formalization competence: Prover-trained models (Goedel-Prover, Kimina-Prover) fail to transfer their Lean competence to faithful statement generation, suggesting these are distinct capabilities requiring separate evaluation and training.

3. Tools are not monotone add-ons: The factorial analysis reveals that feedback, search, and drafting can help, interfere, or change failure modes depending on domain and trajectory. The negative interactions (e.g., T slightly hurting with F enabled: $\Delta_T(F=1) = -2.0$ pts) show that average gains alone are insufficient for understanding a formalization pipeline.

Bottleneck-Specific Insights

• Elaboration feedback (F) is the largest validity intervention but not a semantic oracle: it moves many noncompiling cases into both the faithful and compile-pass-but-unfaithful buckets (gap increases from 26 to 121 for 000→010).

• Search (S) serves dual roles: as a capability tool when feedback is absent ($\Delta_S(F=0) = +12.4$ pts) and as an efficiency/selectivity tool when feedback is present ($\Delta_S(F=1) = +1.2$ pts, with REPL calls falling by 29.8% for 010→011 and 26.6% for 110→111).

• Translation prior (T) is largely substitutable: it helps without feedback ($\Delta_T(F=0) = +3.9$ pts) but slightly hurts with feedback ($\Delta_T(F=1) = -2.0$ pts), suggesting fine-tuned drafting is redundant once a strong orchestrator has compiler feedback and grounding.

Domain-Specific Considerations

Complex Analysis converts most feedback-driven validity gains into faithful statements (81.5% faithful/compile ratio), while Algebra (63.5%) and Topology (64.5%) gain far less. Topology's lower conversion is attributed to advanced Mathlib encoding and coverage constraints in examples involving covering spaces and fundamental groups.

Conclusion

Main Takeaways

1. Statement formalization should be evaluated as meaning preservation, not only as Lean acceptance. Human-calibrated semantic evaluation makes the compile-pass gap visible and provides a conservative way to compare systems at scale.

2. The bottleneck is semantic, not syntactic. Even with strong validity repair (89.5% compilation), nearly one-third of benchmark entries land in the compile-pass but consensus-unfaithful bucket, and human review confirms this is usually a genuine semantic failure.

3. Tools should be understood as moving different boundaries. Feedback dominates validity repair, search improves grounding and selectivity, and fine-tuned drafting is largely substitutable in this tool stack.

Future Directions

The authors suggest that future systems should:

• Pair strong Lean feedback with semantic evaluation and policies that decide when to search, repair, restart, or stop
• Implement per-instance routing or early-stopping policies, since final scores alone do not distinguish a clean first translation from a long repair loop that eventually compiles the wrong statement
• Use trajectory length as a warning signal—longer repair trajectories with feedback enabled are strongly associated with semantic drift (12.0% faithfulness for 19–24 step runs vs. 81.3% for 1–2 step runs)

Limitations

• The benchmark covers 400 statements from four open sources; broader coverage and research-level statements remain out of scope
• The Search factor measures implemented retrieval tools (Mathlib symbol lookup, namespace resolution, web search), not dedicated semantic retrievers like LeanSearch—stronger retrieval may change the Search main effect and F×S interaction
• The main orchestrator and one judge (GPT-5.2) are from the same model family; Sonnet/Gemini orchestrator checks and human audits mitigate but do not eliminate this possible dependence
• Tool-augmented formalization is more expensive than one-shot generation; the full REPL loop remains a barrier to real-time interactive use

The released benchmark, agent implementation, evaluation scripts, and tool-call logs support reproducible analysis of successful and failed formalization trajectories, enabling the field to move toward more diagnostic views of autoformalization.