证明自动形式化鲁棒性基准提出

2026年10月20日，arXiv 人工智能板块发布研究，Zhengtao Gui 等作者提出首个针对证明自动形式化模型鲁棒性的研究。该研究设计两类扰动：全局扰动以不同风格改写非形式化定理-证明对，局部扰动改动数值、符号或证明步骤。研究在 miniF2F 和 MATH-500 上构建基准，评估七个近期模型，发现模型正确性在全局扰动下出现波动，且多数模型在局部扰动下无法保持忠实。该基准针对 Lean 4 中的证明自动形式化模型，用于自动衡量证明自动形式化正确性在全局扰动下的稳定性，以及输出对局部扰动的忠实程度。

AI 根据报道生成 · 2 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。