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

背景

证明自动形式化（Proof Autoformalization）旨在将用自然语言书写的非形式化数学证明，翻译为如 Lean 4 这样的形式化语言中的正式证明。近年来，随着大型语言模型（LLM）的发展，多个研究团队开发了基于 LLM 的证明自动形式化模型。

然而，现有的评估工作通常局限于将来自精心策划数据集的、结构良好的非形式化证明进行翻译。这种评估方式假设输入是理想化的、无噪声的。但在实际应用场景中，自然语言证明往往存在表述差异、细微错误或非标准逻辑。因此，一个鲁棒的证明自动形式化器必须在面对偏离理想化标准的非形式化证明时，依然保持忠实和一致性。本文提出了针对证明自动形式化模型鲁棒性的首次系统性研究。

核心内容

本研究通过构建包含两种类型扰动（Perturbations）的基准测试，来评估证明自动形式化模型的鲁棒性。这两种扰动分别对应全局扰动和局部扰动，旨在模拟真实世界中证明表述的多样性和潜在错误。

1. 扰动分类与评估标准

全局扰动（Global Perturbation）

• 定义：以不同的风格对非形式化证明进行改写（Paraphrasing），而不改变其数学含义。
• 评估目标：形式化结果应保持一致性。即无论自然语言表述如何变化，生成的形式化证明在逻辑上应等价。

局部扰动（Local Perturbation）

• 定义：改变证明中的某个值、符号或证明步骤，甚至可能以反事实（Counterfactual）的方式进行修改。
• 评估目标：鲁棒的形式化应忠实地反映这些局部扰动，而不是回退到原始证明或自行推断出不同的结论。这要求模型能够精确捕捉输入中的细微变化，并将其准确映射到形式化输出中。

2. 基准测试构建

研究者在 miniF2F 和 MATH-500 两个广泛使用的数学数据集上构建了包含上述两种扰动的基准测试。

• 全局稳定性测量：自动测量证明自动形式化在面临全局扰动时，其正确性的稳定程度。
• 局部忠实度测量：自动测量模型输出在多大程度上忠实地反映了局部扰动。

3. 模型评估结果

研究评估了七个近期的证明自动形式化模型。实验结果显示：

• 全局敏感性：所有被评估的模型都对全局扰动敏感，表明它们在处理同义改写时难以保持形式化的一致性。
• 局部忠实度缺失：大多数模型在面临局部扰动时失败，无法忠实反映输入中的细微变化，往往忽略扰动或产生错误的推断。

代码和数据已通过指定链接公开，供社区进一步研究和复现。

关键要点

• 现有评估的局限性：当前基于 LLM 的证明自动形式化研究多关注理想化、结构良好的证明，缺乏对非理想化输入鲁棒性的考量。
• 鲁棒性的双重维度：
  • 全局鲁棒性：要求模型对自然语言的风格变化不敏感，保持逻辑等价。
  • 局部鲁棒性：要求模型对输入中的具体数值、符号或步骤变化高度敏感，确保形式化输出精确对应输入变更。
• 基准测试创新：首次提出了针对证明自动形式化的扰动基准，涵盖 miniF2F 和 MATH-500 数据集，并提供了自动化的稳定性与忠实度测量方法。
• 当前模型表现不佳：评估的七个主流模型在全局扰动下均表现出敏感性，且在局部扰动下大多无法保持忠实，揭示了当前技术在处理真实世界非形式化证明时的脆弱性。

意义与影响

这项研究揭示了当前证明自动形式化技术在鲁棒性方面的显著短板。尽管基于 LLM 的方法在翻译标准证明方面取得了一定进展，但它们在面对自然语言的变体和细微错误时表现脆弱。

对学术界的意义：

• 为证明自动形式化领域提供了新的评估维度，强调了“鲁棒性”作为核心指标的重要性。
• 提出的全局和局部扰动框架为后续研究提供了标准化的测试基准，有助于更公平地比较不同模型的性能。

对应用的影响：

• 在实际数学辅助证明或形式化验证场景中，自然语言输入往往是非标准且包含噪声的。当前模型的鲁棒性不足限制了其在真实环境中的可靠部署。
• 未来的模型开发需要着重提升对语义不变性（全局）和细节敏感性（局部）的平衡能力，以增强系统在复杂、非理想化输入下的实用性。

通过公开代码和数据，本研究促进了社区的透明度和可复现性，为开发更稳健、更可靠的证明自动形式化系统奠定了基础。