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

证明自动形式化旨在将以自然语言编写的数学非正式证明转换为正式语言（例如 Lean~4）的形式证明。一些工作已经开发了基于 LLM 的模型用于证明自动形式化。然而，现有的评估通常侧重于从整理的数据集中翻译格式良好的非正式证明。我们认为，即使对于与这些理想化证明不同的非正式证明，稳健的证明自动形式化器也必须保持忠实，并且我们提出了第一个关于证明自动形式化模型的稳健性的研究。我们制定了两类扰动，并评估了每种扰动的鲁棒性：全局扰动以不同的风格解释了非正式的证明，在这种情况下，形式化应该保持一致；局部扰动可能会以反事实的方式改变值、符号或证明步骤，而稳健的形式化应该忠实地反映扰动，而不是恢复到原始扰动或自行推断出不同的扰动。我们在 miniF2F 和 MATH-500 上建立了一个包含扰动的基准，并自动测量证明自动形式化的正确性在全局扰动下的稳定性以及其输出如何忠实地反映局部扰动。我们评估了七个最近的模型，所有这些模型都对全局扰动敏感，并且大多数在局部扰动下都无法保持忠实。代码和数据可通过 https://github.com/ucr-rai/robust-proof-autoformalization 获得。