我们形式化基准测试中的缺陷：Lean定理证明的数据集缺陷和评估失败

# Lean定理证明中的数据集缺陷与评估失败
来源: https://arxiv.org/html/2606.29493

## 形式化基准测试中的缺陷：Lean定理证明中的数据集缺陷与评估失败

###### 摘要

LLM辅助的Lean定理证明基准测试通常被认为天生可靠，因为每个已解决的实例都附带机器验证的证明。然而，内核仅验证证明是否建立了某个*形式化*陈述；它既不验证该陈述是否忠实地编码了预期的非正式问题，也不验证评估框架是否对琐碎或对抗性解法具有鲁棒性。我们审计了五个广泛使用的Lean定理证明基准测试及其分支，利用语料库规模的静态检查器发现了4,833个问题，其中包括398个机器可验证的问题实例，如反例、空洞定理和不合逻辑的公理。我们还记录了语义缺陷，例如缺失前提、问题简化、不完整或不正确的翻译以及Lean特有的规范风险。除了数据集构建，我们还调查了评估阶段的故障模式，并在修正后的子集上表明，缺陷既可能夸大也可能低估报告中的证明器得分。我们提出了一个故障分类体系、一套自动化检查器和面向召回率的语义审计提示，并发布了指导创建形式化数学数据集的标准，使评估更具可重复性和可信度。我们的检查器、审计提示和修正后的数据集快照可在 https://github.com/Shashi456/atp-checkers 获取。

自动化定理证明，形式化数学

## 1 引言

深度学习已快速推进自动化定理证明，模型越来越多地被训练以生成Lean格式的证明。最近的系统如DeepSeek-Prover V2 (Ren et al., 2025 (https://arxiv.org/html/2606.29493#bib.bib27))、Goedel Prover 2 (Lin et al., 2026 (https://arxiv.org/html/2606.29493#bib.bib34)) 和 Kimina Prover (Wang et al., 2025 (https://arxiv.org/html/2606.29493#bib.bib28)) 报告了在广泛使用的基准测试（如 miniF2F 和 ProofNet）上的进展。然而，与其他LLM评估设置类似，当问题陈述定义错误或过时，或评估协议存在漏洞时，基准测试得分可能具有误导性。一种常见的直觉是，Lean基准测试是“自验证”的，因为内核会检查每个证明。这种直觉并不完整。Lean内核仅对一个狭窄的断言提供确定性：给定的证明构件建立了给定的*形式化陈述*。这为形式化声明提供了数学上的确定性，但整体基准测试的可靠性受限于规范准确性和自然语言到Lean翻译的正确性。Lean并不验证形式化陈述是否匹配预期的非正式问题、基准测试是否避免了Lean特有的语义陷阱，或评估协议是否无法被利用。这些差距可能夸大报告的成功率，而不代表更强的证明能力。

表 1：本研究中引用的基准测试（详情见§3）。
参考图注
图 1：形式化基准测试流程及错误可能进入的环节。内核（可信边界）仅证明证明构件建立了*形式化*的Lean陈述。出现三类问题：翻译步骤中的**保真度问题**，证明检查和报告步骤中的**评估漏洞**（鲁棒性），以及贯穿整个流程的**维护问题**（有效性 + 漂移）。表2 (https://arxiv.org/html/2606.29493#S2.T2) 详细列出了每个类别中的具体故障类型。

在本文中，我们审计了五个广泛使用的Lean基准测试及其分支（表1 (https://arxiv.org/html/2606.29493#S1.T1)）。我们分析了基准测试开发流程（第2节 (https://arxiv.org/html/2606.29493#S2)），并提出了一个故障分类体系（第3节 (https://arxiv.org/html/2606.29493#S3)），将形式化阶段的保真度失败、评估阶段的漏洞和维护衰减区分开来。为了将检测扩展到人工审查之外，我们实现了作为Lean 4元程序的自动化静态检查器，并在所有13个基准变体（约10,000个问题）的语料库上运行，发现了4,833个发现，其中398个带有机器可检查的不可证或空洞证书；此外，我们还针对静态分析无法判定的语义不匹配，在一个包含92个问题的标注挑战集上评估了基于LLM的提示，并测量了修正后的陈述如何改变报告的证明器得分（第4节 (https://arxiv.org/html/2606.29493#S4)）。最后，我们提出了发布标准和工具，以强化未来数据集的创建和评估（第5节 (https://arxiv.org/html/2606.29493#S5)）。

## 2 形式化基准测试验证了什么（以及它没有验证什么）

形式化基准测试通常通过一系列步骤从非正式问题改编而来，这些步骤可能破坏基准测试的有效性。图1 (https://arxiv.org/html/2606.29493#S1.F1) 展示了这一流程。我们逐一走过每个阶段，并指出错误可能进入的环节。

##### 步骤 1：非正式问题。流程从**非正式问题**开始，即用自然语言表述的竞赛题、教科书习题或研究猜想。错误可能早已在该阶段出现：原始材料可能包含错误，问题可能表述不当或模棱两可，数学声明可能是错误的。这些是*有效性*问题，任何精细的形式化都无法修复。

##### 步骤 2：形式化。非正式问题随后被**形式化**为Lean陈述。这个翻译步骤是大多数缺陷出现的地方（*保真度*问题）。前提可能被遗漏，域可能翻译错误（例如，用N\mathbb{N}代替Z\mathbb{Z}），或者Lean特有的编码问题可能静默地改变含义或使定理变得空洞。对所得形式化陈述的证明可能在数学上有效，但证明的东西与非正式问题原本意图证明的东西不同。

##### 步骤 3：模型/证明器。模型或自动化证明器接收Lean陈述（加上提示和策略），并尝试生成**证明构件**。

##### 步骤 4：Lean内核。证明构件由Lean内核检查，并输出通过/未通过结果。这是**可信边界**：内核提供数学确定性，即证明构件建立了形式化陈述。然而，模型可能发现Lean环境中的错误，从而生成看似被“接受”但实际上并未经过适当内核验证的证明（*鲁棒性*问题）。

##### 步骤 5：报告指标。最后，评估框架将通过/未通过结果汇总为报告的指标。前一阶段的漏洞可能在不展示真正能力的情况下夸大得分。

##### 内核验证了什么。关键在于，Lean的内核是提供数学确定性的唯一组件，并且它只在这个流程的单个点上运作。图1 (https://arxiv.org/html/2606.29493#S1.F1) 中的可信边界标志着Lean保证的极限：内核左侧和右侧的所有内容都必须通过其他方式验证。它**不**验证形式化陈述是否匹配预期的非正式问题（步骤2），也不验证非正式问题本身是否正确（步骤1），也不验证评估协议和指标报告是否健全（步骤5）。

表 2：Lean定理证明基准测试中的故障分类。
| 类别 | 子类别 | 问题 |
|------|--------|------|
| 保真度 | 规范 | 缺失前提/条件；多余或不正确的约束；不完整或过度简化的规范 |
|  | 形式化 | 目标/前提翻译错误；缺失子目标；空洞的前提 |
|  | 域与定义 | 类型错误；错误的 mathlib 概念；滥用库 API；编码伪影 |
|  | Lean编码 | Nat 减法截断；除以/模零；Int/Nat 强制转换 |
| 评估（鲁棒性） | 证明接受 | 不恰当的公理使用；`native_decide` 捷径；不安全的策略 |
| 维护（有效性 + 漂移） | 衰减 | 版本漂移（Lean 3→4）；依赖腐烂（mathlib API 变化） |
|  | 基准缺陷 | 自然语言陈述缺陷；不可证明的陈述；评估框架漂移 |

我们将这些失败模式组织为三类（图1 (https://arxiv.org/html/2606.29493#S1.F1) 底部；表2 (https://arxiv.org/html/2606.29493#S2.T2)）：**保真度问题**出现在步骤2；**评估漏洞**出现在步骤4-5；**维护问题**贯穿整个流程，包括步骤1中的源错误和随着 mathlib 随时间演变而出现的语义漂移。

## 3 故障分类与代表性失败模式

我们对 miniF2F、ProofNet、FormalMath、CombiBench 和 ProverBench 的审计揭示，基准测试缺陷聚集在需要根本不同干预的类别中。我们根据故障进入基准测试流程的位置（图1 (https://arxiv.org/html/2606.29493#S1.F1)）以及所需的修复措施（表2 (https://arxiv.org/html/2606.29493#S2.T2)）对故障进行组织：
- •**保真度问题**：形式化过程中的问题需要在创建时仔细审查 / Lean编码危险可通过静态分析检测
- •**评估漏洞**：需要更严格的评估框架和修补后的 Lean 版本
- •**维护衰减**：需要版本锁定和主动维护

不能通过添加数据集审查来“修复”内核错误/绕过，也不能通过限制策略来防止缺失前提。分类使得修复措施可操作，通过将故障与适当的干预措施相匹配。我们以审计中发现的代表性缺陷来说明每个类别，并用其（子）类别标记每个示例；更多示例见附录B (https://arxiv.org/html/2606.29493#A2)。

### 3.1 保真度问题

这些故障发生在 Lean 陈述未能忠实地编码预期的非正式问题时。我们区分两种主要失败模式：*.规范错误*遗漏了必要的内容，例如缺失的前提、被丢弃的子目标或未编码的约束，使得陈述有效但比预期*更弱*，因此比原题更容易证明。*.形式化错误*则通过不正确的翻译、错误的量词范围或编码伪影而曲解原题，使得陈述可能变得*不可证明*或证明的是*不同的内容*。两者需要相反修复：规范错误通过*添加*缺失内容来修复，形式化错误通过*修正*编码来修复。

##### 缺失前提。（规范）忘记数学对象的性质可能使问题变得琐碎、空洞或错误。在图2 (https://arxiv.org/html/2606.29493#S3.F2) 中，形式化省略了要求 VV 是有限维的，而该条件在非正式问题中明确陈述且对结果至关重要。

ProofNet – Axler 习题3.8
问题：假设 VV 是有限维的，且 T∈L(V,W)T∈L(V,W)。证明存在 VV 的子空间 UU，使得 U∩nullT={0}U∩nullT={0} 且 rangeT={Tu:u∈U}rangeT={Tu:u∈U}。
[⬇](data:text/plain;base64,dGhlb3JlbSBleGVyY2lzZV8zXzgge0YgViBXIDogVHlwZSp9IFthZGRfY29tbV9ncm91cCBWXQogIFthZGRfY29tbV9ncm91cCBXXSBbZmllbGQgRl0gW21vZHVsZSBGIFZdIFttb2R1bGUgRiBXXQogIChMIDogViDihpLigpdbRl0gVykgOgogIOKIgyBVIDogc3VibW9kdWxlIEYgViwgVSDiipMgTC5rZXIgPSDiiqUg4oinCiAgICBsaW5lYXJfbWFwLnJhbmdlIEwgPSByYW5nZSAoZG9tX3Jlc3RyaWN0IEwgVSkgOj0gc29ycnk=)
theoremP\mathscr{P}exercise\_3\_8 {F V W : Type\*} [add\_comm\_group V] [add\_comm\_group W] [field F] [module F V] [module F W] (L : V →l[F] W) : ∃ U : submodule F V, U ⊓ L.ker = ⊥ ∧ linear\_map.range L = range (dom\_restrict L U) := sorry

图2：缺失前提：Lean 陈述省略了有限维性，而该条件是定理成立所必需的。

##### 不完整翻译。（形式化）问题通常包含多个部分，形式化可能静默地遗漏其中一个。在图3 (https://arxiv.org/html/2606.29493#S3.F3) 中，Lean 陈述捕获了不等式，但省略了“确定等号何时成立”的要求，只编码了原题的一半，使其严格弱于原题。在另一个例子图5 (https://arxiv.org/html/2606.29493#S3.F5) 中，形式化将 uu 作为自由变量，而未指定 u=y−2xu=y-2x。

miniF2F – IMO 1983 问题6
问题：设 a,b,c 是三角形的边长。证明 a^2 b(a-b) + b^2 c(b-c) + c^2 a(c-a) ≥ 0。确定等号何时成立。
[⬇](data:text/plain;base64,dGhlb3JlbSBpbW9fMTk4M19wNiAoYSBiIDog4oqdKSAoaOKCgCA6IDAgPCBhIOKIpyAwIDwgYiDiiqcgMCA8IGMpCiAgKGjigoIgOiBjIDwgYSArIGIpICho4oKDIDogYiA8IGEgKyBjKSAoaOKChCA6IGEgPCBiICsgYykgOgogIDAg4omkIGFeMiAqIGIgKiAoYSAtIGIpICsgYl4yICogYyAqIChiIC0gYykgKwogICAgICBjXjIgKiBhICogKGMgLSBhKSA6PSBzb3JyeQ==)
theoremP\mathscr{P}imo\_1983\_p6 (a b c : R\mathbb{R}) (h0 : 0 < a ∧ 0 < b ∧ 0 < c) (h1 : c < a + b) (h2 : b < a + c) (h3 : a < b + c) : 0 ≤ a^2 * b * (a - b) + b^2 * c * (b - c) + c^2 * a * (c - a) := sorry

图3：不完整规范：形式化中缺少等号情况的确定。

##### 错误的域或类型。（域与定义不匹配）不准确地翻译变量域会改变问题的语义。如果问题陈述“对于所有正整数 n”，使用 (n : N\mathbb{N}) 而没有守卫 (hn : 0 < n) 会包含 n=0。反之，当意图使用 Z\mathbb{Z} 时使用 N\mathbb{N} 可能引入截断错误。

##### Nat 减法和除法风险。（Lean 编码）即使陈述“看起来正确”，Lean 语义可能静默地改变含义：我们在 FormalMath 和 ProverBench 中发现了多个实例，其中 N\mathbb{N} 减法静默地改变了问题语义（附录B (https://arxiv.org/html/2606.29493#A2)）。

##### 定义不匹配。（域与定义不匹配）有时 Lean 编码使用了不正确或过时的 mathlib 概念。这是一个数学表示问题。

##### 空洞前提。（形式化）不正确的翻译可能产生矛盾的前提，使得