评估Lean 4中证明自动形式化的鲁棒性
本文首次系统研究证明自动形式化模型在Lean 4中的鲁棒性。提出了全局扰动（改写风格）和局部扰动（修改值、符号或步骤）来测试模型的忠信度，发现所有七个评估模型均对全局扰动敏感，且多数无法忠实反映局部扰动。
证明自动形式化旨在将自然语言撰写的非正式数学证明转化为Lean 4等正式语言中的形式证明。近年来，基于大型语言模型（LLM）的自动形式化方法取得了显著进展，但现有评估通常仅关注从精选数据集中选取的、结构良好的非正式证明。然而，现实场景中的非正式证明可能偏离这些理想情况，例如使用不同的表述风格或包含错误。为此，来自加州大学河滨分校的研究人员首次系统研究了证明自动形式化模型的鲁棒性。
研究者提出了两类扰动来模拟现实中的变体。第一类是全局扰动，即用不同风格改写非正式证明，此时形式化结果应保持一致。第二类是局部扰动，即修改证明中的某个值、符号或步骤，甚至可以是反事实的修改；鲁棒的模型应忠实反映这一变化，而非自动纠回原样或自行推断。他们基于miniF2F和MATH-500数据集构建了包含两类扰动的基准测试，并自动评估了模型在全局扰动下正确性的稳定性以及局部扰动下输出的忠实性。
实验评估了七个近期模型，包括GPT-4o、Claude 3.5等。结果显示所有模型均对全局扰动敏感，即改变证明的表述风格后，形式化结果的正确率明显下降。在局部扰动下，大多数模型无法保持忠实，它们常常忽略修改后的值或步骤，而输出与原始证明一致的形式化结果。这表明当前自动形式化模型在应对非理想输入时存在显著脆弱性。
该研究揭示了当前自动形式化模型的脆弱性，并提供了公开代码与数据，为后续改进提供了方向。研究者希望通过这项工作，推动开发更鲁棒的自动形式化系统，以支持数学证明的自动化验证。