评估Lean 4中证明自动形式化的鲁棒性
摘要
本文评估了在全局和局部扰动下，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)
相似文章
我们现在有了证明自动化
本文讨论了LLMs如何自动生成证明，在如Lean和Rocq这样的依赖类型语言中，通过利用证明无关性并减少手动证明工程的需求，使得形式验证变得更加实用。
超越图书馆：一种用于自动形式化研究数学的智能体框架
提出了一种智能体框架，利用通用编码大语言模型将研究级数学自动形式化为Lean 4代码，并在Putnam问题和STOC会议论文上进行了评估。
发现与证明：Lean 4中困难模式自动定理证明的开源智能体框架
本文介绍了 Discover and Prove (DAP)，一个用于 Lean 4 自动定理证明的开源智能体框架，针对"困难模式"问题进行优化——即在构造形式化证明前必须独立发现答案。该工作发布了新的困难模式基准变体，达到最先进的结果，同时揭示了 LLM 答案准确率（>80%）与形式化证明器成功率（<10%）之间的巨大差距。
计算机科学逻辑的理论级自动形式化
引入LCS-Bench，这是一个基于计算机科学逻辑的理论级自动形式化基准，覆盖327个教科书条目、4,076个Lean声明。对14个模型的评估表明该基准具有挑战性，最先进模型在自动形式化任务上仅达到20.1%。
理论级别的自动形式化：从孤立陈述到统一形式知识库
这篇立场论文主张理论级别的自动形式化，即将包括公理、定义和引理在内的整个理论形式化为一致的库，而不是孤立的陈述。它讨论了这种转变的重要性、不同观点、开放挑战，并为形式化研究中的这一转变提出了前进方向。