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

arXiv cs.CL 论文
autoformalization lean4 robustness llm mathematical-proofs formal-verification

摘要

本文评估了在全局和局部扰动下，Lean 4中证明自动形式化模型的鲁棒性，发现当前基于LLM的模型对扰动敏感，且常常无法忠实地反映局部变化。

arXiv:2606.14867v1 公告类型：新 摘要：证明自动形式化旨在将自然语言编写的数学非正式证明翻译成形式语言（如Lean 4）中的形式证明。已有若干工作开发了基于LLM的证明自动形式化模型。然而，现有评估通常侧重于翻译来自精心策划数据集的、结构良好的非正式证明。我们认为，一个鲁棒的证明自动形式化器即使在非正式证明偏离这些理想化版本时也必须保持忠实，并提出了首个关于证明自动形式化模型鲁棒性的研究。我们制定了两类扰动，并评估了每种扰动下的鲁棒性：全局扰动以不同风格改写非正式证明，此时形式化结果应保持一致；局部扰动改变一个值、符号或证明步骤，可能以反事实的方式进行，而鲁棒的形式化应忠实地反映该扰动，而不是自行恢复为原样或推断出不同的内容。我们构建了一个包含miniF2F和MATH-500上两类扰动的基准，并自动衡量证明自动形式化在全局扰动下正确性的稳定性，以及其输出在局部扰动下的忠实程度。我们评估了七个近期模型，所有模型均对全局扰动敏感，且大多在局部扰动下无法保持忠实。代码和数据可通过 https://github.com/ucr-rai/robust-proof-autoformalization 获取。
查看原文
查看缓存全文

缓存时间: 2026/06/16 11:43 

# 评估 Lean 4 中证明自动形式化的鲁棒性
来源：https://arxiv.org/abs/2606.14867
查看 PDF (https://arxiv.org/pdf/2606.14867)

> **摘要：**证明自动形式化的目标是将用自然语言编写的数学非形式化证明，转换为用 Lean~4 等形式语言编写的形式化证明。已有若干工作开发了基于 LLM 的证明自动形式化模型。然而，现有评估通常侧重于翻译来自精选数据集的、结构良好的非形式化证明。我们认为，一个鲁棒的证明自动形式化器即使对于偏离这些理想情况的非形式化证明，也必须保持忠实性，并提出了首个关于证明自动形式化模型鲁棒性的研究。我们定义了两类扰动，并在每类扰动下评估鲁棒性：全局扰动以不同风格改写非形式化证明，在此情况下形式化结果应保持一致；局部扰动会改变某个值、符号或证明步骤，可能以反事实的方式进行，鲁棒的形式化应忠实反映该扰动，而非自行恢复为原有形式或推断出不同的结果。我们构建了一个包含 miniF2F 和 MATH-500 上两类扰动的基准测试，并自动衡量证明自动形式化在全局扰动下的正确性稳定性，以及其输出在局部扰动下的忠实性。我们评估了七个近期模型，所有模型均对全局扰动敏感，且大多在局部扰动下无法保持忠实性。代码和数据可通过此 https URL (https://github.com/ucr-rai/robust-proof-autoformalization) 获取。

## 提交历史

来自：周兴石 \[查看邮件 (https://arxiv.org/show-email/b3912353/2606.14867)\] **\[v1\]** 2026年6月12日星期五 18:10:21 UTC (246 KB)

相似文章

我们现在有了证明自动化

Hacker News Top

本文讨论了LLMs如何自动生成证明，在如Lean和Rocq这样的依赖类型语言中，通过利用证明无关性并减少手动证明工程的需求，使得形式验证变得更加实用。

大语言模型生成的证明在程序重构下有多稳定？针对可验证代码生成的压力测试

arXiv cs.AI

本文介绍了 RefactorProof，这是一项压力测试，从 VERINA 任务中派生出 458 个经 Lean 认证的重构变体，用于衡量在保持程序行为不变的代码修改下，大语言模型生成的证明是否仍然有效。研究发现，参考证明和专用证明模型（DeepSeek-Prover-V2、Goedel-Prover-V2）均表现出显著的脆弱性，同时指出，大多数失效的证明只需少量修改即可修复。

发现与证明：Lean 4中困难模式自动定理证明的开源智能体框架

arXiv cs.CL

本文介绍了 Discover and Prove (DAP)，一个用于 Lean 4 自动定理证明的开源智能体框架，针对"困难模式"问题进行优化——即在构造形式化证明前必须独立发现答案。该工作发布了新的困难模式基准变体，达到最先进的结果，同时揭示了 LLM 答案准确率（>80%）与形式化证明器成功率（<10%）之间的巨大差距。