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

> Tool-augmented agents reach 89.5% compilation but only 60.5% semantic faithfulness, exposing a 29-point gap where Lean-valid statements misrepresent the original theorem.

- **Source:** [arXiv](https://arxiv.org/abs/2606.31002)
- **Published:** 2026-08-18
- **Permalink:** https://picx.dev/p/KxfmZJ
- **Whiteboard:** https://picx.dev/p/KxfmZJ/image

## Summary

# 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:

| Domain | Source Material | N |
|--------|----------------|-----|
| Real Analysis | Basic Analysis (Lebl) | 100 |
| Complex Analysis | Cultivating Complex Analysis (Lebl) | 100 |
| Topology | Notes on Topology (McKay) | 100 |
| Algebra | Abstract Algebra (Doty) | 100 |
| **Total** | | **400** |

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:

| Tool | Factor | Description |
|------|--------|-------------|
| **Expert Drafting** (T) | Translation prior | `lean4_translator` tool requesting drafts from the fine-tuned Herald model |
| **Knowledge Search** (S) | Grounding | `lean_inspect_name`, `lean_resolve_name` for Mathlib symbol lookup, plus general web search |
| **Compiler Feedback** (F) | Validity repair | `lean_repl_runner` exposing Lean elaboration feedback and error messages |

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

| System Category | Compile Rate | Consensus Faithfulness |
|----------------|-------------|----------------------|
| General-purpose LLM baselines | — | 19.8–28.0% |
| Specialized formalizers (Herald, Kimina-Autoformalizer, StepFun) | — | 9.0–12.3% |
| Prover-oriented models (Goedel-Prover, Kimina-Prover) | 19.2% | 4.0–5.0% |
| **Full tool-augmented agent (111)** | **89.5%** | **60.5%** |

**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

| Outcome | Count | Rate |
|---------|-------|------|
| All-tools config 111 faithful | 242/400 | 60.5% |
| Best single config 011 faithful | 248/400 | 62.0% |
| Faithful under at least one config | 313/400 | 78.2% |
| Faithful under every config | 41/400 | 10.2% |
| Never faithful under any config | 87/400 | 21.8% |
| Missed by 111 but faithful elsewhere | 71/400 | 17.8% |
| — of missed: compile-pass under 111 | 55/400 | 13.8% |
| — of missed: compile-fail under 111 | 16/400 | 4.0% |

### Factorial Decomposition Results

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

| Factor | X=1 | X=0 | Effect | 95% CI |
|--------|-----|-----|--------|--------|
| Elaboration feedback (F) | 60.6 | 28.3 | **+32.3** | [28.7, 35.9] |
| Grounding search (S) | 47.9 | 41.1 | **+6.8** | [3.6, 10.0] |
| Translation prior (T) | 44.9 | 44.0 | **+0.9** | [-2.1, 4.0] |

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

| Fixed factors | | $F=0$ | | $F=1$ | |
|---------------|-----|-------|------|-------|------|
| T | S | Comp. | Faith. | Comp. | Faith. |
| 0 | 0 | 26.25 | 19.75 | 91.50 | 61.25 |
| 1 | 0 | 30.25 | 24.50 | 93.50 | 58.75 |
| 0 | 1 | 45.50 | 33.00 | 87.25 | 62.00 |
| 1 | 1 | 50.00 | 36.00 | 89.50 | 60.50 |

**Domain-wise feedback effects**:

| Domain | Δ Compile | Δ Faithful | Δ Gap | Faithful/Compile (F=1) |
|--------|-----------|------------|-------|------------------------|
| Complex Analysis | +66.2 | +54.2 | +12.0 | 81.5% |
| Real Analysis | +56.8 | +31.2 | +25.5 | 57.4% |
| Topology | +42.0 | +22.8 | +19.2 | 64.5% |
| Algebra | +44.8 | +21.0 | +23.8 | 63.5% |

### Per-Item Transition Ledger

| Change | Configs | New faithful | Lost faithful | Net |
|--------|---------|-------------|---------------|-----|
| Add F alone | 000 → 010 | 175 | 9 | +166 |
| Add F with S | 001 → 011 | 129 | 13 | +116 |
| Add F with T,S | 101 → 111 | 117 | 19 | +98 |
| Add S with F | 010 → 011 | 42 | 39 | +3 |
| Add S with T,F | 110 → 111 | 38 | 31 | +7 |
| Add T with F,S | 011 → 111 | 33 | 39 | -6 |

### 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.

---

_Markdown view of https://picx.dev/p/KxfmZJ, served by PicX — AI-generated visual whiteboard summaries of research papers._