编辑：编辑部
【新智元导读】让陶哲轩大神赞不绝口的形式化研究神器Lean，运行LLM的推理却有个bug。最近，加州理工团队解决了这个bug，把80%以上的数学证明步骤，都自动化了！
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要求他构建02。由此，Lean无法基于负的0