Evaluating the Robustness of Proof Autoformalization in Lean 4

The gist The paper presents the first study on proof autoformalization robustness by evaluating how well existing models maintain correctness and faithfulness when subjected to global paraphrases and local edits in natural language proofs.

Robustness Categories

The researchers formulated two categories of perturbations to test robustness: global perturbations, which paraphrases the entire NL proof in a different style, under which the formalization should remain consistent (Page 2). Second, they designed local perturbations, where "a subtle change is introduced into the NL proof — even a counterfactual one that represents an error — the autoformalization should faithfully reflect this change in the FL proof rather than inferring a different one on its own" (Page 2).

Evaluation Methodology

The study builds a benchmark using miniF2F and MATH-500 datasets to measure stability under these perturbations (Page 1). For global perturbations, robustness is measured by the stability of correctness across styles: large variation across styles indicates sensitivity to surface wording rather than the underlying mathematics (Page 3). Correctness is assessed using three metrics: Type Correctness (TC), Statement Semantic Correctness (StmtSC), and Proof Semantic Correctness (ProofSC); a FullyCorrect output requires all three to be satisfied simultaneously (Page 3). For local perturbations, faithfulness is measured by the Faithful Rate (FR) and Reverted Rate (RR); a higher FR marks a Faithful Autoformalizer, while a higher RR indicates a Biased Autoformalizer (Page 3).

Perturbation Details

The global perturbations involve using LLMs like Gemini-2.5-Flash and Qwen3.5-397B-A17B to generate paraphrases in free-form (-FF) and step-by-step (-Step) modes, which expose models to different wording, levels of detail, and proof organization (Page 3). Local perturbations include three types: a number edit (changing a numeric literal), a symbol edit (replacing a relation or operator with its opposite), and a step deletion (removing the justification of one substantive proof step while keeping its stated outcome) (Page 3).

Key Findings on Model Performance

The experiments reveal that all existing proof autoformalization methods exhibit limited robustness, typically suffer from unstable correctness under global perturbations and limited faithfulness under local perturbations (Page 1). Specifically, models are sensitive to global perturbations and mostly fail to remain faithful under local perturbations (Page 1). The results show that for seven recent models evaluated, they generally exhibit instability across different proof styles when exposed to global paraphrases (Table 2, Page 6), and they often revert or fail to reflect local edits under counterfactual changes (Table 3 and Table 4, Pages 8 and 9). Specialized models like ProofBridge and ProofFlow show relatively better faithfulness on certain local perturbations compared to other models (Page 8).

Conclusion

The study concludes that "proof autoformalization should be evaluated beyond correctness on well-formed proofs from standard datasets; robustness to NL proofs of varying styles and quality should be considered in future development to build reliable proof autoformalizers that can enable broader applications" (Page 5). The findings suggest a substantial need for improvement in existing models regarding their stability under varied input conditions (Page 1).

Evaluating the Robustness of Proof Autoformalization in Lean 4

Abstract

Page 1

The gist The paper presents the first study on proof autoformalization robustness by evaluating how well existing models maintain correctness and faithfulness when subjected to global paraphrases and local edits.

Robustness Categories The researchers formulated two categories of perturbations to test robustness: global perturbations, which paraphrases the entire NL proof in a different style, under which the formalization should remain consistent (Page 2). Second, they designed local perturbations, where "a subtle change is introduced into the NL proof — even a counterfactual one that represents an error — the autoformalization should faithfully reflect this change in the FL proof rather than inferring a different one on its own" (Page 2).

Evaluation Methodology The study builds a benchmark using miniF2F and MATH-500 datasets to measure stability under these perturbations (Page 1). For global perturbations, robustness is measured by the stability of correctness across styles: large variation across styles indicates sensitivity to surface wording rather than the underlying mathematics (Page 3). Correctness is assessed using three metrics: Type Correctness (TC), Statement Semantic Correctness (StmtSC), and Proof Semantic Correctness (ProofSC); a FullyCorrect output requires all three to be satisfied simultaneously (Page 3).

Perturbation Details The global perturbations involve using LLMs like Gemini-2.5-Flash and Qwen3.5-397B-A17B to generate paraphrases in free-form (-FF) and step-by-step (-Step) modes, which expose models to different wording, levels of detail, and proof organization (Page 3). Local perturbations include three types: a number edit (changing a numeric literal), a symbol edit (replacing a relation or operator with its opposite), and a step deletion (removing the justification of one substantive proof step while keeping its stated outcome) (Page 3).

Key Findings on Model Performance The experiments reveal that all existing proof autoformalization methods exhibit limited robustness, typically suffer from unstable correctness under global perturbations and limited faithfulness under local perturbations (Page 1). Specifically, models are sensitive to global perturbations and mostly fail to remain faithful under local perturbations (Page 1). Specialized models like ProofBridge and ProofFlow show relatively better faithfulness on certain local perturbations compared to other models (Page 8).

Conclusion The study concludes that "proof autoformalization should be evaluated beyond correctness on well-formed proofs from standard datasets; robustness to NL proofs of varying styles and quality should be considered in future development to build reliable proof autoformalizers that can enable broader applications" (Page 5).

Acknowledgement This work is supported in part by an NVIDIA Academic Grant award.

Limitations Our study has several limitations that suggest directions for future work. First, the evaluated datasets consist of mathematical competition problems and undergraduate-level mathematics, which provide a controlled setting; we have not yet extended the study to more advanced domains (Page 9).

References Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. 2023. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics (Page 9).

Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, and 1 others. 1999. The coq proof assistant reference manual (Page 9).

Rafael Cabral, Tuan Manh Do, Xuejun Yu, Wai Ming Tai, Zijin Feng, and Xin Shen. 2025. Proofflow: A dependency graph approach to faithful proof autoformalization (Page 9).

Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. 2024. Herald: A natural language annotated lean 4 dataset (Page 9).

1. Develop robustness checks for proof autoformalization models by evaluating their correctness across global perturbations like free-form paraphrasing and step-by-step paraphrasing of natural language proofs. This will ensure that the formalization remains consistent even when the informal proof is written in different styles, as required by the paper's findings that all existing proof autoformalization methods exhibit limited robustness, typically suffer from unstable correctness under global perturbations.

2. Implement faithfulness evaluation for local perturbations by measuring whether a formalization faithfully reflects the perturbation rather than reverting to the original one or inferring a different one on its own. This allows the system to be distinguished from Biased Autoformalizers by quantifying their Faithful Rate (FR) versus Reverted Rate (RR).

3. Create specialized judges for semantic correctness that explicitly test CRITICAL — Independence from validity, comparing Lean tactics against natural-language steps on their own merit, ignoring whether the tactics prove the target theorem. This prevents models from being misled by incorrect formal proofs while still assessing if the reasoning sequence is equivalent.

4. Enhance local perturbation testing by distinguishing between edits in the statement versus edits in the proof, as research shows FR is higher when the same type of edit is made in the statement rather than in the proof. This informs model development where a Biased Autoformalizer tends to produce an FL proof consistent with the statement, making statement-level edits more likely to be reflected.

5. Design automated perturbation construction pipelines that rigorously verify that edits are localized, ensuring the two differ in exactly one contiguous span (the intended edit) and are otherwise identical (100%). This guarantees the validity of the robustness study by confirming that perturbations are indeed minimal and targeted.