LeanDojo Benchmark
研究者使用 LeanDojo 构建了一个包含 96,962 条从 mathlib 提取的定理 / 证明的基准。该基准是目前最大的以数学为重点的定理证明数据集之一，涵盖了不同的主题，如分析、代数和几何。
与现有的 Lean 数据集不同，LeanDojo Benchmark 还包含了 128,163 个前提的定义，不仅包括定理，还包括可以作为前提的其他定义，例如图 2 中的 gcd。此外，该数据集有 212,787 个策略，其中 126,058 个策略至少有一个前提。在有前提的策略中，前提的平均数量为 2.12。
LeanDojo Benchmark 解决了两项关键问题：
- 前提信息
Lean repos（例如，mathlib 或 lean-liquid）包含人写定理 / 证明的源代码。然而，原始代码并不适合用于训练验证器，它缺乏人类在使用 Lean 时可以获得的运行时信息，例如证明步骤之间的中间状态。
而 LeanDojo 可以从 Lean 的任何 GitHub repo 中提取数据，这些数据包含在原始 Lean 代码中无法直接看到的丰富信息，包括文件依赖关系、抽象语法树（AST）、证明状态、策略和前提。LeanDojo Benchmark 包含细粒度的前提注释（它们在证明中使用的位置和在库中定义的位置），为前提选择提供有价值的数据，也是定理证明的关键瓶颈。
- 具有挑战性的数据分割
研究者发现，将定理随机分成训练 / 测试的常见做法导致了之前论文中高估了性能。LLM 只需在训练期间记住类似定理的证明，就能证明看似困难的定理。
在人类编写的 Lean 代码中，一个常见的惯用语法是为同一数学概念的略微不同的属性设置了一个类似的定理 / 证明块。例如，在图 3 中，最后两个定理不仅看起来相似，而且有相同的证明。如果其中一个在训练中，模型可以通过记忆轻松证明另一个。这种捷径使模型能够证明看似不简单的定理，包括那些需要前提才能证明的定理。
在 LeanDojo Benchmark 中，研究者通过设计具有挑战性的数据分割 novel_premises 来缓解这个问题，它需要测试证明以使用至少一个从未在训练中使用过的前提。
例如，图 3 中的最后两个定理都使用了前提 conj_mul。如果一个定理在 novel_premises 分割的训练集中，另一个也必须在训练中。
以编程方式与 Lean 交互
LeanDojo 的另一个重要功能是以编程方式与 Lean 交互。它把 Lean 变成了一个类似健身房的环境，在这个环境中，证明器可以观察证明状态，运行策略来改变状态，并接收错误或证明完成的反馈。这个环境对于评估 / 部署验证器或通过 RL 训练证明器是不可缺少的。
下面是 LeanDojo 的主要形式，用于通过策略与 Lean 交互。Lean 同样支持不基于策略的其他证明风格，不过 LeanDojo 只支持策略风格的证明。但只要有足够的通用性，任何证明都可以转换为策略风格的证明。
ReProver
随后，研究者使用 LeanDojo Benchmark 来训练和评估了 ReProver。其核心是一个由检索增强的策略生成器（图 1 底部）。
根据当前的证明状态，它可以检索出少数可能有用的前提，并根据状态和检索出的前提的连接情况生成一个策略。在证明定理时，该模型在每一步都会生成多个策略候选者，这些候选者被用于标准的最优搜索算法来寻找证明。
值得注意的是，ReProver 的训练只需要在单 GPU 上花费五天时间（120 个 GPU 时），所需的计算量大大低于之前的方法（1000 小时以上）。
此前的基于 LLM 的证明器都在数学和编码的特定数据集上进行预训练，计算成本很高而且数据集是保密的。相比之下，ReProver 避免特定领域的预训练，建立在「google/byt5-small」之上，这是一个通用的、公开可用的、相对较小的模型检查点。
此外，ReProver 只在人类写的策略上进行了微调，没有辅助数据或通过与 Lean 在线互动收集的数据。虽然这些正交方向是有价值的，但会大大增加方法的复杂性和计算要求。
在评估实验中，ReProver 可以证明 51.4% 的定理，优于直接生成策略而不进行检索的 baseline（47.5%）和另一个使用 GPT-4 以零样本方式生成策略的 baseline（28.8%）。
研究者还在 MiniF2F 和 ProofNet 两个数据集上测试了 ReProver。它可以在 MiniF2F 中证明 26.5% 的定理，在 ProofNet 中证明 13.8% 的定理，这几乎能够媲美强化学习的 SOTA 方法，且训练时使用的资源少得多。
此外，许多定理在 Lean 中没有 ground- truth 证明。而 ReProver 能够证明 65 个目前在 Lean 中没有得到证明的定理，其中 MiniF2F 发现了 33 条证明，ProofNet 中发现了 39 条。研究者表示，ReProver 也可以作为一个有效的工具来增强 Lean 中现有的数学库。
ChatGPT 插件
研究者还构建了一个 LeanDojo ChatGPT 插件，使 ChatGPT 能够通过与 Lean 交互来证明定理。与专门针对定理证明进行微调的 LLM（例如 ReProver）相比，ChatGPT 可以将非形式化数学与形式化证明步骤交织在一起，类似于人类与证明助手的交互方式。它可以解释来自 Lean 的错误消息，并且比专门的证明器更容易操纵。然而，由于搜索和规划方面的弱点，在大多数情况下很难找到正确的证明。
示例如下：
a + b + c = a + c + b
Stirling’s formula
Gauss' summation formula
团队信息
最后来认识一下这篇文章的作者们：
论文一作杨凯峪目前是加州理工学院计算和数学科学 (CMS) 系的博士后研究员 ，此前在普林斯顿大学获得博士学位。
Alex Gu 是麻省理工学院的一名博士生，导师为 Armando Solar-Lezama。此前，他在麻省理工学院获得了学士和硕士学位，拥有 Meta AI Research、Jane Street 和 pony.ai 多家公司的实习经历。
Peiyang Song 目前是加州大学圣巴巴拉分校（UCSB）创意研究学院（CCS）的计算机科学本科生。他的研究工作主要集中在两个方向：1）神经定理证明和自动推理，结合大型语言模型（LLMs）和交互式定理证明器（ITPs）；2）用于能源效率机器学习推理的时间逻辑。
Shixing Yu 目前是美国康奈尔大学计算机科学专业博士生，此前在德州大学奥斯汀分校获硕士学位，本科就读于北京大学信息科学技术学院。
参考链接：
