Evaluating the Robustness of Proof Autoformalization in Lean 4

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

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. 证明自动形式化旨在将用自然语言编写的非正式数学证明翻译为 Lean 4 等形式语言中的形式化证明。目前已有若干研究开发了基于大语言模型（LLM）的证明自动形式化模型。

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. 我们在 miniF2F 和 MATH-500 数据集上构建了一个包含上述两种扰动的基准测试，并自动测量了证明自动形式化在全局扰动下的正确性稳定性，以及其输出对局部扰动的反映忠实度。我们评估了七个近期模型，结果显示它们均对全局扰动敏感，且在面对局部扰动时大多无法保持忠实性。