大模型帮陶哲轩解题、证明数学定理：数学成为首个借助AI实现突破的学科？

去年 2 月份，DeepMind 发布了编程辅助利器 AlphaCode。它使用人工智能技术来帮助程序员更快地编写代码，可以自动完成代码、提供代码建议并检查错误，从而提高编程效率。AlphaCode 的问世意味着 AI 在解决现实世界问题的道路上又迈出了一大步。

巧合的是，在同一天，OpenAI 也展示了一项重要成果：他们开发的神经定理证明器成功解出了两道国际奥数题。这一成果是在微软打磨了多年的数学 AI——Lean 的基础上完成的。Lean 于 2013 年推出，数学家可以把数学公式转换成代码，再输入到 Lean 中，让程序来验证定理是否正确。OpenAI 的成功表明，AI 不仅可以用于解决编程等应用学科的问题，还能用来攻克数学等自然学科。

值得注意的是，这并不是 AI 研究者的「一厢情愿」。就像快速接受 AlphaCode 的软件工程师一样，数学家也在越来越频繁地使用 AI，比如获得过菲尔茨奖的陶哲轩。他甚至预言，到 2026 年，AI 将成为数学研究领域可信赖的合著者（co-author）。

与此同时，主攻数学问题的 AI 也在不断发展壮大：一个名为 LeanDojo 的开放平台提供了一套基于大型语言模型的开源定理证明器，消除了在机器学习方法用于定理证明时存在的私有代码、数据和大量计算需求等障碍，为机器学习方法在定理证明领域的研究提供了便利。

「我相信，数学将成为第一门通过人工智能实现重大突破的学科。」在看到这些进展之后，英伟达高级 AI 研究科学家 Jim Fan 在一篇推特中预言说。

除了以上种种进展，Jim Fan 还列出了以下推断依据：

• 数学可以被方便地转化为编码问题，字符串在其中具有重要地位，这使得数学问题可以通过人工智能工具进行处理和分析；

• 与依赖实证结果的学科不同，数学可以通过定理证明器（如 Lean）进行严格验证；

• 与需要依赖物理实验的学科（如生物学和医学）不同，数学不需要进行物理实验，无需依赖尚未完全成熟的机器人技术或实验设备。

在数学与 AI 的这场交叉之旅中，数学家和 AI 研究科学家在共同探索更多可能性。或许，陶哲轩和 Jim Fan 的预言都将加速实现。

在陶哲轩手里，AI 成了数学家的得力助手

「我预计，如果使用得当，到 2026 年，AI 将成为数学研究和许多其他领域值得信赖的合著者。」数学家陶哲轩在前不久的一篇博客中说道。

在众多知名数学家中，陶哲轩是较早接受并发现 ChatGPT 这类 AI 大模型数学价值的一个。早在今年 3 月份 ChatGPT 连鸡兔同笼问题都搞不定的时候，陶哲轩就给予了它肯定的态度，认为这类大模型完全可以胜任一些辅助性质的工作，比如帮数学研究者进行语义搜索、生成一些提示。

 

在这个例子中，陶哲轩提出的问题是：「我在寻找一个关于 xx 的公式。我想这是一个经典的定理，但我不记得名字了。你有什么印象吗？」在这轮问答中，虽然 ChatGPT 没能给出正确答案（库默尔定理），但根据它给出的近似答案（Legendre 公式），我们可以结合传统搜索引擎轻松找到正确答案。

没过多久，OpenAI 就发布了数学能力显著提升的 GPT-4。陶哲轩也一直在尝试解锁这一强大的 AI 工具。在使用过程中，他总结出了一些经验：不要试图让 AI 直接回答数学问题（这样得到的答案八成是废话），而是让它扮演合作者的角色，要求它提供策略建议。按照这种提示方法，陶哲轩在 GPT-4 的帮助下成功解决了一个数学证明题（GPT4 提出了 8 种方法，其中 1 种成功解决了问题）。

陶哲轩利用 GPT-4 解决的问题。

 

陶哲轩为了解决上述证明题提供给 GPT-4 的 Prompt：「你好，我是一名数学教授，我希望你能扮演一位善于提出解题技巧的数学专家合作者。我正试图回答 MathOverflow 中的以下问题……」

 

GPT-4 给出的部分建议。

当然，除了这个证明题外，陶哲轩也在用 GPT-4 完成其他一些工作，包括但不限于：

• 提出问题：他将最近一些数学预印本论文的前几页输入给 GPT-4，并让其生成一些与该论文相关的问题，就像同行提出的问题一样。这可以帮助他更好地进行演讲准备。

• 回答问题：他现在经常使用 GPT-4 来回答随意和模糊的问题，以前他可能会通过精心准备的搜索引擎查询来尝试回答这些问题；

• 辅助写作：他曾经让 GPT-4 给复杂文档提供初稿建议，以辅助写作。

不过，陶哲轩也指出，AI 在数学等学术领域的广泛应用对出版界和教育界来说都是一个考验：当人工智能指导的研究生入门级数学论文可以在不到一天的时间内生成时，研究期刊将如何改变其出版和引用机制？我们的研究生教育方式将如何改变？我们会积极鼓励和训练学生使用这些工具吗？对于这些问题，陶哲轩并没有给出答案。

 

拿下数学定理证明，这项研究或让陶哲轩预言早日成真

一直以来，形式化的定理证明都是机器学习的重要挑战。形式化证明本质上是一种计算机程序，但与 C++ 或 Python 中的传统程序不同，证明的正确性可以用证明助手（如开头提到的 Lean）来验证。定理证明是代码生成的一种特殊形式，在评估上非常严格，没有让模型产生幻觉的空间。

这对目前的大型语言模型（LLM）来说是有挑战性的，尽管 LLM 在代码生成方面表现出了优秀的能力，但在事实性和幻觉性方面还有缺陷。

以往，对于用于定理证明的 LLM 研究面临着许多障碍：比如，现有的基于 LLM 的证明器没有一个是开源的；它们都使用私有的预训练数据，而且计算要求可以达到数千个 GPU 时；此外，有些基础设施是依赖于为分布式训练和与证明助手的互动而定制的，如果没有开源代码，这两者是不可能完全复现的。

在最近的一项研究中，来自加州理工学院、英伟达等机构的研究者在该命题的解决进程上走出了重要一步，提出了开放平台 LeanDojo。

 

论文链接：https://arxiv.org/pdf/2306.15626.pdf 

项目主页：https://leandojo.org/

总体来说，该研究有如下贡献：

• 首先，介绍了从 Lean 中提取数据并与之交互的工具；

• 第二，开发了第一个用于定理证明的检索增强的语言模型 ReProver；

• 第三，为基于学习的定理证明构建了一个具有挑战性的基准，并利用它来验证 ReProver 的有效性；

• 最后，公开发布数据、模型和代码，推动了对定理证明的 LLM 的研究。

LeanDojo 的诞生有望改变当前现状：从开源工具包、模型到基准，LeanDojo 让研究人员能够以适度的计算成本获得最先进的基于 LLM 的证明器。ReProver 不依赖私人数据集，并且可以在一周内在单个 GPU 上完成训练。

研究细节

Lean 是一种编程语言，既可以写传统的程序，也可以写定理和证明。它提供了两个机制：首先，基于具有依赖类型的函数式编程，Lean 为定义程序、数学对象、定理和证明提供了一种统一的语言；第二，Lean 提供了一个策略系统（tactic system），用于半自动地构建机器可检查的证明。

图 2 展示了一个简单的例子，以说明定理是如何在 Lean 中被形式化和证明的：

策略（tactic）的语法是相当灵活的，可以接受参数，也可以组合成复合策略。策略可以看作是特定领域语言（DSL）中的程序。用户可以通过定义新的策略来扩展 DSL。这种离散的、组合的和无界的行为空间使得定理证明对机器学习具有挑战性。

另一个挑战是前提的选择。前提是对证明一个定理有用的现有公理或定义，被用作策略的论据。证明不能使用尚未定义的前提，也不能使用未导入当前文件的前提。通常，前提是来自一个包含数十万个现有定义和定理的大型数学库，这使得人类和机器都很难在生成策略时选择正确的前提。这是定理证明中的一个关键瓶颈，也是研究者希望通过检索增强的 LLM 来解决的。

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 中现有的数学库。