1. 项目概述：FormalML基准与形式化验证的实践价值

在机器学习理论的研究与工程实践中，一个长期存在的挑战是如何确保我们提出的算法、定理和推导在数学上是绝对严密的。一个看似合理的直觉性证明，往往隐藏着微妙的逻辑漏洞或对边界条件的忽视，这些漏洞在理论论文中可能被忽略，但在实际系统部署时却可能引发灾难性的后果，例如导致优化算法不收敛、泛化边界失效，或概率模型的计算出现偏差。形式化验证，作为一种将数学证明转化为计算机可验证代码的技术，正是解决这一痛点的终极方案。它要求证明的每一步都基于明确的公理和已证引理，由验证器（如Lean、Coq、Isabelle）进行机械检查，从而提供无懈可击的正确性保证。

然而，构建一个复杂的形式化证明本身就是一项极其耗时且需要专业知识的任务。近年来，基于大型语言模型的定理证明器（如DeepSeek-Prover、Goedel-Prover）的出现，为自动化或半自动化完成证明提供了新的可能。但这些模型的能力究竟如何评估？它们在处理机器学习领域特有的、融合了分析、代数和概率的复杂定理时表现怎样？这正是FormalML基准数据集要回答的核心问题。FormalML并非一个普通的代码数据集，它是一个专门为评估定理证明器在“子目标完成”任务上的能力而设计的基准。所谓“子目标完成”，可以理解为在一个大型证明的中间步骤，给定当前的证明状态（即一堆假设和一个待证目标），让模型生成下一步正确的证明策略（Tactic）。这比从头生成整个证明更贴近实际的人机交互证明场景，也更能考验模型对当前数学上下文的理解和推理能力。

简单来说，如果你是一位研究机器学习理论可靠性的学者，或是一位希望将形式化验证引入算法开发流程的工程师，FormalML为你提供了一把标尺和一个训练场。它通过结构化的数据，让你能够量化地比较不同证明器的强弱项，理解它们在面对优化理论中的梯度计算、概率论中的测度论问题时，容易在何处犯错，从而推动更强大、更可靠的AI辅助证明工具的发展。接下来，我将深入拆解这个数据集的设计、核心实验发现以及其中蕴含的实用洞见。

2. FormalML数据集深度解析：从JSON结构到数学语义

要理解一个基准，首先必须吃透它的数据。FormalML的每个数据点，本质上是对一个定理证明过程中某个瞬间的“快照”。这个快照被精心设计为结构化的JSON格式，包含了复原和评估该证明步骤所需的全部信息。我们逐字段拆解其设计意图和背后的数学内涵。

2.1 核心字段的“为什么”

数据集中的每个条目（Entry）都对应一个具体的子目标完成任务。其JSON结构如下，每个字段都不是随意设置的：

{
  "filename": "FoML/FoML/ForMathlib/Probability/Moments.lean",
  "line": 98,
  "tactic_state_before": "string",
  "tactic": "apply aemeasurable_expt_hX",
  "tactic_state_after": "string",
  "goal": "∀ (t' : R), AEStronglyMeasurable (e t') µ",
  "theorem_header": "theorem extracted_formal_statement_27",
  "formal_statement": "theorem ... : ... := sorry",
  "full_formal_statement": "theorem ... {Ω: Type u_1} ... : ... := sorry",
  "retrieval": [{"library": "FoML", "definition": "lemma aemeasurable_expt ..."}]
}

1. filename 与 line ：这是可追溯性的基石。它指明了这个子目标来源于项目代码库中的哪个文件、哪一行。这对于研究者复现问题、理解上下文（例如，这个定理是属于概率论模块还是优化模块）至关重要。它确保了基准的每个任务都根植于真实的、有意义的数学开发项目中。

2. tactic_state_before 与 tactic_state_after ：这是理解“子目标”的关键。在交互式定理证明器（如Lean）中，证明过程是一个状态机。 tactic_state_before 记录了应用策略前的证明状态，通常包括“假设列表”（Context）和“当前目标”（Goal）。 tactic_state_after 则记录了应用正确策略后的新状态。模型的任务就是根据 before 状态，生成能正确过渡到 after 状态的 tactic 。这两个字段共同定义了任务的输入和期望的输出状态。

3. tactic ：这是模型需要预测的目标——一个能推动证明前进的Lean策略。例如 apply aemeasurable_expt_hX 、 rw [h1] 、 linarith 等。评估标准就是看模型生成的策略是否能在Lean中执行，并产生与 tactic_state_after 一致（或等价）的状态。

4. goal 与 formal_statement / full_formal_statement ：这里存在一个精妙的层次设计。

   • goal ：是当前子目标的具体内容，即 tactic_state_before 中需要证明的那个命题。它是模型最直接需要关注的对象。
   • theorem_header 和 formal_statement ：给出了这个子目标所属的顶层定理的名称和语句。这提供了高级别的语义信息。
   • full_formal_statement ：则给出了包含所有隐式参数和完整类型的定理语句。这对于需要深度类型推理或理解复杂依赖关系的模型尤为重要。 实操心得 ：在构建基于此数据集的训练或评估管道时，你需要根据模型的能力决定喂给它哪个层次的语句。对于仅关注局部推理的模型， goal 和 tactic_state_before 可能就够了；但对于需要全局理解的模型， full_formal_statement 能提供关键的类型约束和前提条件。

5. retrieval ：这是FormalML一个极具特色的设计，它模拟了现实证明中“查找相关引理”的过程。该字段提供了一个可能相关的引理列表（来自指定库，如 FoML ），并给出了引理的定义。在提供的例子中，当目标是证明某个函数的“几乎处处强可测性”时，检索系统提供了 aemeasurable_expt 这个引理。 关键点在于 ：这个引理可能有用，也可能无关，甚至可能误导。模型需要具备判断和选择的能力。这直接评估了模型在知识检索和知识应用上的综合能力，而不仅仅是代码生成。

2.2 一个实例的“庖丁解牛”

让我们结合输入材料中的例子（ FoML/FoML/ForMathlib/Probability/Moments.lean ，第98行）来具体感受一下。

• 场景 ：我们正在证明一个关于随机变量矩（Moments）的概率论定理。
• 当前目标 ( goal ) ： ∀ (t' : R), AEStronglyMeasurable (e t') µ 。意思是：对于所有实数 t' ，函数 e t' 关于测度 µ 是“几乎处处强可测的”。
• 证明状态 ( tactic_state_before ) ：假设中包含了 hX : AEMeasurable X µ （X关于µ几乎处处可测）以及 h : ∀m (ω : Ω) ∂µ, X ω ∈ Set.Icc a b （X的值域被限制在区间[a, b]内）。
• 正确策略 ( tactic ) ： apply aemeasurable_expt_hX 。
• 检索到的引理 ( retrieval[0].definition ) ： lemma aemeasurable_expt (X : Ω → R) (t : R) (hX : AEMeasurable X µ) : AEStronglyMeasurable (fun ω ↦ exp(t • X ω)) µ 。

推理链条分析 ：

1. 目标匹配 ：我们的目标是 AEStronglyMeasurable (e t') µ 。检索到的引理结论是 AEStronglyMeasurable (fun ω ↦ exp(t • X ω)) µ 。如果我们能证明 e t' 在形式上就是 fun ω ↦ exp(t' • X ω) ，那么应用 ( apply ) 这个引理就能把当前目标转化为证明该引理的前提条件。
2. 定义追溯 ：根据 full_formal_statement ， e 被定义为 fun t ω => exp(t • X ω) 。因此 e t' 就是 fun ω => exp(t' • X ω) ，与引理结���中的函数形态完全匹配。
3. 前提检查 ：引理需要两个前提： (t : R) 和 (hX : AEMeasurable X µ) 。第一个前提 t' 是现成的（来自目标中的全称量词）。第二个前提 hX 正好在我们的假设列表中。因此， apply aemeasurable_expt_hX 是一个完美匹配的策略，它直接利用现有假设，通过应用已知引理一步完成证明。

这个例子清晰地展示了FormalML任务的设计：它要求模型不仅会写代码，更要理解数学对象之间的逻辑关系，并能在给定的上下文中（包括可用的引理）选择正确的推理路径。

3. 核心实验与性能评估：模型表现揭示了什么？

FormalML论文的核心贡献之一，是提供了对当前主流定理证明器在子目标完成任务上的系统性评估。输入材料中的表格和案例分析提供了非常丰富的洞察。我们重点解读两个维度：错误类型分析和检索的影响。

3.1 错误类型分析：模型“死法”大不同

论文将模型的输出分为三类，这个分类极具实践指导意义：

1. has_error ：生成的Lean代码存在语法错误、类型错误或无法通过Lean编译器检查的执行错误。这反映了模型的“语法/基础语义”能力不足。
2. is_valid_with_sorry ：代码能通过Lean检查，但其中包含了 sorry 策略。 sorry 在Lean中相当于“跳过此证明”，是证明未完成的占位符。这表示模型生成了一个结构正确但内容空洞的“证明框架”，它知道这里该有个证明，但不知道具体是什么。
3. is_valid_no_sorry ：生成的代码不仅语法正确，而且确实完成了子目标的证明，不含任何 sorry 。这是唯一完全成功的输出。

从输入材料的Table 5中，我们可以提炼出几个关键结论：

模型 \ 表现	趋势解读
DeepSeek-Prover-V2 (CoT)	在Pass@16和Pass@32设置下，其 has_error 率（优化~63%，概率~62%）显著低于其他模型，而 is_valid_with_sorry 率（~10.7%， ~7.6%）最高。这表明CoT（思维链）提示极大地提升了模型生成代码的“语法正确性”和“结构合理性”。模型更倾向于生成一个逻辑通顺但可能用 sorry 跳过最难部分的证明草图，而不是产出根本无法编译的垃圾代码。这是一种“保守但稳健”的策略。
Goedel-Prover	呈现出几乎相反的特征： has_error 率极高（~90%， ~85%），而 is_valid_with_sorry 率几乎为0。这说明该模型要么生成完全正确的证明，要么就生成完全错误的代码，很少妥协。这可能意味着其训练或推理机制更“激进”，试图直接生成完整证明步骤，但一旦推理偏差，就会产生无法通过基础检查的代码。
DeepSeek-Prover-V1.5	表现介于两者之间，但更接近Goedel-Prover，错误率高， sorry 率低。这或许体现了从V1.5到V2（引入CoT）的巨大改进。

给实践者的启示 ：如果你在项目中集成了一个定理证明模型，你需要根据场景选择模型。对于需要快速探索证明思路、生成证明大纲的场景，DeepSeek-Prover-V2 (CoT) 可能更有帮助，因为它能给出更多结构正确的“半成品”，人类专家可以在此基础上填补 sorry 。而对于需要全自动、高置信度完成简单子目标的场景，可能需要更关注 is_valid_no_sorry 率高的模型，或者对高 sorry 率模型的输出进行后处理。

3.2 检索的“双刃剑”效应：帮助还是干扰？

输入材料中的案例研究（E.1 Cases of Retrieval）揭示了一个反直觉但非常重要的现象： 提供检索到的相关前提（Retrieval），有时反而会降低模型的证明成功率。

• 问题 ：一个关于Lasso优化问题中范数不等式（ |λ * ∑|y_i| - λ * ∑|x_i|| ≤ ε ）的定理。
• 无检索时（STP模型） ：模型给出了一个简洁而正确的证明，核心是 cases‘ 结合 linarith 进行情况分析和线性算术计算。
• 有检索时 ：系统提供了一系列可能相关的定理，如 norm_one_proximal , inner_add_left , mul_pos , mul_sub 等。然而，模型被这些额外的、可能无关甚至干扰的信息所误导，尝试构建一个复杂得多的证明，涉及 have h0 , have h1 , calc 块和 field_simp 等策略，最终这个冗长的证明很可能是错误的（因为材料中未标记其正确，且逻辑显得迂回）。

这个案例的教训是深刻的 ：

1. 检索不是银弹 ：单纯的语义相似性检索（例如，都包含“范数”、“乘法”、“不等式”等关键词）可能会返回大量相关但非必要的引理，淹没核心的、简单的证明思路。
2. 模型抗干扰能力 ：这考验了模型在“信息过载”环境下的聚焦和判断能力。一个强大的定理证明模型，应该能像人类专家一样，快速识别出哪些引理是核心的，哪些是冗余的，甚至能识别出某些引理在当前语境下根本不适用。
3. 评估指标需细化 ：这提示我们，未来的基准或评估中，可能需要加入“检索质量”或“模型在检索干扰下的鲁棒性”作为新的维度。一个模型在无检索时表现良好，但在有（可能嘈杂的）检索时表现下降，说明其推理的稳健性有待加强。

3.3 长思维链（Long-CoT）的冗余与幻觉问题

材料E.2部分展示了DeepSeek-Prover-V2 (CoT)模型在一个简单等式证明上产生的冗长输出。目标很简单：利用假设 aa + bb = 1 ，证明一个等式两边因 (aa+bb) 被替换为 1 而成立。一个人类专家可能直接用 rw [abh] （重写假设）或 linarith 一步解决。

然而，模型的CoT输出包含了大量冗余的文本分析、分步计划、 have 语句的声明（甚至包含未完成的 sorry ），以及复杂的 calc 块。最终它给出的“完整证明”虽然正确，但绕了一个大圈子。

这暴露了当前LLM在定理证明中的两个典型问题：

1. 过度思考（Overthinking） ：模型被设计成“展示思考过程”，但有时它会为简单的步骤生成不必要的复杂解释，这增加了输出长度和解析成本，也可能在复杂链条中引入更多出错点。
2. 规划与执行的割裂 ：模型生成的“详细计划”和最终的Lean代码有时并不完全对应。计划中可能提到使用某个引理，但代码中并未体现。这说明模型的“说”和“做”可能不一致。

实操建议 ：在使用CoT模型进行辅助证明时，不应全盘接受其生成的文本计划，而应重点关注其最终产出的Lean代码块。同时，可以尝试通过提示工程（Prompt Engineering）来约束其输出，例如要求“给出最简洁的证明”，或“直接输出Lean代码，无需解释”。

4. 构建与使用FormalML基准的实践指南

如果你是一名研究者或开发者，想要复现、扩展或基于FormalML进行工作，以下是一些从工程角度出发的实操要点和避坑指南。

4.1 环境搭建与数据预处理

核心工具链 ：

• Lean 4 ：FormalML基于Lean 4。首先需要安装Lean 4及其包管理器 lake 。建议使用版本管理器（如 elan ）来管理Lean版本，确保与论文中实验环境的一致性。
• 项目依赖 ：FormalML数据集通常依赖于特定的数学库（如 Mathlib 的某个版本，以及项目自有的 FoML 库）。克隆代��库后，第一件事是运行 lake exe cache get 来获取编译缓存，否则从头编译 Mathlib 可能耗时数小时。
• 数据加载 ：数据集以JSON格式存储。使用Python处理时，除了标准的 json 库，更推荐使用 pydantic 库来定义数据模型（Data Model）。这能提供自动化的类型检查和数据验证，避免因字段名拼写错误或类型不匹配导致的隐蔽Bug。

from pydantic import BaseModel
from typing import List, Optional

class RetrievalEntry(BaseModel):
    library: str
    definition: str

class FormalMLEntry(BaseModel):
    filename: str
    line: int
    tactic_state_before: str
    tactic: str
    tactic_state_after: str
    goal: str
    theorem_header: str
    formal_statement: str
    full_formal_statement: str
    retrieval: Optional[List[RetrievalEntry]] = None

# 示例加载
import json
with open('formalml_dataset.json', 'r') as f:
    data = json.load(f)
entries = [FormalMLEntry(**item) for item in data]

注意事项 ：Lean的证明状态（ tactic_state_before/after ）是纯文本，但包含了丰富的结构信息（如 ⊢ 符号分隔目标和假设）。在将其输入模型前，可能需要进行简单的清洗或格式化，但要注意保持其语义完整性。一种常见做法是将其与 theorem_header 或 goal 字段拼接，作为模型的输入上下文。

4.2 评估流程的实现

评估的核心是“执行模型生成的策略，并检查证明状态是否与预期匹配”。这个过程需要与Lean交互。

推荐方案 ：使用Lean的 --run 模式或编写一个小的Lean脚本来执行。更稳健的做法是利用Lean的服务器模式（LSP），但复杂度较高。一个简单的本地评估流程可以如下：

1. 模板生成 ：为每个数据点创建一个临时的Lean文件（ .lean ）。
2. 文件内容 ：文件需要导入必要的库（ Mathlib 等），然后复现证明的上下文。通常需要构造一个 theorem ，其证明体中先通过一系列 have 和 let 还原 tactic_state_before 中的假设，然后使用模型预测的 tactic ，最后尝试通过 done 或检查目标是否被解决来验证。
3. 执行与检查 ：使用 lake exec lean 命令运行该临时文件。捕获输出：
   • 成功（无错误） ：检查是否产生了新的目标？是否与 tactic_state_after 等价？这里“等价”的判断可能需要比较目标状态的规范化形式，因为Lean可能会对表达式进行 α 等价转换。
   • 失败 ：解析Lean的错误信息，将其归类为 has_error 。
4. sorry 检测 ：在成功执行的情况下，还需要扫描生成的代码中是否包含 sorry 关键字，以区分 is_valid_with_sorry 和 is_valid_no_sorry 。

避坑指南 ：

• 环境隔离 ：每个评估应在干净的临时目录中进行，避免文件残留或缓存干扰。
• 超时控制 ：对Lean进程设置严格的超时（如30秒），防止因模型生成死循环或极其复杂的策略导致评估进程挂起。
• 错误信息分类 ：Lean的错误信息多样，可以粗略分为：语法错误、未知标识符、类型不匹配、策略失败等。进行更细粒度的错误分析有助于诊断模型的弱点。

4.3 基于FormalML进行模型训练或微调

如果你想用FormalML数据训练自己的定理证明模型，有几个关键决策点：

1. 输入输出格式 ：
   • 输入 ：通常将 tactic_state_before 、 goal 和 retrieval[i].definition 拼接作为提示（Prompt）。是否加入 full_formal_statement 取决于模型容量和任务设计。
   • 输出 ：直接生成 tactic 字符串。也可以尝试生成更结构化的输出，如策略序列或带置信度的策略列表。
2. 数据拆分 ：务必按照论文或原始数据集的指示进行训练/验证/测试拆分，避免数据泄露。机器学习领域的定理和优化领域的定理在风格和知识上有差异，确保拆分时考虑领域平衡。
3. 负样本与困难样本 ：FormalML提供的是正例（正确的策略）。为了提升模型的鲁棒性，可以考虑通过以下方式构造负样本：
   • 随机替换 ：从其他样本中随机抽取一个 tactic 作为负例。
   • 相似干扰 ：使用语法正确但语义错误的策略（如 apply 一个类型不匹配的引理）。
   • 利用错误输出 ：收集模型在评估中产生的 has_error 输出作为负样本。
4. 使用检索信息 ：如何将 retrieval 字段有效融入模型是一个研究点。可以将其作为额外的上下文输入，也可以训练一个单独的检索评分模块，让模型学会给检索到的引理打分，选择最相关的一个。

5. 常见问题与排查技巧实录

在实际操作中，无论是运行FormalML评估还是基于其开发，都会遇到一些典型问题。这里记录一些我踩过的坑和解决思路。

5.1 Lean环境与依赖问题

• 问题 ：克隆代码后， lake build 失败，提示找不到 Mathlib 的某个版本或依赖冲突。
• 排查 ：
  1. 首先检查 lakefile.lean 或 lakefile.toml 中的依赖声明。FormalML项目通常会锁定 Mathlib 的某个commit hash。
  2. 运行 lake update 来更新依赖。
  3. 清理缓存并重试： rm -rf .lake build 然后 lake build 。
  4. 最根本的解决办法是使用论文作者提供的Docker镜像（如果有），确保环境完全一致。
• 心得 ：形式化验证项目对依赖版本极其敏感。强烈建议使用 elan 固定Lean版本，并使用项目锁定的 Mathlib commit，不要随意升级。

5.2 评估脚本中的“等价性”判断难题

• 问题 ：模型生成的策略执行后，证明状态改变了，但如何自动判断它是否与标准的 tactic_state_after “等价”？字符串直接比较往往失败，因为变量名可能α转换（重命名），表达式可能以不同但数学等价的形式呈现。
• 解决方案 ：
  1. 规范化（Normalization） ：使用Lean的 #eval 或 rfl （自反性）策略。可以编写一个Lean脚本，在新的证明状态下，尝试证明当前目标与标准目标“在逻辑上等价”。例如，使用 have h : current_goal = standard_goal := by ... 然后尝试用 rfl 或 simp 证明。
  2. 目标数量检查 ：首先检查策略执行后，剩余的子目标数量是否与标准状态一致。
  3. 保守策略 ：在学术评估中，有时采用更保守但可靠的方法：不直接比较状态，而是看模型生成的策略是否能够成功“闭合”当前目标（即生成 no goals 状态）。如果标准策略能做到，模型策略也能做到，则认为成功。这需要将评估嵌入到一个更大的、能自动尝试完成证明的框架中。
• 实操技巧 ：对于初步研究和原型开发，可以暂时采用“目标闭合”法。对于需要发表精确定量结果的正式评估，则需要实现一个更健壮的、基于Lean表达式树比对或等价性证明的检查器。

5.3 模型生成策略的“似是而非”问题

• 现象 ：模型生成了一个策略（如 rw [h] ），语法完全正确，在Lean中也能执行，没有错误，但证明状态并没有向目标推进，或者引入了一个无法证明的新目标。这不会被归类为 has_error ，但也不是真正的成功。
• 分析 ：这属于“语义错误”而非“语法错误”。例如， h 可能是一个等式，但 rw [h] 的方向反了，或者 h 的结论形式与当前目标不匹配， rw 只做了部分改写。
• 应对 ：严格的评估需要检测这种情况。可以在执行模型策略后，不仅检查有无错误，还检查证明状态是否“真正进步了”。一个简单的启发式方法是：检查当前首要目标的“复杂度”（如表达式的深度或大小）是否比之前显著减少？或者，可以尝试再执行一步标准策略，看能否快速闭合剩余目标？这需要设计更复杂的评估逻辑。

5.4 处理大规模评估的性能瓶颈

• 问题 ：FormalML数据集可能包含数千个样本。对每个样本启动一个独立的Lean进程进行验证，耗时极长。
• 优化方案 ：
  1. 并行化 ：使用Python的 multiprocessing 或 concurrent.futures 库并行运行多个Lean评估进程。注意控制并发数，避免耗尽内存。
  2. 进程复用 ：研究使用Lean的LSP（语言服务器协议）模式，维持一个长期运行的Lean服务器进程，通过IPC（进程间通信）发送评估请求，避免频繁的进程启动开销。但这需要处理服务器状态管理和隔离问题。
  3. 抽样评估 ：在开发迭代阶段，可以先在一个小的、有代表性的测试集（如每个难度等级、每个领域抽50个）上进行快速评估，待模型稳定后再进行全量评估。
• 硬件建议 ：评估是CPU密集型任务（Lean类型检查）。使用多核CPU的机器比单纯追求高GPU性能的机器更有效。确保有足够的内存（≥32GB），因为 Mathlib 的加载非常占用内存。

FormalML基准的出现，标志着机器学习形式化验证评估向标准化、精细化迈出了重要一步。它不仅仅是一组数据，更是一个研究范式的体现：将定理证明这个高度智能的任务，分解为可测量、可比较的子任务。通过深入分析模型在其中的表现，我们不仅能对现有模型的能力有更清晰的认识，更能为下一代定理证明AI的设计指明方向——例如，如何更好地整合检索与推理，如何生成更简洁可靠的证明，以及如何提升对复杂数学结构的理解能力。对于身处这个交叉领域的研究者和工程师而言，熟练掌握这个基准，意味着握有了评估和推进自己工作的关键工具。