LEAP：以智能体框架为形式数学超级充能LLM

摘要

大型语言模型 (LLM) 表现出强大的非正式数学推理能力，但很难用 Lean 等正式语言生成可机械验证的证明。我们提出了 LEAP，一种代理框架，使通用基础模型能够在自动化形式定理证明方面实现最先进的性能。 LEAP 利用基础模型功能，例如非正式推理、指令遵循和迭代自我完善。通过将复杂的问题分解为更小的单元，系统通过与Lean编译器的持续交互，将正式的证明构造与非正式的蓝图联系起来。为了提供超越日益饱和的基准的严格评估，我们引入了 Lean-IMO-Bench，这是一种以Lean形式化的 IMO 风格问题的基准，具有简短的陈述，但在各种难度级别上都具有高度非常规和多步骤的证明。根据经验，在最新的 2025 年普特南竞赛（北美一年一度的本科生数学竞赛）上，LEAP 解决了全部 12 个问题，与前沿形式数学模型的最新突破相匹配。在 Lean-IMO-Bench 上，LEAP 将通用 LLM 的一次性正式解决率从低于 10% 提高到 70%，显着超过了专门的金牌级 IMO 系统设定的 48% 基准。此外，我们通过自动形式化开放组合挑战的复杂证明来展示 LEAP 的研究级实用性，包括偶数阶凯莱图 Knuth 哈密顿分解中关键子问题的验证证明。

LEAP：以智能体框架为形式数学超级充能LLM：论文配图 — 图 2：Putnam 2025 问题 A6 的 DAG 示例。 LEAP 将定理分解为证明草图和支持引理。通过预期引理规划，智能体还可以提出辅助引理陈述，这些陈述不是立即需要的，但以后可能有用；这些用虚线边缘显示，不需要证明主要定理。绿色节点是经过验证的节点，棕色块表示在节点处引入的定义、结构或变量。