数学证明自动化神器！你能想象数学研究的新速度吗？
|
4月23日消息，近日，加州理工教授Anima Anandkumar宣布，其团队已经发布了Lean Copilot论文的扩展版本，并对代码库进行了更新。该论文中介绍的Copilot工具，现在能够自动化完成80%以上的数学证明步骤，这一成绩较之前的基线aesop提升了2.3倍。该工具在MIT许可下保持开源。 这一重大进展的背后，是一位华人小哥宋沛洋的杰出贡献。他是UCSB的荣誉CS本科生，同时也是加州理工学院计算+数学科学(CMS)系的SURF研究员。网友们对此纷纷表示赞叹，甚至有人戏言，陶哲轩现在的数学研究可以原地加速5倍了。
Lean Copilot工具的推出，旨在启动人类和大型语言模型(LLM)的协作，以编写出100%准确的形式化数学证明。该工具解决了一个核心技术挑战，即在Lean中运行LLM的推理。通过这一工具，LLM可以在Lean中提出证明策略，同时允许人类以无缝的方式进行干预和修改。 形式化数学证明自动化一直是一项艰巨的挑战。尽管LLM在处理数学和推理任务时表现出色，但它们也时常会犯错误，产生不准确的结果。因此，数学证明大多仍需要手动推导和仔细验证。而Lean等定理证明工具，虽然可以形式化证明过程的每一步，但人类编写Lean代码却相当费力。在这种背景下，Lean Copilot的诞生显得尤为重要。 此前，陶哲轩等多位数学家已经多次证实了LLM可以作为辅助人类证明定理的有效工具。而此次Lean Copilot的更新，无疑让这一观点得到了进一步的印证。该工具不仅提高了数学证明的自动化程度，还为数学家们提供了一个更为高效、灵活的研究环境。 据本站了解，Lean Copilot的构建基于一些创新性的工具，如策略建议、证明搜索和前提选择等。这些工具通过LLM生成策略建议，完成中间证明目标，并选择相关前提，从而大大提高了数学证明的效率和准确性。此外，该工具还提供了一个通用框架，使得用户能够创建各种自动化证明工具，进一步推动了数学研究的进步。 |
