文章摘要
【关 键 词】 自动化数学证明、Lean Copilot、LLM协作、开源工具、数学研究效率
新智元报道了加州理工学院团队在形式化数学工具Lean Copilot方面的最新进展。Lean Copilot是一个自动化数学证明工具，能够辅助数学家进行定理证明。最近，该团队解决了一个关键的bug，使得Lean Copilot能够自动化80%以上的数学证明步骤，这一成果比之前的基线aesop提高了2.3倍。该工具在MIT许可下开源，由UCSB的荣誉CS本科生宋沛洋等人贡献巨大。
Lean Copilot的发布旨在促进人类与LLM（大型语言模型）的协作，以编写100%准确的形式化数学证明。该工具解决了在Lean中运行LLM推理的核心技术挑战，允许LLM在Lean中提出证明策略，同时允许人类无缝地干预和修改。这一进步对于自动化定理证明尤为重要，因为LLM在进行数学和推理任务时可能会犯错误，而数学证明大多是手动推导并需要仔细验证的。
陶哲轩等数学家已经多次证实了LLM作为辅助证明定理的工具的潜力。例如，去年6月，加州理工、英伟达、MIT等机构的学者构建了一个基于开源LLM的定理证明器LeanDojo。同年9月，微软亚洲研究院、北大、北航等机构的研究人员通过97个回合的严格推理，成功让GPT-4得出了“P≠NP”的结论。去年10月，陶哲轩在GPT-4和Copilot的帮助下发现了自己论文中的一个隐藏bug。年底，陶哲轩成功地用AI工具完成了形式化多项式Freiman-Ruzsa猜想的证明过程。
Lean Copilot的研究让Lean变得更强大。团队基于Lean Copilot构建了一些工具，用于建议证明步骤（策略建议）、完成中间证明目标（证明搜索）和使用LLM选择相关前提（前提选择）。实验结果表明，与Lean中现有的基于规则的证明自动化相比，Lean Copilot在辅助人类自动化定理证明上是有效的。
Lean Copilot提供了一个通用框架，可以通过CTranslate 2在本地或服务器上运行LLM的推理。用户可以创建各种自动化证明工具。例如，团队构建了suggest_tropics，一种用LLM生成策略建议的工具。它将当前目标输入LLM，并从LLM获取生成的策略候列表。只有无错误的策略才会显示在视图面板中，成功完成证明的策略用绿色标记，未完成证明但无错误的策略用蓝色标记。用户可以选择是否接受这些建议，或使用它们作为灵感来源制定新策略。
总的来说，Lean Copilot的研究为数学证明自动化领域带来了重大突破，有望极大地提高数学研究的效率和准确性。
原文和模型
【原文链接】 阅读原文 [ 6076字 | 25分钟 ]
【原文作者】 新智元
【摘要模型】 moonshot-v1-32k
【摘要评分】 ★★★★★
