2026-06-16原文2 min readUpdated: 2026-06-16

Evaluating the Robustness of Proof Autoformalization in Lean 4

This paper presents the first study on the robustness of proof autoformalization models in Lean 4. It introduces global and local perturbations to test model faithfulness, finding that all seven evaluated models are sensitive to changes and mostly fail to reflect local perturbations faithfully.

SourcearXiv Computational LinguisticsAuthor: Zhengtao Gui, Sheng Yang, Zhouxing Shi

[2606.14867] Evaluating the Robustness of Proof Autoformalization in Lean 4

[Submitted on 12 Jun 2026]

Title:Evaluating the Robustness of Proof Autoformalization in Lean 4

View a PDF of the paper titled Evaluating the Robustness of Proof Autoformalization in Lean 4, by Zhengtao Gui and 2 other authors

View PDF

Abstract:Proof autoformalization aims to translate a mathematical informal proof written in natural language into a formal proof in a formal language such as Lean~4. Several works have developed LLM-based models for proof autoformalization. However, existing evaluations have typically focused on translating well-formed informal proofs from curated datasets. We argue that a robust proof autoformalizer must remain faithful even for informal proofs that diverge from these idealized ones, and we present the first study on the robustness of proof autoformalization models. We formulate two categories of perturbations and evaluate robustness under each: a global perturbation paraphrases the informal proof in a different style, under which the formalization should remain consistent; a local perturbation alters a value, symbol, or proof step, possibly in a counterfactual way, and a robust formalization should faithfully reflect the perturbation rather than reverting to the original one or inferring a different one on its own. We build a benchmark with both perturbations on miniF2F and MATH-500, and automatically measure how stable a proof autoformalization's correctness is under global perturbations and how faithfully its output reflects local perturbations. We evaluate seven recent models, all of which are sensitive to global perturbations and mostly fail to remain faithful under local perturbations. Code and data are available via this https URL.

Comments: Preprint

Subjects:

Computation and Language (cs.CL); Artificial Intelligence (cs.AI); Machine Learning (cs.LG)

Cite as: arXiv:2606.14867 [cs.CL]

(or arXiv:2606.14867v1 [cs.CL] for this version)

https://doi.org/10.48550/arXiv.2606.14867

arXiv-issued DOI via DataCite (pending registration)

Submission history

From: Zhouxing Shi [view email] [v1] Fri, 12 Jun 2026 18:10:21 UTC (246 KB)

Full-text links:

Access Paper:

View a PDF of the paper titled Evaluating the Robustness of Proof Autoformalization in Lean 4, by Zhengtao Gui and 2 other authors

View PDF

TeX Source

view license

Current browse context:

cs.CL

new | recent | 2026-06

Change to browse by:

cs cs.AI cs.LG

References & Citations

NASA ADS

Google Scholar

Semantic Scholar

Data provided by:

Bibliographic Tools

Bibliographic and Citation Tools

Bibliographic Explorer Toggle

Bibliographic Explorer (What is the Explorer?)

Connected Papers Toggle

Connected Papers (What is Connected Papers?)

Litmaps Toggle

Litmaps (What is Litmaps?)

scite.ai Toggle

scite Smart Citations (What are Smart Citations?)

Code, Data, Media

Code, Data and Media Associated with this Article

alphaXiv Toggle

alphaXiv (What is alphaXiv?)

Links to Code Toggle

CatalyzeX Code Finder for Papers (What is CatalyzeX?)

DagsHub Toggle

DagsHub (What is DagsHub?)

GotitPub Toggle

Gotit.pub (What is GotitPub?)

Huggingface Toggle

Hugging Face (What is Huggingface?)

ScienceCast Toggle

ScienceCast (What is ScienceCast?)

Demos

Replicate Toggle

Replicate (What is Replicate?)

Spaces Toggle

Hugging Face Spaces (What is Spaces?)

Spaces Toggle

TXYZ.AI (What is TXYZ.AI?)