大语言模型助力数学研究：定理证明的新篇章

文章主题：自然语言处理, 大语言模型, 数学定理证明, 人工智能

用大语言模型定理证明，加州理工华人一作最新研究可能改变数学未来。

大语言模型，可以用来证明数学定理了！

著名数学天才陶哲轩曾在一篇博客中预测，到2026年，人工智能将能够与搜索和符号数学工具相互协作，成为数学研究中的重要合作伙伴。如今，这个预测已经变成了现实。一些来自加州理工学院、英伟达以及麻省理工学院等知名学府的学者们，共同打造了一个基于开源LLM（大型语言模型）的定理证明器。

而这篇论文，或许将改变数学的未来。

项目地址：https://leandojo.org/

在这篇文章中，研究者们介绍了一个名为 LeanDojo 的开源平台。这个平台提供了丰富的工具包、基准和模型，旨在为定理证明提供一个交互式的环境，尤其是针对语言模型（LLM）。通过这些工具和资源，研究人员和学生们可以更加便捷地进行定理证明的研究和探索。

数学：首个见证 AI 重大突破的领域

论文一作杨凯峪表示，公式证明是计算机程序，其正确性可以被验证。

最重要的是，这项研究为解决 LLM，在事实性和幻觉方面的缺陷开辟了一条新途径。

因为，定理证明是一种具有严格评价的代码生成形式，根本没有让模型产生幻觉的空间。

我很荣幸地看到这一重要时刻的到来。英伟达首席科学家Jim Fan深情地转发了这个消息：数学，这个 initially 用来描述自然界的语言，如今很可能成为第一个实现人工智能重大突破的学科。

他建议，每个人都应该阅读数学家陶哲轩的博客。在这个博客里，陶哲轩预测到，到了2026年，人工智能将会与搜索和符号数学工具紧密结合，从而成为数学研究中的重要合作伙伴。

为什么 AI 的第一个重大突破会在数学？理由如下——

数学可以方便地表示为编码问题

可以通过 Lean 这样的定理证明器进行严格的验证，而不是依赖经验结果

不需要像生物学和医学这样的物理实验，机器人技术的发展还有待进步

GPT 擅长编码，Lean 是公式数学的编码语言，还不会出现幻觉。

人工智能数学 co-pilots 来了。发现新定理的全自动人工智能数学家就是下一个！

有网友称，所以陶哲轩可以被解雇，很容易被取代，不是吗？

LeanDojo 究竟有多强？

LeanDojo：定理证明交互式环境

机器学习，特别是大型语言模型，在使用证明助手 Lean 证明公式定理方面显示出广阔的前景。

LeanDojo 其主要特点包括：

提供了用于数据提取和与 Lean 交互的工具

证明中的前提（现有定理）的细粒度标注：使用和定义这些前提的位置

LeanDojo基准测试得出的结果是:在97000个由人类编写的定理/证明中,有97000个定理/证明被成功地用于训练机器学习模型来验证定理。这个结果表明,使用人类编写的定理/证明作为训练数据可以有效地提高机器学习模型的准确性和可靠性。

ReProver是一款针对LLM的检索增强证明器，专注于提升前提选择的效率。作为一款创新的证明工具，它致力于加强搜索过程，从而提高整体推理效果。

Lean 是一个在数学家中非常受欢迎的证明助手工具。

研究团队针对 Lean 进行了加工和改进，开发出了 LeanDojo。它可以从 Lean 中提炼出人类撰写的证明过程，形成一个数据集。

从而可以通过与 Lean 的证明环境互动，使得这个训练出来的模型可以用来证明定理。

LeanDojo 的工作流程和原理大致如下图所示：

顶部右边：

LeanDojo从Lean中提取证明到数据库中，用来训练机器学习模型。

这个流程也可以通过和Lean的证明环境进行交互后让训练好的模型来证明定理。

顶部左边：这是Lean定理

的证明树。在这里gcd是最大公约数的意思。

在证明定理时，我们从原始定理作为初始状态（根）开始，并重复应用策略（边）将状态分解为更简单的子状态，直到所有状态都得到解决（叶节点处）。

策略可能依赖于大型数学库中定义的诸如 mod_self 和 gcd_zero_left 之类的前提。

例如，mod_self 是证明中用于简化目标的现有定理：

底部：只要给定一个状态，Reprover模型就能从数学库中检索前提，这些前提与状态连接起来，输入到一个作为编码器和解码器的Transformer中以生成下一个策略。 Benchmarks 基准测试

LeanDojo Benchmark：从 mathlib 中提取的 96,962 个定理 / 证明、212,787 个策略和 128,163 个前提。

LeanDojo Benchmark 4：从 mathlib4 中提取的 91,766 个定理 / 证明和 177,349 个策略。前提信息将很快提供。

LeanDojo 可以从 Lean 中的任何 GitHub 存储库中提取数据（支持 Lean 3 和 Lean 4）。这些数据包含原始 Lean 代码中不直接可见的丰富信息，包括文件依赖项、抽象语法树 (AST)、证明状态、策略和前提。

主要特征 1：前提信息

LeanDojo Benchmark 包含前提的细粒度标注（在证明中使用它们以及在库中定义它们），为前提选择（定理证明中的关键瓶颈）提供有价值的数据。

主要特征 2：具有挑战性的数据分割

将定理随机分割到训练 / 测试中会导致高估模型性能。大语言模型可以通过在训练期间记住类似定理的证明，就可以证明看似困难的定理。

研究人员通过设计具有挑战性的数据分割来缓解这个问题，要求模型基于从未在训练中使用的创新性前提来泛化到定理。

与 Lean 产生交互

如上图所示，LeanDojo 将 Lean 变成了一个类似体育馆的环境，数学家可以在其中观察证明状态，运行策略来改变状态，并接收有关错误或证明完成的反馈。

这样的一个环境对于评估 / 部署证明器或通过强化学习进行训练是必不可少的。

实验评估

研究人员使用 LeanDojo Benchmark 来训练和评估 ReProver。

下图展示了 10 分钟内证明的定理的百分比。每一列代表不同的数据分割。

ReProver 的性能优于 Lean 内置的证明自动化策略（tidy），提供了一个无需检索即可直接生成策略的测试基准。

研究人员采用的另一个基准是使用 GPT-4 以零样本方式生成策略。

发现新证明 & 发现公式错误

研究人员采用在 miniF2F 和 FroofNet 中的定理来评估 ReProver。

他们发现 miniF2F 中有 33 个证明，ProffNet 中有 39 个证明在 Lean 中是不存在的。

与此同时，最新研究还发现了 ProofNet 定理陈述公式中的多个错误。

详见：https://github.com/zhangir-azerbayev/ProofNet/pull/14

ChatGPT 插件

研究人员还构建了一个 LeanDojo 的 ChatGPT 插件，使 ChatGPT 能够通过与 Lean 交互来证明定理。

他们具体在三种数学公式上进行了尝试，包括 a+b+c=a+c+b，斯特林公式（Stirlings formula），以及高斯求和公式（Gauss summation formula）。

结果发现，专业的定力证明 LLM（ReProver）相比，ChatGPT 可以将非正式数学与正式证明步骤交叉在一起，类似人类与证明助手的交互方式。

它甚至可以解释 Lean 的错误信息，并且比专业证明器更容易控制（通过提示工程）。

然而，由于搜索和规划方面的弱点，它在多数情况下很难找到正确的证明。

具体演示如下：

a+b+c=a+c+b

关闭

观看更多

正在加载

退出全屏

视频加载失败，请刷新页面再试

刷新

视频详情

斯特林公式（Stirling’s formula）

关闭

观看更多

正在加载

退出全屏

视频加载失败，请刷新页面再试

刷新

视频详情

高斯求和公式（Gauss summation formula）

关闭

观看更多

正在加载

退出全屏

视频加载失败，请刷新页面再试

刷新

视频详情

GitHub 上，开发者给出使用演示方法示例：

插件安装成功后，你可以让 ChatGPT 证明定理，只需告诉它定理的名称和定义。比如：

I want you to prove a theorem in Lean. The theorems name is hello_world, and it is defined in the file src/example.lean in https://github.com/yangky11/lean-example. Please explain the theorem to me, lay out a high-level proof plan, and then try various tactics to prove the theorem.

初始化证明搜索可能需要一些时间。

你可以用提示来控制 ChatGPT 的行为。例如，在尝试任何测术之前，你可以要求它「产生一个高级证明计划」。

网友评论