arXiv cs.AI· Zhengtao Gui, Sheng Yang, Zhouxing Shi·· 13 小时前AI 评分31
首个证明自动形式化鲁棒性研究：在 Lean 4 上评测七款模型
Evaluating the Robustness of Proof Autoformalization in Lean 4
AI 导读
首个针对证明自动形式化鲁棒性的研究提出两类扰动：全局扰动改写定理-证明对的风格，局部扰动修改数值、符号或证明步骤，并在 miniF2F 与 MATH-500 上构建基准。评测的七款近期模型在全局扰动下正确性出现波动，且在局部扰动下大多无法忠实反映改动。
正文 · AI 翻译
摘要：证明自动形式化旨在将自然语言中的非形式化数学证明转换为 Lean 4 等形式语言中的形式化证明。现有的基于 LLM 的证明自动形式化模型通常仅在来自精选数据集、格式良好的非形式化证明上进行评估。我们认为，一个稳健的证明自动形式化器即使面对偏离这些理想化形式的非形式化证明，也必须保持忠实，并且我们提出了首个关于证明自动形式化模型稳健性的研究。我们提出了两类扰动：全局扰动以不同风格改写非形式化定理-证明对，在此情况下形式化结果应保持一致；局部扰动改变某个值、符号或证明步骤，可能以反事实的方式进行，而稳健的形式化应忠实反映该扰动，而不是回退到原始内容或自行推断出不同的内容。我们在 miniF2F 和 MATH-500 上构建了包含这两类扰动的基准，并自动衡量证明自动形式化的正确性在全局扰动下有多稳定，以及其输出在局部扰动下有多忠实。我们评估了七个近期模型：它们的正确性在全局扰动下会发生变化，且大多无法在局部扰动下保持忠实。
| 评论： | 22 页，4 幅图 |
| 主题： | 计算与语言（cs.CL）；人工智能（cs.AI）；机器学习（cs.LG） |
| 引用为： | arXiv:2606.14867 [cs.CL] |
| （或 arXiv:2606.14867v3 [cs.CL] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2606.14867 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Zhengtao Gui [查看邮箱]
[v1]
2026 年 6 月 12 日星期五 18:10:21 UTC（246 KB）
[v2]
2026 年 10 月 16 日星期五 19:24:19 UTC（252 KB）
[v3]
2026 年 10 月 29 日星期四 00:34:37 UTC（252 KB）
来源：arXiv cs.AI · arxiv.org