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中的定理证明过程，紧张以策略证明为主。

因此，在详细实验中，作者紧张评估了用于「策略建议」，以及「证明搜索」的证明自动化工具。

总而言之，aesop是当前是一种用于证明搜索，最前辈的基于规则的证明自动化工具。

研究职员在两种情形下，验证了基于LLM的搜索证明与aesop比较的有效性：

（1）自主证明定理（LLM独立完成）

（2）帮忙人类进行定理证明（人类与AI协作）

此外，研究者还将搜索证明与策略建议进行了比较，以证明除了单一策略建议之外，搜索证明表示的上风。

研究Lean Copilot如何有效地帮助人类进行ITP的过程，类似于人类在软件编程中利用Copilot的范式。

也便是说，当我们面对一个目标时，首先会调用Copilot，看其是否可以直接办理问题。

如果不能，我们会进一步简化目标，然后再次考试测验Copilot。
然后，一贯重复上述过程，直至Copilot成功办理剩余目标。

而研究职员便是通过这样的迭代协作范例中，去查看每个证明自动化工具可以自动化多少人力。

详细结果，如下表1显示。

证明搜索（search_proof）可以自动证明64%的定理（50个中的32个），明显高于aesop和策略建议（suggest_tropics）。

当用于赞助人类时， 证明搜索仅须要均匀1.02个手动输入策略，这也比aesop（3.62）和策略建议（2.72）更好。

末了，对付每个测试的定理，作者打算了三个工具中每一个可以自动化的证明步骤的百分比。

结果创造，证明搜索可以自动完成定理中约81.2%的证明步骤，明显高于策略建议（48.6%）和aesop（35.2%）。

总之，证明搜索的性能比策略建议，要赶过1.67倍，比基于规则的基线aesop高2.31倍。

通过Copilot在Lean中进行本地LLM推理

Lean Copilot中的tactic建议、证明搜索和条件选择，这三个任务在实质上可能看起来不同，但对付用户体验的哀求是相似的。

它们都须要足够快速地天生相应，具有适中的打算需求，同时在Lean中运行。

用户之以是有这些哀求，是由于Lean本身在大多数情形下都能非常快速地供应环境反馈（比如剩余目标，缺点信息，类型信息等）。

这种快速，跟证明定理的实质是同等的——它须要连贯的推理。

如果Lean Copilot须要用户等待很长一段韶光，那么人类和AI之间的协作就很难发挥浸染。

同样，我们也非常希望知足低打算的需求。
由于Lean中的定理证明本身不须要GPU，可以在用户本地的条记本电脑上运行。

因此，能够在大多数硬件（包括没有GPU的条记本电脑）上高效运行，对付Lean的用户就非常主要。

由于用户在编写证明时，可能无法访问支持CUDA的GPU。

由于须要知足快速推理和低打算需求，而且所有盛行的高效深度学习框架都是在Python中，团队想到的一个自然的办理方案，便是在Python中托管模型(本地或远程)，然后从Lean向模型发出要求。

然而，这种方法会受到进程间通信的开销的影响，并且它须要用户实行额外的设置步骤，并不适宜Lean的传统事情流程。

为了战胜这些问题，Lean Copilot通过外部功能接口(FFI)在Lean中本地运行LLM。

FFI是一种机制，可以用一种措辞编写的程序调用另一种措辞的子程序。

Lean部分用c++实现，可以与c++高效互操作。

程序员可以在Lean中声明一个函数，但在c++中实现函数体。
实现会被编译到一个共享库中，并动态链接到Lean。

默认情形下，我们采取的是LeanDojo预演习的repver模型。
它基于一个编码器-解码器转换器，BVT5，它将输入字符串映射到输出字符串。

Lean Copilot通过将模型包装成一个对字符串操作的c++函数，使其在Lean中可运行，该函数可以通过FFI在精益中调用。

华人作者立大功

最新论文中的三人团队，也是23年6月开源平台LeanDojo个中的作者。

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

宋沛洋是加州大学圣巴巴拉分校创意研究学院（CCS）的打算机科学名誉本科生，导师是Richert Wang和Phill Conrad 。

与此同时，他还是加州理工学院打算与数学科学系（CMS）的SURF研究员，由Anima Anandkumar教授和Kaiyu Yang博士共同辅导。

其余，他还是UC伯克利建筑实验室的研究员，与Tim Sherwood和Dr. Jeremy Lau（谷歌）一起互助。

他的研究兴趣是机器学习（ML），涉及自然措辞处理（NLP）和打算机视觉（CV）等运用领域，以及系统和编程措辞（PL）等根本理论。

宋沛洋最近的研究紧张有两个方向。

一是神经符号推理和人工智能数学（AI4Math），将大模型与交互式定理证明器（ITPs）相结。

另一个是基于时序逻辑的高能效机器学习。

杨凯峪是加州理工学院打算+数学科学（CMS）系的博士后研究员，导师是Anima Anandkumar。

他曾在普林斯顿大学得到了博士学位，导师是Jia Deng，还曾与Olga Russakovsky、陈丹琦一起事情。

他的研究重点是神经符号人工智能，旨在使机器学习能够进行符号推理，希望通过两个方向实现：

（1）将机器学习运用于符号推理任务，如形式逻辑或自然措辞中的数学推理和定理证明；

（2）将符号组件引入机器学习模型，使其更具可阐明性、可验证性和数据高效。

目前，他正在研究能够理解和推理数学的人工智能。
数学推理是人类智能的一个主要里程碑，它有可能改变科学和工程中的许多主要问题，比如办理偏微分方程和公式验证。

Anima Anandkumar现在是加州理工学院打算和数学科学教授。

她的研究兴趣紧张集中在大规模机器学习、非凸优化和高维统计等领域。

特殊是，她一贯在带头开拓和剖析机器学习的张量算法。

张量分解方法具有极高的并行性和可扩展性，可运用于海量数据。
它可以担保收敛到最优解，并对许多概率模型（比如Markov模型）输出同等的估计结果。

更广泛地说，Anandkumar教授一贯在研究加速非凸优化的高效技能。

参考资料：

https://arxiv.org/abs/2404.12534

https://github.com/lean-dojo/LeanCopilot

https://twitter.com/AnimaAnandkumar/status/1782518528098353535