加州理工华人用AI颠覆数学证明！提速5倍震惊陶哲轩，80%数学步骤全自动化

加州理工团队解决了形式化研究神器Lean运行LLM推理时的核心技术挑战，可以让LLM在Lean中提出证明策略，允许人类以无缝的方式干预和修改。

Lean Copilot，让陶哲轩等众多数学家赞不绝口的这个形式化数学工具，又有超强进化了？

就在刚刚，加州理工教授Anima Anandkumar宣布，团队发布了Lean Copilot论文的扩展版本，并且更新了代码库。

论文地址：https://arxiv.org/pdf/2404.12534.pdf

最新实验表明，这个Copilot工具，可以自动化80%以上的数学证明步骤了！这个纪录，比以前的基线aesop还要好2.3倍。

并且，和以前一样，它在MIT许可下是开源的。

而对此做出巨大贡献的，是一位华人小哥宋沛洋，他是UCSB的荣誉CS本科生，加州理工学院计算+数学科学（CMS）系的SURF研究员。

网友惊呼：所以，陶哲轩现在的数学研究可以原地加速5倍了？

LLM提出证明策略，人类无缝干预

团队就发布了这个Lean Copilot的工具，希望启动人类和LLM的协作，编写出100%准确的形式化数学证明。

它解决了一个核心技术挑战：在Lean中运行LLM的推理。

通过这个工具，我们就可以让LLM在Lean中提出证明策略，允许人类以无缝的方式干预和修改。

之所以开发这个项目，是因为自动化定理证明在如今仍是一项艰巨的挑战。

我们都知道，LLM在做数学和推理任务时，时常会犯错误、产生幻觉，十分不可靠。

因此，到目前为止，数学证明大多是手动推导的，需要仔细验证。

像Lean这的定理证明工具，倒是可以形式化证明过程的每一步，但人类编写起Lean，着实很费力。

在这种情况下，Lean Copilot的诞生就显得意义重大。

让陶哲轩多次震惊的神器：数学家还不会用就完蛋了

LLM可以作为辅助人类证明定理的工具，这一论点已经被陶哲轩多次证实了。

他前脚刚在博客里预测，26年AI将和搜索、符号数学工具结合，成为数学研究中值得信赖的合著者。

紧接着，佐证他观点的研究就如雨后春笋一般源源不断地冒出来。

去年6月，加州理工、英伟达、MIT等机构的学者，就构建了一个基于开源LLM的定理证明器LeanDojo。

9月，微软亚洲研究院、北大、北航等机构的研究人员，通过97个回合的「苏格拉底式」严格推理，成功让GPT-4得出了「P≠NP」的结论，破解了这个千禧年难题。

在第97轮对话中，GPT-4得出结论，证明示例在没有穷举法的情况下无法求解，证明了结论为P≠NP

去年10月，陶哲轩在GPT-4、Copilot的帮助下，直接发现了自己论文中的一处隐藏bug。

在用Lean4形式化第6页论点的过程中发现，他发现表达式在n=3,k=2时，实际上是发散的。

这个不太容易看出的bug能被及时捉住，多亏了Lean4。原因是，Lean要求他构建0<n−3，但陶哲轩只假设了n>2。由此，Lean无法基于负的0<n−3得到反证。

这一发现直接让陶哲轩瞳孔震惊。

而在去年年底，陶哲轩直接成功地用AI工具，完成了形式化多项式Freiman-Ruzsa猜想证明过程的工作。

最后，依赖关系图已经完全被绿色所覆盖，Lean编译器也报告说，这个猜想完全遵循标准公理。

在这个过程中，所有最前线的数学研究者，都在第一时间感受到了AI对于数学研究颠覆力量的直接冲击。

Lean Coilot，让Lean更好用

而今天，Lean Copilot的这项研究，让Lean直接变得更强大了。

在这篇论文中，团队基于Lean Copilot构建了一些工具，用于建议证明步骤（策略建议）、完成中间证明目标（证明搜索）和使用LLM选择相关前提（前提选择）。

实验结果也充分表明了，跟Lean中现有的基于规则的证明自动化相比，Lean Copilot在辅助人类自动化定理证明上，是有效的。

Lean Copilot提供了一个通用框架，可以通过CTranslate 2在本地，或者在服务器上运行LLM的推理。

通过这个框架，用户就能创建各种自动化证明工具。

Lean是一个在数学家中很受欢迎的证明助手。如下图所示，Lean中的一个证明，是由一系列被称为策略（tactics）的证明步骤组成。

从整个定理开始作为初始目标，策略反复地将当前的目标转化为更简单的子目标，直到所有目标都被解决。

用户在由VSCode驱动的IDE中交互编写策略，在右边的infoview面板中显示目标。

生成策略建议

利用Lean Copilot，团队构建出了suggest_tropics，一种用LLM生成策略建议的工具。

而它本身，也是一种策略。

应用时，它将当前目标输入LLM，并且从LLM获取生成的策略候列表。

它会查看每个选项，看它们是否会 1）导致错误；2）结果没有错，但不能完成证明；3）顺利完成证明。

如果是1），这个策略就会被删除。

只有无错误的策略，才会显示在右边的视图面板中。

其中，成功完成证明的策略，使用绿色标记（类别3）；没有错误改变证明目标，但未完成证明的策略，使用蓝色标记（类别2）。

注意！当所有列出的策略都属于类别2时，这个信息对于用户来说，可能极有价值。

在这种情况下，剩余目标的信息，可以直接帮助用户选择策略，作为下一个中间证明步骤。

看到建议后，用户可以选择是否接受，或使用它们作为灵感来源，制定新策略。

比如，我们在Lean代码中定义了一个定理add_abc，它的初始目标如图3右所示。

当我们输入suggest_tropics时，会在右边看到策略建议。

第一个策略显示为绿色，表示证明已成功完成。

接下来三个建议均为蓝色，这就表明无法直接完成证明，但不会导致错误。

因而，它们很有可能是有效的中间证明步骤！

同时，剩余子目标也显示了出来。

而Tactic state字段显示No goal，是因为至少有一个策略建议可以被证明。

搜索完整证明

此外，因为人类和机器都不能始终如一地产生正确的策略，因此在这个过程中必须回溯、探索不同的替代方案，这个过程就是证明搜索。

当是上面所说的Suggest_tropics，仅能生成当前步骤的策略，不具备搜索多策略证明的能力。

为此，团队将其与基于规则的证明搜索工具aesop结合起来，构建了一个基于LLM的证明搜索工具。

Aesop会将最佳优先搜索作为Lean的策略实施，并且允许用户配置搜索树的扩展方式。

搜索树是由作为节点的目标组成。

起初，它只有原始目标作为根节点。在每一步中，aesop都会选择最有希望的未扩展节点，通过应用策略对其扩展，将生成的节点添加为子节点。

而当aesop找到一条从根源到可轻松解决的目标的路径，就证明搜索成功了！

因此，aesop的性能关键取决于用户是否配置了有效的规则集。

这就可以看出，aesop缺乏灵活性。因此，Search_proof通过在每一步中由suggest_tropics生成的目标相关策略，来增强aesop的规则集，让它变得更加灵活。

对于图3中的原始目标，用户只需输入search_prrof，找到可以解决目标的完整证明，就显示在了信息视图中（图5右）。

可以看到，由于发现了成功的证据，所以剩余的Tactic state是No goals。

选择注释好的前提

此外，定理证明中另一项具有挑战性的重要任务是，找到减少或完成证明的相关前提。

除了源码库和标准库中有大量前提，Lean还有一个大型数学库（Mathlib）。

然而，从所有库中搜索候选前提，极其困难且耗时耗力。

所以许多人都试图，能在Lean，或其他的证明助手中得到辅助，或自动完成这一过程。

在Lean中，最先进的前提选择方法是，直接在Lean中实现的基于随机森林（random forest）的框架。

然而，前提选择任务非常适合检索增强型LLM，即在大模型训练期间训练检索矩阵（前提嵌入），以估计证明目标与候选前提之间的相关性。

给定推理时的证明目标，首先将目标编码成一个向量，然后在前提嵌入和目标向量之间执行矩阵向量乘法。

然后，为了选择前k个前提（其中k可以是一个超参数，决定用户想要返回多少个前提），这时只需返回得分最高的k个前提。

而要在Lean中执行推理任务，除了Lean Copilot提供的快速推理外，还需要一个高效的矩阵乘法库和一个C++的numpy矩阵阅读器。

研究人员采用了来自CTranslate2的矩阵乘法函数，和来自Libnpy的C++快速numpy文件阅读器。

他们再次通过FFI机制，将这些数链接到Lean。

因此，前提选择的策略可以非常高效地运行，因为前提嵌入可以预先计算，所有后续操作都可以使用上文介绍的库在C++中快速完成。

在获得返回的前提后，研究者进一步用有用的信息对其进行注释。

这里将所有前提所分为两类：可直接在当前环境中使用的前提（范围内前提）和不可直接在当前环境中使用的前提（范围外前提）。

这取决于是否导入了所需的软件包。

如果已经导入了前提所需的包，则可以轻松使用该前提。如下图6显示了带注释的范围内前提。

图7所示是带注释的范围外前提。

下面举个使用「前提选择」的例子，对于图3中的定理add_abc，可以直接在证明中输入select_premises（图8左）。

然后，相关前提的列表，就会出现在信息视图中（图8右）。

对于这个简单的定理，可以清晰看到所选的前提确实相关，因为它们都与自然数和加法规则有关。

在这种情况下，所选的4个前提都在当前范围内，这意味着它们的模块已经导入。

如上，便是研究人员通过Lean Copilot构建的三个实用的证明自动化工具，用于策略建议、搜索证明和前提选择。

81.2%的证明步骤，全都自动化了

通过Lean Copilot框架，研究人员凭经验提出了假设——在Lean交互式定理证明（ITP）中进行人机协作是有益的。

由于Lean中的定理证明过程，主要以策略证明为主。

Prev Chapter：Redis 分布式锁 [翻译]

Next Chapter：电子书《The Linux Perf Master》