arXiv cs.AI· Po-Nien Kung, Linfeng Song, Dawsen Hwang, Jinsung Yoon, Chun-Liang Li, Simone Severini, Mirek Ol\v{s}\'ak, Edward Lockhart, Quoc V Le, Burak Gokturk, Thang Luong, Tomas Pfister, Nanyun Peng·· 1 天前AI 评分60
LEAP：用智能体框架提升 LLM 形式数学证明能力
LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
AI 导读
LEAP 是一个智能体框架，让通用基础模型在自动形式定理证明上达到 SOTA，通过与 Lean 编译器持续交互，把复杂问题拆成小单元，并用非形式化蓝图衔接形式证明构造。
正文 · AI 翻译
作者：Po-Nien Kung、Linfeng Song、Dawsen Hwang、Jinsung Yoon、Chun-Liang Li、Simone Severini、Mirek Olšák、Edward Lockhart、Quoc V Le、Burak Gokturk、Thang Luong、Tomas Pfister、Nanyun Peng
摘要：大型语言模型（LLM）展现出很强的非形式化数学推理能力，但难以在 Lean 等形式化语言中生成可机械验证的证明。我们提出 LEAP，一个智能体框架，使通用基础模型在自动化形式化定理证明上达到最先进性能。LEAP 利用基础模型的能力，如非形式化推理、指令遵循和迭代式自我改进。通过将复杂问题分解为更小的单元，该系统借助与 Lean 编译器的持续交互，将形式化证明构建与非形式化蓝图连接起来。为在日益饱和的基准之外提供严格评估，我们推出 Lean-IMO-Bench，这是一个用 Lean 形式化的 IMO 风格问题基准，其陈述简短，但证明高度非例行且多步骤，难度范围广泛。在实证上，在最新的 2025 年 Putnam 竞赛（北美一年一度的本科生数学竞赛）中，LEAP 解出了全部 12 道题，与前沿形式化数学模型近期的突破相当。在 Lean-IMO-Bench 上，LEAP 将通用 LLM 的一次性形式化求解率从低于 10% 提升到 70%，显著超过了由专门的、金牌水准的 IMO 系统所设定的 48% 基准。此外，我们通过自主形式化开放组合挑战的复杂证明，展示了 LEAP 的研究级实用性，其中包括为 Knuth 关于偶数阶 Cayley 图的哈密顿分解中的一个关键子问题提供了经过验证的证明。
| 学科： | 人工智能（cs.AI） |
| 引用为： | arXiv:2606.03303 [cs.AI] |
| （或本版本的 arXiv:2606.03303v3 [cs.AI]） | |
| https://doi.org/10.48550/arXiv.2606.03303 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Po-Nien Kung [查看邮箱]
[v1]
2026年6月2日星期二 08:16:42 UTC（891 KB）
[v2]
2026年6月3日星期三 06:16:05 UTC（891 KB）
[v3]
2026年11月12日星期四 18:13:31 UTC（892 KB）
来源：arXiv cs.AI · arxiv.org