【第659期】LEAP让通用大模型数学考满分

Seventy3 是一档借助 NotebookLM 解读前沿论文的播客——不是念摘要，也不是泛泛而谈，而是让 AI 帮你把论文掰开揉碎，说人话。我们蹲在人工智能、大模型、机器人算法、crypto 这几个领域，每期挑一篇值得关注的工作，用对话的方式聊给你听。你可以在通勤路上听，做实验的时候听，也可以当背景音放着，让新知识自然地长进脑子里。

如果你正在做有意思的研究，想让更多人看到——不管你是博士生、独立研究者还是实验室的博士后——把论文发给我们，我们帮你用 AI 做一期深度解读，让你的工作被更多同路人发现。

联系小助手微信：seventy3_podcast（加群/投稿论文）

今天的这篇的主题是：

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

Summary

大型语言模型（LLMs）在**非形式化数学推理（informal mathematical reasoning）**方面已展现出较强能力，但在生成能够被 Lean 等形式化证明语言机械验证（mechanically verifiable）的证明时，仍然存在较大困难。

我们提出 LEAP，一个智能体化（agentic）的框架，使通用基础模型（general-purpose foundation models）能够在自动形式化定理证明（automated formal theorem proving）任务上达到当前最先进（state-of-the-art）的性能。

LEAP 充分利用了基础模型已有的能力，包括：

• 非形式化数学推理（informal reasoning）；

• 指令遵循（instruction following）；

• 迭代式自我改进（iterative self-refinement）。

通过将复杂证明任务拆解为多个较小的子问题，LEAP 在 Lean 编译器的持续交互反馈下，将形式化证明的构造过程与非形式化证明思路（informal blueprints）有效衔接，从而逐步完成形式化证明。

为了突破现有基准逐渐趋于饱和的问题，我们进一步提出了 Lean-IMO-Bench，一个由 Lean 形式化表示的国际数学奥林匹克（IMO）风格题目组成的新基准。该基准中的题目虽然题干较短，但证明过程高度非套路化（non-routine），通常包含多个推理步骤，并覆盖了广泛的难度范围，因此能够更严格地评估形式化证明能力。

实验结果表明，在 2025 年 Putnam 数学竞赛（北美本科生年度数学竞赛）上，LEAP 成功解决了全部 12 道题目，与近期前沿形式化数学模型取得的突破性成果相当。

在 Lean-IMO-Bench 上，LEAP 更显著提升了通用大语言模型的一次性形式化证明成功率（one-shot formal solve rate）：由不足 10% 提升至 70%，明显超过了此前由一个专门面向 IMO、达到金牌水平的系统所创造的 48% 基准成绩。

此外，我们还展示了 LEAP 在数学研究中的实际应用价值。该系统能够自主完成复杂证明的形式化工作，用于解决开放性的组合数学问题。其中包括为 Knuth 关于偶数阶 Cayley 图哈密顿分解（Hamiltonian decomposition of even-order Cayley graphs）中的一个关键子问题，自动构造并验证了一份形式化证明。

这些结果表明，LEAP 不仅显著提升了通用大语言模型的形式化证明能力，也展示了其作为数学研究辅助工具在前沿科研中的潜力。

原文链接：https://arxiv.org/abs/2606.03303