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

现在,数学辅助注明东西都用上了大模型。「我预计,如果利用得当,到 2026 年,AI 将成为数学钻研和许多其他领域值得信赖的合著者。」数学家陶哲轩在之前的一篇博客中说道。陶哲轩这样说了,也这样做了。他最近一直在用 GPT-4、Copilot、Lean 等东西从事数学钻研,并且还在 AI 的帮助下发现了自己论文中的一处隐藏 bug。不仅如此,前几天,陶哲轩表示:对多项式 Freiman-Ruzsa 想象(PFR)的注明从事形式化的 Lean4 项目成功完成,并且耗时仅三周时间。Lean 编译器也报告该想象符合标准公理

现在,数学辅助注明东西都用上了大模型。

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

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

他最近一直在用 GPT-4、Copilot、Lean 等东西从事数学钻研,并且还在 AI 的帮助下发现了自己论文中的一处隐藏 bug。

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

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

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

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

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

在数学领域被广泛利用的 Lean,在大模型(LLM)刷屏的今天,两者有没有更好的结合方式呢?

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

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

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

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

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

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

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

在 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,配置好后就可以从事实验了。项目作者也给出了一些官方示例。陶哲轩青睐的注明助手Lean,用上了大模型

战略倡议。导入 LeanCopilot 后,你可以利用 suggest_tactics 生成战略倡议。利用过程中,你也可以点击倡议的战略,并在注明中利用它(参照下图)。

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

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

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

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

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

条件采用。该战略用于检索潜在有用条件(premises)的列表。目前,Lean Copilot 利用 LeanDojo 中的检索器从 Lean 和 mathlib4 (Lean 4 数学库)的固定 snapshot 中采用条件。

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

运转 LLM。你还可以运转 Lean 中的任何 LLM 推理,不限于定理注明。在内地或远程运转任意模型(请参阅自带模型)。

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

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

参照链接:https://analyticsindiamag.com/lean-co-pilot-lets-you-use-llms-as-copilots-in-lean/

给TA打赏
共{{data.count}}人
人已打赏
工程

GPT-2能监视GPT-4,Ilya带头OpenAI超等对齐首篇论文来了:AI对齐AI取得实证结果

2023-12-15 15:00:00

工程

源代码is all you need!7B代码小模型同尺寸无敌,性能媲美ChatGPT和谷歌Gemini

2023-12-18 15:36:00

0 条回复 A文章作者 M管理员
    暂无讨论,说说你的看法吧
个人中心
今日签到
有新私信 私信列表
搜索