陶哲轩青睐的证明助手Lean,用上了大模型
现在,数学辅助证明工具都用上了大模型。
「我预计,如果使用得当,到 2026 年,AI 将成为数学研究和许多其他领域值得信赖的合著者。」数学家陶哲轩在之前的一篇博客中说道。陶哲轩这样说了,也这样做了。他最近一直在用 GPT-4、Copilot、Lean 等工具进行数学研究,并且还在 AI 的帮助下发现了自己论文中的一处隐藏 bug。在 Lean 中使用 LLM,加快数学证明速度一直以来,自动化定理证明面临重重困难,传统上,数学证明依赖于手工推导,需要细致的验证。现在随着 AI 的进步,研究者开始借助人工智能进行深入探索,但又免不了出现这种问题,即 LLM 在数学和推理任务中有时不是很靠谱,容易出现错误和幻觉。Lean Copilot 允许用户在 Lean 中使用大型语言模型来自动化证明过程,从而显着加快证明合成的速度,在必要时还允许人类无缝介入和修改,从而在机器和人类智力之间提供平衡的协作。Lean Copilot 允许在 Lean 中使用 LLM 来使证明自动化,如策略建议(suggesting tactics)、前提(premises)以及搜索证明(searching for proofs)。用户可以选择使用 LeanDojo 提供的内置模型,或者导入自己的模型。这些模型可以在本地运行(无论是否有 GPU),或者在云端运行。
简而言之,Lean Copilot 为用户提供了一个灵活的方式,通过引入 LLM 来增强和优化在 Lean 中进行定理证明的过程。Lean Copilot 的主要特点可总结为:LLM 能够提出证明步骤,搜索证明,并从大型数学库中选择有用的引理。Lean Copilot 可作为 Lean 包进行设置,并且能够无缝地在 Lean 的 VS Code 工作流中运行。用户可以使用 LeanDojo 中的内置模型,或者使用自己的模型,这些模型可以在本地(有或没有 GPU)或云端运行。该工具可在各种平台上运行,包括 Linux、macOS 和 Windows WSL。为了使 LLM 更易于 Lean 用户使用,Lean Copilot 希望能够启动一个正反馈循环:证明自动化将带来更好的数据,并最终提高 LLM 在数学上的性能。Lean Copilot 效果展示大家可以根据官方教程配置 Lean Copilot,配置好后就可以进行实验了。项目作者也给出了一些官方示例。
- 免责声明
- 本文所包含的观点仅代表作者个人看法,不代表新火种的观点。在新火种上获取的所有信息均不应被视为投资建议。新火种对本文可能提及或链接的任何项目不表示认可。 交易和投资涉及高风险,读者在采取与本文内容相关的任何行动之前,请务必进行充分的尽职调查。最终的决策应该基于您自己的独立判断。新火种不对因依赖本文观点而产生的任何金钱损失负任何责任。