2023/12/18 15:08

陶哲轩青睐的证明助手Lean，用上了大模型

现在，数学辅助证明工具都用上了大模型。

「我预计，如果使用得当，到 2026 年，AI 将成为数学研究和许多其他领域值得信赖的合著者。」数学家陶哲轩在之前的一篇博客中说道。

陶哲轩这样说了，也这样做了。

他最近一直在用 GPT-4、Copilot、Lean 等工具进行数学研究，并且还在 AI 的帮助下发现了自己论文中的一处隐藏 bug。

不仅如此，前几天，陶哲轩表示：对多项式 Freiman-Ruzsa 猜想（PFR）的证明进行形式化的 Lean4 项目成功完成，并且耗时仅三周时间。Lean 编译器也报告该猜想符合标准公理，可以说这是计算机和 AI 辅助证明的一项巨大成功。

关于上述研究的更多内容，感兴趣的读者可以参考《陶哲轩用 AI 形式化的证明究竟是什么？一文看懂 PFR 猜想的前世今生》。

看到这，细心的读者可能已经发现了端倪，陶大神在进行数学研究时，多次都提到过 Lean。简单来讲，Lean 是一种可帮助数学家验证定理的编程语言，用户可以在其中编写和验证证明。相比初代 Lean，现在最新的 Lean 4 版本进行了多项优化，包括更快的编译器、改进的错误处理和更好的与外部工具集成的能力等。

在数学领域被广泛使用的 Lean，在大模型（LLM）刷屏的今天，两者有没有更好的结合方式呢？

现在已经有人实现了，开放平台 LeanDojo 团队（关于 LeanDojo，可参考「AI 大模型帮陶哲轩解题，还能证明数学定理了？」）和加州理工学院的研究者推出了 Lean Copilot，这是一款专为 LLM 与人类交互而设计的协作工具，旨在通过人机协作给出 100% 准确的形式化数学证明。

值得注意的是，LeanDojo 团队的研究主要集中在使用 LLM 自动化定理证明方面，从这点也不难看出，他们推出的 Lean Copilot 和 LLM 相关也不会令人吃惊。

项目地址：https://github.com/lean-dojo/LeanCopilot

对于这项研究，大家除了说 Cool，就是 very cool，评价还是很高的。

在 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，配置好后就可以进行实验了。项目作者也给出了一些官方示例。

策略建议。导入 LeanCopilot 后，你可以使用 suggest_tactics 生成策略建议。使用过程中，你也可以点击建议的策略，并在证明中使用它（参考下图）。

你可以提供一个前缀如 simp 来约束生成的策略。

证明搜索。如下图所示 search_proof 将 LLM 生成的策略与 aesop （用于 Lean 4 的白盒自动化项目）相结合，来搜索多策略证明。找到证明后，你可以单击该策略以将其插入编辑器中。

前提选择。该策略用于检索潜在有用前提（premises）的列表。目前，Lean Copilot 使用 LeanDojo 中的检索器从 Lean 和 mathlib4 （Lean 4 数学库）的固定 snapshot 中选择前提。

运行 LLM。你还可以运行 Lean 中的任何 LLM 推理，不限于定理证明。在本地或远程运行任意模型（请参阅自带模型）。

项目中还提到了一些高级用法，感兴趣的读者，可以去原项目了解更多内容。

^{参考链接：https://analyticsindiamag.com/lean-co-pilot-lets-you-use-llms-as-copilots-in-lean/}

工程Lean Copilot陶哲轩