评估 Lean 4 证明自动形式化的鲁棒性

View PDF HTML (experimental)

Abstract:Proof autoformalization aims to translate a mathematical informal proof in natural language into a formal proof in a formal language such as Lean 4. Existing LLM-based models for proof autoformalization are typically evaluated only on 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: a global perturbation paraphrases the informal theorem-proof pair 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 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: their correctness varies under global perturbations, and they mostly fail to remain faithful under local perturbations.

Comments:	22 pages, 4 figures
Subjects:	Computation and Language (cs.CL); Artificial Intelligence (cs.AI); Machine Learning (cs.LG)
Cite as:	arXiv:2606.14867 [cs.CL]
	(or arXiv:2606.14867v3 [cs.CL] for this version)
	https://doi.org/10.48550/arXiv.2606.14867 arXiv-issued DOI via DataCite

Submission history

From: Zhengtao Gui [view email]
[v1] Fri, 12 Jun 2026 18:10:21 UTC (246 KB)
[v2] Fri, 16 Oct 2026 19:24:19 UTC (252 KB)
[v3] Thu, 29 Oct 2026 00:34:37 UTC (252 KB)