LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
本文介绍了 LEAP，这是一个代理框架，它通过将非形式化推理与 Lean 编译器的反馈相结合，使通用大语言模型能够在形式化定理证明领域达到最先进的性能，成功解决了 2025 年普特南数学竞赛的所有 12 道题目，并在新提出的 Lean-IMO-Bench 上显著超越了专门化系统。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你拥有一位才华横溢、世界级的数学家，他能用通俗易懂的语言解释复杂的概念，能讲出精彩的故事，并能推理解决难题。然而，这位数学家非常不擅长编写代码。如果你要求他写一个程序来解决数学问题，他写的代码可能听起来很对，但一旦你尝试运行，就会立即崩溃。
这就是大语言模型（LLMs）在数学领域的现状。它们擅长“非正式”数学（讨论数学），但在“正式”数学（编写一种严格的、计算机可检查的语言，如 Lean，其中一个拼写错误就会导致整个证明失败）方面却表现挣扎。
这篇论文介绍了 LEAP（LLM-in-Lean 环境智能体证明器），它是一个全新的系统，扮演着一个超级组织严密的项目经理的角色，帮助这位才华横溢的数学家最终写出完美的代码。
以下是 LEAP 的工作原理，我们使用简单的类比来解释：
1. 问题所在：“一气呵成”的陷阱
以前，如果你要求 AI 证明一个定理，它会尝试一次性写出整个解决方案，就像一个学生试图一口气写完 50 页的论文一样。如果他们在第 3 页犯了错，整个任务就失败了。论文称之为“单次形式化”（one-shot formalization），而对于难题来说，这很少奏效。
2. 解决方案：“蓝图”方法
LEAP 改变了游戏规则，通过将过程分解，就像建造摩天大楼一样：
- 第一步：建筑师的草图（蓝图）： LEAP 不会尝试一次构建整栋建筑，而是首先要求 AI 画出一份“蓝图”。这是一份用通俗英语编写的高层计划。它会说：“要解决这个问题，我们首先需要证明引理 A，然后证明引理 B，最后将它们结合起来。”
- 第二步：施工队（形式化证明）： 一旦蓝图获得批准，AI 会尝试为计划中的仅仅“一小部分”编写实际的 Lean 代码。
- 第三步：检查员（编译器）： Lean 编译器充当严格的建筑检查员。它会检查代码。如果代码完美无缺，那就太好了！如果有错误，它会发回一条特定的消息：“这里的地基出现了裂缝。”
- 第四步：修复者（自我完善）： AI 阅读检查员的笔记，修复特定的错误，然后再次尝试。它不会从头开始，而只是修补那个漏洞。
3. 核心秘诀：“记忆地图”（DAG）
LEAP 最聪明的部分在于它如何记住自己做过的事情。想象一下你在解一个巨大的迷宫。
- 旧方法： 如果你撞到了死胡同，你可能会忘记自己从哪里来，从而在原地打转，浪费时间。
- LEAP 的方法： LEAP 绘制了一张地图（称为有向无环图，或 DAG）来记录整个迷宫。
- 如果它在迷宫的一个分支中解决了一个小谜题（一个“引理”），它会将其记录在地图上。
- 如果它稍后在另一个分支中遇到同一个谜题，它不会再次解决它。它只需查看地图，看到解决方案已经在那里了，然后直接使用。
- 这防止了 AI 浪费精力去重复造轮子，并使其能够处理那些原本需要耗费极长时间才能完成的庞大且复杂的问题。
4. 结果：从零到英雄
论文在世界上最难的数学问题上测试了这个系统：
- 普特南数学竞赛（Putnam Competition）： 这是北美大学生的艰苦数学竞赛。2025 年，平均得分仅为 120 分中的 2 分。LEAP 解决了 100% 的题目（全部 12 道题）。
- IMO-Bench： 作者创建了一个基于国际数学奥林匹克竞赛（IMO）的新测试。之前的专门数学 AI 系统（仅针对数学训练）解决了大约 48%。而使用通用型 AI 的 LEAP 解决了 70%。
5. 核心启示
论文认为，我们不需要构建只针对数学的小型专用机器人。相反，我们可以采用一个通用型 AI（了解广泛知识的 AI），并赋予它一个良好的工作流（蓝图、检查员和记忆地图）。
可以这样理解：你不需要一个专门擅长烘焙的机器人才能烤出完美的蛋糕。你只需要一位拥有好食谱、严格品尝者和笔记本（用来记录成功经验）的通用型厨师。LEAP 提供了那份食谱、品尝者和笔记本，将一个“善于交谈的人”变成了一个“完美的证明者”。
简而言之： LEAP 并没有让 AI 变得更聪明；它只是给了 AI 一种更好的方式来组织思路、检查工作并记住成功，从而使其能够解决那些此前对于通用 AI 来说无法完成的数学难题。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。