评估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)

相似文章

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

arXiv cs.CL

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

通过严格步骤级验证评估研究级数学证明

arXiv cs.AI

本文介绍了一种严格的步骤级验证框架，用于评估使用LLM的研究级数学证明，解决了上下文污染问题，并优于全局评估。该方法将重点转向演绎约束，并揭示了剩余错误通常源于学究式过度严谨，暴露了基准中的隐含歧义。

未完成项并非难点：半自动形式化的专家评审案例研究

arXiv cs.AI

本文介绍了一项案例研究，使用大型语言模型（Claude Code）在Lean定理证明器中形式化格罗滕迪克消失定理。研究发现，虽然智能体可以生成经验证的代码，但在定义和API设计方面存在困难，强调了超越单纯编译的专家评审需求。

OProver：一个统一的代理式形式定理证明框架

Hugging Face Daily Papers

OProver是一个统一的框架，用于Lean 4中的代理式形式定理证明，通过使用经过验证的证明和编译器反馈进行训练，迭代地改进证明生成，在多个基准测试中取得了最先进的结果。