LEAP：基于智能体框架为大型语言模型注入形式化数学推理能力

背景

大型语言模型（LLMs）在非形式化数学推理方面展现出了强大的能力，但在生成可在形式化语言（如 Lean）中进行机械验证的证明时却显得力不从心。形式化证明要求极高的逻辑严谨性和语法正确性，这与传统自然语言处理任务存在显著差异。尽管前沿模型在解决特定数学问题上取得了突破，但通用基础模型在形式化定理证明领域的表现仍远未达到实用水平。

为了弥合这一差距，研究人员提出了 LEAP 框架。该框架旨在利用通用基础模型的非形式化推理、指令遵循以及迭代自我完善等能力，通过智能体（Agentic）交互机制，将复杂的数学问题分解为更小的单元，并通过与 Lean 编译器的持续互动，搭建起非形式化蓝图与形式化证明构建之间的桥梁。

此外，现有的基准测试日益饱和，难以准确评估模型在形式化数学领域的真实水平。为此，研究团队引入了 Lean-IMO-Bench，这是一个基于 Lean 形式化的国际数学奥林匹克（IMO）风格问题集。该基准包含简短但高度非例行、多步骤的证明问题，涵盖了广泛难度等级，旨在提供超越传统基准的严格评估标准。

核心内容

LEAP 框架的核心在于其智能体架构，它通过以下机制显著提升通用 LLM 在形式化定理证明中的表现：

1. 智能体驱动的形式化证明构建： LEAP 不仅仅是一个简单的提示工程工具，而是一个多步骤的智能体系统。它利用基础模型的非形式化推理能力制定解题策略，然后通过迭代自我完善机制，不断调整和优化形式化代码。系统通过与 Lean 编译器的持续交互，实时获取错误反馈并修正证明步骤，从而将非形式化的数学思路转化为可被机器验证的形式化证明。

2. 问题分解与蓝图映射： 面对复杂的数学证明，LEAP 将其分解为更小的、可管理的单元。这种分解策略使得模型能够专注于局部逻辑的正确性，再通过组合这些局部证明来构建整体证明。这一过程有效地桥接了非形式化的解题蓝图与形式化的代码实现。

3. Lean-IMO-Bench 基准测试： 为了全面评估 LEAP 的性能，研究团队构建了 Lean-IMO-Bench。该基准专门针对 IMO 风格的难题，这些问题虽然陈述简短，但需要多步骤、非例行的推理过程。这为评估模型在复杂、高难度形式化证明任务中的能力提供了新的标准。

4. 实证结果与性能突破：

   • 2025 年普特南数学竞赛（Putnam Competition）：LEAP 成功解决了该年度北美本科生数学竞赛的所有 12 道题目。这一成绩与近期前沿形式化数学模型取得的突破性进展相媲美。
   • Lean-IMO-Bench 表现：在 Lean-IMO-Bench 上，LEAP 将通用 LLM 的一次性形式化解题率从低于 10% 大幅提升至 70%。这一成绩显著超越了由专门针对 IMO 级别、金牌水平的系统所设定的 48% 的基准线。
   • 研究级应用：LEAP 还展示了其在研究层面的实用性。它能够自主形式化复杂证明，包括解决开放组合挑战中的关键子问题。例如，研究团队利用 LEAP 成功形式化并验证了关于偶阶 Cayley 图的 Knuth 哈密顿分解中的一个关键子问题。

关键要点

• 通用模型的能力跃升：LEAP 证明了通用基础模型（General-purpose Foundation Models）在经过智能体框架增强后，可以在形式化定理证明领域达到甚至超越专用模型的性能。
• 交互式的自我完善：核心创新在于利用与 Lean 编译器的持续交互进行迭代自我完善，而非依赖静态的提示或一次性生成。
• 基准测试的创新：Lean-IMO-Bench 的引入填补了高难度、多步骤形式化证明评估的空白，提供了比传统基准更具挑战性和区分度的评估标准。
• 性能对比显著：
  • 一次性形式化解题率从 <10% 提升至 70%。
  • 超越专门 IMO 金牌系统（48%）约 22 个百分点。
  • 在 2025 普特南竞赛中实现 100% 解题率（12/12）。
• 实际研究价值：LEAP 不仅限于竞赛题目，还能处理开放研究问题，如 Knuth 哈密顿分解中的子问题，证明了其在前沿数学研究中的潜在应用价值。

意义与影响

LEAP 框架的提出标志着形式化数学辅助工具的一个重要转折点。首先，它降低了形式化证明的门槛。以往，形式化证明往往需要专家级的数学和编程知识，而 LEAP 使得通用 LLM 能够胜任这一任务，这意味着更多数学家和研究人员可以利用 AI 辅助进行形式化验证，而无需成为 Lean 语言专家。

其次，LEAP 展示了“智能体”范式在科学推理领域的巨大潜力。通过分解问题、迭代反馈和自我修正，智能体框架能够处理传统 LLM 难以应对的长链条、高复杂度逻辑任务。这种范式可能不仅限于数学，还可能扩展到代码生成、形式化验证软件系统等其他需要严格逻辑一致性的领域。

最后，Lean-IMO-Bench 和 LEAP 在普特南竞赛及研究问题上的成功，为 AI 在数学领域的角色重新定位提供了实证支持。AI 不再仅仅是辅助计算或搜索的工具，而是能够参与高水平数学推理甚至辅助解决开放研究问题的合作伙伴。这为未来构建更强大的 AI 科学家（AI Scientist）奠定了基础，推动了数学研究方法的现代化变革。