半岛【新智元导读】让陶哲轩大神赞不绝口的形式化研究神器Lean，运行LLM的推理却有个bug。最近，加州理工团队解决了这个bug，把80%以上的数学证明步骤，都自动化了！
Lean Copilot，让陶哲轩等众多数学家赞不绝口的这个形式化数学工具，又有超强进化了？
就在刚刚，加州理工教授Anima Anandkumar宣布，团队发布了Lean Copilot论文的扩展版本，并且更新了代码库。
最新实验表明，这个Copilot工具，可以自动化80%以上的数学证明步骤了！这个纪录，比以前的基线倍。
而对此做出巨大贡献的，是一位华人小哥宋沛洋，他是UCSB的荣誉CS本科生，加州理工学院计算+数学科学（CMS）系的SURF研究员。
团队就发布了这个Lean Copilot的工具，希望启动人类和LLM的协作，编写出100%准确的形式化数学证明。
通过这个工具，我们就可以让LLM在Lean中提出证明策略，允许人类以无缝的方式干预和修改。
我们都知道，LLM在做数学和推理任务时，时常会犯错误、产生幻觉，十分不可靠。
像Lean这的定理证明工具，倒是可以形式化证明过程的每一步，但人类编写起Lean，着实很费力。
他前脚刚在博客里预测，26年AI将和搜索、符号数学工具结合，成为数学研究中值得信赖的合著者。
在第97轮对线得出结论半岛，证明示例在没有穷举法的情况下无法求解，证明了结论为P≠NP
这个不太容易看出的bug能被及时捉住，多亏了Lean4。原因是，Lean要求他构建02。由此，Lean无法基于负的0
最后，依赖关系图已经完全被绿色所覆盖，Lean编译器也报告说，这个猜想完全遵循标准公理。
在这个过程中，所有最前线的数学研究者，都在第一时间感受到了AI对于数学研究颠覆力量的直接冲击。
而今天，Lean Copilot的这项研究，让Lean直接变得更强大了。
在这篇论文中，团队基于Lean Copilot构建了一些工具，用于建议证明步骤（策略建议）、完成中间证明目标（证明搜索）和使用LLM选择相关前提（前提选择）。
实验结果也充分表明了，跟Lean中现有的基于规则的证明自动化相比，Lean Copilot在辅助人类自动化定理证明上，是有效的。
Lean Copilot提供了一个通用框架，可以通过CTranslate 2在本地，或者在服务器上运行LLM的推理。
Lean是一个在数学家中很受欢迎的证明助手。如下图所示，Lean中的一个证明，是由一系列被称为策略（tactics）的证明步骤组成。
从整个定理开始作为初始目标，策略反复地将当前的目标转化为更简单的子目标，直到所有目标都被解决。
用户在由VSCode驱动的IDE中交互编写策略，在右边的infoview面板中显示目标。
它会查看每个选项，看它们是否会 1）导致错误；2）结果没有错，但不能完成证明；3）顺利完成证明。
其中，成功完成证明的策略，使用绿色标记（类别3）；没有错误改变证明目标，但未完成证明的策略，使用蓝色标记（类别2）。
注意！当所有列出的策略都属于类别2时，这个信息对于用户来说，可能极有价值。
在这种情况下，剩余目标的信息，可以直接帮助用户选择策略，作为下一个中间证明步骤。
比如，我们在Lean代码中定义了一个定理add_abc，它的初始目标如图3右所示。
而Tactic state字段显示No goal，是因为至少有一个策略建议可以被证明。
此外，因为人类和机器都不能始终如一地产生正确的策略，因此在这个过程中必须回溯、探索不同的替代方案，这个过程就是证明搜索。
当是上面所说的Suggest_tropics，仅能生成当前步骤的策略，不具备搜索多策略证明的能力。
为此，团队将其与基于规则的证明搜索工具aesop结合起来，构建了一个基于LLM的证明搜索工具。
Aesop会将最佳优先搜索作为Lean的策略实施，并且允许用户配置搜索树的扩展方式。
起初，它只有原始目标作为根节点。在每一步中，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文件阅读器。
因此，前提选择的策略可以非常高效地运行，因为前提嵌入可以预先计算，所有后续操作都可以使用上文介绍的库在C++中快速完成。
这里将所有前提所分为两类：可直接在当前环境中使用的前提（范围内前提）和不可直接在当前环境中使用的前提（范围外前提）。
如果已经导入了前提所需的包，则可以轻松使用该前提。如下图6显示了带注释的范围内前提。
下面举个使用「前提选择」的例子，对于图3中的定理add_abc，可以直接在证明中输入select_premises（图8左）。
对于这个简单的定理，可以清晰看到所选的前提确实相关，因为它们都与自然数和加法规则有关。
在这种情况下，所选的4个前提都在当前范围内，这意味着它们的模块已经导入。
如上，便是研究人员通过Lean Copilot构建的三个实用的证明自动化工具，用于策略建议、搜索证明和前提选择。
通过Lean Copilot框架，研究人员凭经验提出了假设——在Lean交互式定理证明（ITP）中进行人机协作是有益的。
因此，在具体实验中，作者主要评估了用于「策略建议」，以及「证明搜索」的证明自动化工具。
总而言之，aesop是当前是一种用于证明搜索，最先进的基于规则的证明自动化工具。
研究人员在两种情况下，验证了基于LLM的搜索证明与aesop相比的有效性：
此外，研究者还将搜索证明与策略建议进行了比较，以证明除了单一策略建议之外，搜索证明体现的优势。
研究Lean Copilot如何有效地帮助人类进行ITP的过程，类似于人类在软件编程中使用Copilot的范式。
也就是说，当我们面对一个目标时，首先会调用Copilot，看其是否可以直接解决问题。
如果不能，我们会进一步简化目标，然后再次尝试Copilot。然后，一直重复上述过程，直至Copilot成功解决剩余目标。
而研究人员便是通过这样的迭代协作范例中，去查看每个证明自动化工具可以自动化多少人力。
当用于辅助人类时， 证明搜索仅需要平均1.02个手动输入策略，这也比aesop（3.62）和策略建议（2.72）更好。
最后，对于每个测试的定理，作者计算了三个工具中每一个可以自动化的证明步骤的百分比。
结果发现，证明搜索可以自动完成定理中约81.2%的证明步骤，明显高于策略建议（48.6%）和aesop（35.2%）。
Lean Copilot中的tactic建议、证明搜索和前提选择，这三个任务在本质上可能看起来不同，但对于用户体验的要求是相似的。
它们都需要足够快速地生成响应，具有适中的计算需求，同时在Lean中运行。
用户之所以有这些要求，是因为Lean本身在大多数情况下都能非常快速地提供环境反馈（比如剩余目标，错误信息，类型信息等）。
如果Lean Copilot需要用户等待很长一段时间，那么人类和AI之间的协作就很难发挥作用。
同样，我们也非常希望满足低计算的需求。因为Lean中的定理证明本身不需要GPU，可以在用户本地的笔记本电脑上运行。
因此，能够在大多数硬件（包括没有GPU的笔记本电脑）上高效运行，对于Lean的用户就非常重要。
因为需要满足快速推理和低计算需求，而且所有流行的高效深度学习框架都是在Python中，团队想到的一个自然的解决方案半岛，就是在Python中托管模型(本地或远程)，然后从Lean向模型发出请求。
然而，这种方法会受到进程间通信的开销的影响，并且它需要用户执行额外的设置步骤，并不适合Lean的传统工作流程。
程序员可以在Lean中声明一个函数，但在c++中实现函数体。实现会被编译到一个共享库中，并动态链接到Lean。
默认情况下，我们采用的是LeanDojo预训练的repver模型。它基于一个编码器-解码器转换器，BVT5，它将输入字符串映射到输出字符串。
Lean Copilot通过将模型包装成一个对字符串操作的c++函数，使其在Lean中可运行，该函数可以通过FFI在精益中调用。
最新论文中的三人团队，也是23年6月开源平台LeanDojo其中的作者。
宋沛洋是加州大学圣巴巴拉分校创意研究学院（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）将符号组件引入机器学习模型，使其更具可解释性、可验证性和数据高效。
目前，他正在研究能够理解和推理数学的人工智能。数学推理是人类智能的一个重要里程碑，它有可能改变科学和工程中的许多重要问题，比如解决偏微分方程和公式验证。
张量分解方法具有极高的并行性和可扩展性，可应用于海量数据。它可以保证收敛到最优解，并对许多概率模型（比如Markov模型）输出一致的估计结果。
原标题：《加州理工华人用AI颠覆数学证明！提速5倍震惊陶哲轩半岛，80%数学步骤全自动化》
