这项研究解决了通用 LLM 在形式数学中「一次性写完整证明」的致命短板，做 AI 推理、数学辅助工具或形式验证的开发者值得关注——LEAP 的智能体框架思路可能启发更多复杂推理场景的改进。
Google 发布新论文 LEAP，提出一种智能体框架，让通用大语言模型（LLM）能够通过规划证明步骤、分解子目标、重用已有引理并与形式验证器 Lean 交互，显著提升形式数学证明能力。在 Putnam 2025 和 IMO 风格基准测试中，LEAP 将通用 LLM 的成功率从不足 10% 提升至 70%，并解决了所有 12 道 Putnam 2025 问题。该研究揭示了通用 LLM 在形式数学中的弱点并非数学能力不足，而是缺乏与验证器的结构化交互。LEAP 将证明存储为有向图，支持子目标复用，避免一次性生成庞大证明的失败模式。
Another great paper from Google. Shows general L…
Another great paper from Google.
Shows general LLMs can solve formal math by planning proofs and checking each step. Raised general LLM performance from under 10% to 70%.
A general LLM failed badly when asked to write full formal proofs in 1 try, but became much stronger when it planned, split the work into smaller claims, reused past claims, and learned from Lean’s feedback.
The paper shows the weakness was not just the model’s math ability, but the way it was being used - the absence of structured interaction with a verifier.
The key idea is that the model does not try to write one giant perfect proof at once, because that usually fails on long and tricky problems.
Instead, LEAP stores the proof as a graph of goals and subgoals, so useful lemmas can be reused instead of rediscovered every time.
The authors tested LEAP on Putnam 2025 and a new Lean benchmark built from 60 IMO-style problems, where ordinary one-shot proof writing did very poorly.
LEAP solved all 12 Putnam 2025 problems and raised general LLM performance on the Lean IMO benchmark from under 10% to 70%.
----
Link – arxiv. org/abs/2606.03303
Title: "LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks"