做 AI 推理、数学证明或形式化验证的团队会发现，LEAP 把通用 LLM 的数学能力拉高了一个量级——不用专用模型也能解 IMO 级难题，值得直接看论文复现思路。
Google 发布新论文《LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks》，提出一种智能体框架，让通用大语言模型（非专用数学模型）在形式数学证明任务中表现大幅提升。传统方法要求模型一次性写出完整形式证明，在复杂问题上几乎失败（成功率低于10%）。LEAP 将证明过程分解为图结构的目标与子目标，允许模型规划步骤、重用已证明引理，并与 Lean 验证器交互获取反馈。在 Putnam 2025 的 12 道题上，LEAP 全部解出；在基于 IMO 风格的 60 道题基准上，通用 LLM 成功率从不足 10% 提升至 70%。这表明模型在形式数学上的弱点并非能力不足，而是缺乏与验证器的结构化交互方式。
源：https://t.co/MfdIsDX4dT
源： x.com/rohanpaul_ai/s… Rohan Paul @rohanpaul_ai 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" 🔗 View Quoted Tweet 💬 0 🔄 0 ❤️ 0 👀 464 ⚡