arXiv Artificial Intelligence· Zhengtao Gui, Sheng Yang, Zhouxing Shi·2026-10-20 12:00· 3 小时前AI 评分31

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

Evaluating the Robustness of Proof Autoformalization in Lean 4

AI 导读

首个针对证明自动形式化模型鲁棒性的研究提出两类扰动：全局扰动以不同风格改写非形式化定理-证明对，局部扰动改动数值、符号或证明步骤。研究在 miniF2F 和 MATH-500 上构建基准，评估七个近期模型，发现其正确性在全局扰动下波动，且多数在局部扰动下无法保持忠实。