Evaluating the Robustness of Proof Autoformalization in Lean 4

Summary (Overview)

• This paper presents the first study on the robustness of proof autoformalization — the task of translating natural-language (NL) mathematical proofs into formal-language (FL) proofs in Lean 4.
• The authors introduce two categories of perturbations: global perturbations (paraphrasing the entire NL proof in different styles) and local perturbations (modifying a single value, symbol, or proof step, possibly in a counterfactual way).
• A benchmark is built on miniF2F and MATH-500 with 2,637 local perturbation instances and 3,720 problem-style instances across five NL proof styles.
• Seven recent models are evaluated, including specialized autoformalizers (ProofBridge, ProofFlow), repurposed theorem provers (Kimina-Prover variants, DeepSeek-Prover-V2, Goedel-Prover-V2), and a general-purpose LLM (Gemini-3.1-Pro).
• Key finding: All existing models exhibit limited robustness — they are unstable under global perturbations and mostly fail to remain faithful under local perturbations, with reversion rates above 90% for proof-level number/symbol edits in several models.

Introduction and Theoretical Foundation

Background

Large language models (LLMs) have demonstrated strong capabilities in mathematical reasoning, but natural-language reasoning is inherently challenging to verify reliably. Formal theorem provers (Coq, Isabelle, Lean 4) represent mathematical statements and proofs in rigorous formal languages, enabling formal verification. The paper motivates bridging NL and FL reasoning:

• NL → FL direction: NL reasoning can guide the generation of FL proofs
• FL → NL direction: FL verification can verify NL reasoning once faithfully translated

Autoformalization Categories

The paper distinguishes between:

• Statement autoformalization: translating only the mathematical statement (relatively established)
• Proof autoformalization: translating both statement and proof (substantially more challenging, recently gained attention)

Motivation for Robustness

Existing evaluations focus on translating well-formed informal proofs from curated datasets. The authors argue that a robust proof autoformalizer must remain faithful even for informal proofs that diverge from idealized ones. This is critical for:

1. Practical effectiveness across NL proofs of varying styles and quality
2. Error detection: enabling future work that combines autoformalization with Lean-based formal verification to verify NL proofs and detect errors

Key Definitions

For a target model $f$, the task is to translate an NL theorem-proof pair $M_{NL} = \langle T_{NL}, P_{NL} \rangle$ into an FL pair $\widehat{M}_{FL} = \langle \widehat{T}_{FL}, \widehat{P}_{FL} \rangle$:

$$\widehat{M}_{FL} = f(M_{NL})$$

Methodology

Global Perturbations

Global perturbations paraphrase the entire NL proof while preserving mathematical semantics. Two LLMs generate paraphrases:

• Gemini-2.5-Flash (G) — closed-source model
• Qwen3.5-397B-A17B (Q) — open-source model

Two paraphrasing modes per model:

• Free-form (-FF): restate the NL proof in different wording/style
• Step-by-step (-Step): reorganize into a numbered sequence of steps

This yields five NL proof styles per problem: Orig, G-FF, Q-FF, G-Step, Q-Step.

Correctness Metrics

Each generated FL output is evaluated by three complementary metrics:

1. Type Correctness (TC): whether the generated FL compiles (checked by Lean compiler)
2. Statement Semantic Correctness (StmtSC): whether the formal statement semantically matches the NL statement (LLM judge)
3. Proof Semantic Correctness (ProofSC): whether the formal proof semantically matches the NL proof (LLM judge)

FullyCorrect is satisfied only when all three metrics are satisfied simultaneously.

Local Perturbations

Local perturbations change a single value, symbol, or proof step, possibly in a counterfactual way. Three edit types:

1. Number edit: changes a numeric literal to a different value of similar magnitude and same sign
2. Symbol edit: replaces a relation or operator with its opposite (e.g., $+$ with $-$ or $\le$ with $\ge$)
3. Step deletion: removes the justification of one substantive proof step while keeping its stated outcome

Example

Given a proof "from $2x + 3 = 17$ we get $2x = 14$, so $x = 7$", changing the intermediate step to $2x = 16$:

• A Faithful Autoformalizer produces $2 * x = 16$
• A Biased Autoformalizer reverts to $2 * x = 14$

Faithfulness Metrics

Outputs are classified as:

• Faithful: reflects the edited input
• Reverted: matches the original unedited input
• Unclear: matches neither (empty, fails to compile, or never mentions the edited entity)

Metrics computed:

• Faithful Rate (FR): fraction of identifiable outputs that are faithful
• Reverted Rate (RR): fraction of identifiable outputs that are reverted
• Other/Unclear Rate (OUR): unclear share of all outputs

Note: $FR + RR = 1$ for identifiable outputs.

Dataset Statistics

Models Evaluated

Repurposed models (specialized theorem provers, repurposed for autoformalization):

• Kimina-Prover-RL-1.7B
• Kimina-Prover-Distill-8B
• DeepSeek-Prover-V2-7B
• Goedel-Prover-V2-8B
• Gemini-3.1-Pro (general-purpose LLM)

Specialized proof autoformalization models:

• ProofBridge: trained by SFT from Kimina-Prover-RL-1.7B on autoformalization data
• ProofFlow: formalization pipeline preserving proof structure via dependency DAGs

Empirical Validation / Results

Robustness to Global Perturbations

Table 2: FullyCorrect (%) across five NL proof styles

Key observations:

• All models show sensitivity to NL proof presentation
• Rewriting has mixed effects: can improve (DeepSeek-Prover-V2: 1.2% → 12.7% on miniF2F Q-FF) or degrade (Kimina-Prover-Distill-8B on MATH-500) performance
• No input style dominates uniformly
• Model rankings change across styles (e.g., ProofBridge strongest on Orig, Gemini-3.1-Pro strongest on all rewrites on miniF2F)

Faithfulness under Local Perturbations

Proof-Level Edits (Table 3)

Number edit results (FR/RR %):

Symbol edit results (FR/RR %):

Step deletion results (FR/RR %):

Statement-Level Edits (Table 4)

Number edit results (FR/RR %):

Symbol edit results (FR/RR %):

Key Findings

1. Proof-level number/symbol edits are hardest: For five models (excluding ProofBridge and ProofFlow), average FR is only 6.3%, with RR above 90% in almost all cells.

2. Specialized autoformalizers are relatively more faithful: ProofBridge achieves 41.8% average FR on proof-level number/symbol edits; ProofFlow achieves 26.1%. However, both still revert in more than half of identifiable cases.

3. Step deletion shows higher FR but frequent reversion: RR ranges from 48.2% to 75.2% on miniF2F, indicating models often fill in removed reasoning steps.

4. Statement edits are much easier: Every model shows higher FR for statement-level edits than proof-level edits of the same type. This is consistent with the bias hypothesis: since a Biased Autoformalizer tends to produce FL proofs consistent with the statement, statement edits are naturally more likely reflected.

Perturbation Reliability Validation

• Local edits: Automated character-by-character comparison confirms all 2,637 cases differ from originals in exactly one contiguous span (100% validity).
• Global rewrites: 96.4% of 2,976 rewrites preserve every numeric and symbolic token; manual audit of 100 stratified samples confirms semantic preservation.

Theoretical and Practical Implications

Theoretical Implications

1. Bias in autoformalizers: The paper identifies a systematic bias where models silently override local edits with their own inferences, driven by spurious training patterns from well-formed proofs. This reveals a fundamental limitation in how current models learn the NL→FL mapping.

2. Evaluation methodology: The work demonstrates that evaluation solely on well-formed proofs from standard datasets can substantially over- or understate a model's true autoformalization ability, highlighting the need for robustness-aware evaluation.

3. Faithful vs. biased formalization: The paper establishes a theoretical distinction between Faithful and Biased Autoformalizers, providing a framework for characterizing autoformalization behavior under input perturbations.

Practical Implications

1. Verification pipeline: The faithfulness failures undermine the potential use of autoformalization for verifying NL proofs. If a model silently corrects errors during translation, it cannot be used to detect errors in NL reasoning.

2. Model development: The results suggest that specialized autoformalization training (as in ProofBridge) improves faithfulness but is insufficient. Future work should explicitly incorporate robustness objectives.

3. Benchmark value: The released benchmark (code and data available at https://github.com/ucr-rai/robust-proof-autoformalization) provides a standard evaluation suite for future robustness research.

Conclusion

This work presents the first study on the robustness of proof autoformalization in Lean 4. The authors design two perturbation categories with accompanying metrics:

• Global perturbations test correctness stability under semantic-preserving rewrites
• Local perturbations test faithfulness under counterfactual edits

Evaluating seven recent models on miniF2F and MATH-500 reveals two types of robustness failures:

1. Instability under global perturbations: Models are sensitive to surface wording rather than underlying mathematics
2. Limited faithfulness under local perturbations: Models frequently revert edits, particularly at the proof level

The findings suggest that proof autoformalization should be evaluated beyond correctness on well-formed proofs. Future development should consider robustness to NL proofs of varying styles and quality to build reliable proof autoformalizers that can enable broader applications, particularly the verification of NL proofs through formal systems.