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 编译器持续交互，把复杂问题拆成小单元，并用非形式化蓝图衔接形式证明构造。
正文 · 原文
Authors: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
Abstract:Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate mechanically verifiable proofs in formal languages like Lean. We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving. LEAP leverages foundation model capabilities, such as informal reasoning, instruction following, and iterative self-refinement. By decomposing complex problems into smaller units, the system bridges formal proof construction with informal blueprints through continuous interaction with the Lean compiler. To provide a rigorous evaluation beyond increasingly saturated benchmarks, we introduce Lean-IMO-Bench, a benchmark of IMO-style problems formalized in Lean, with short statements yet highly non-routine and multi-step proofs across a wide range of difficulty levels. Empirically, on the latest 2025 Putnam Competition, an annual mathematics competition for undergraduate students in North America, LEAP solves all 12 problems, matching recent breakthroughs by frontier formal mathematical models. On Lean-IMO-Bench, LEAP boosts the one-shot formal solve rate of general-purpose LLMs from below 10% to 70%, notably surpassing the 48% benchmark set by a specialized, gold-medal-caliber IMO system. Furthermore, we demonstrate LEAP's research-level utility by autonomously formalizing complex proofs for open combinatorial challenges, including a verified proof for a key subproblem in Knuth's Hamiltonian decomposition of even-order Cayley graphs.
| Subjects: | Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2606.03303 [cs.AI] |
| (or arXiv:2606.03303v3 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2606.03303 arXiv-issued DOI via DataCite |
Submission history
From: Po-Nien Kung [view email]
[v1]
Tue, 2 Jun 2026 08:16:42 UTC (891 KB)
[v2]
Wed, 3 Jun 2026 06:16:05 UTC (891 KB)
[v3]
Thu, 12 Nov 2026 18:13:31 UTC (892 KB)
来源：arXiv cs.AI · arxiv.org