SorryDB: Can AI Provers Complete Real-World Lean Theorems?

本文介绍了 SorryDB，这是一个基于 GitHub 上真实 Lean 项目的动态更新基准，旨在评估 AI 证明器在解决现实世界形式化任务中的能力，并发现当前通用大模型、智能体方法、专用符号证明器及战术列表等 approaches 具有互补性而非单一主导。

要点

这篇论文介绍了一个名为 SorryDB 的新项目，它的核心目的是测试人工智能（AI）在真实世界中证明数学定理的能力，而不是在“考试”中拿高分。

为了让你轻松理解，我们可以把这篇论文的内容想象成一场**“修路大赛”**的变革。

1. 以前的比赛：在“模拟考场”里修路

过去，人们测试 AI 证明定理的能力，就像让 AI 去参加奥林匹克数学竞赛（比如 IMO 或 Putnam）。

• 比喻：这就像给 AI 一套套精心设计的、独立的“模拟驾驶考题”。题目很完美，路况很清晰，答案也是固定的。
• 问题：
  • 太简单/太旧了：这些题目已经被 AI 刷了无数遍，AI 可能只是背下了答案（死记硬背），而不是真的学会了开车。
  • 不接地气：现实生活中的修路（数学研究）充满了突发状况、复杂的依赖关系和未完成的工程，而模拟考题太干净、太理想化了。
  • 饱和了：现在的 AI 在这些考题上几乎都能拿满分，我们没法看出谁更强，也没法知道它们能不能解决新问题。

2. 现在的创新：去“真实工地”修路

作者们提出了 SorryDB，这就像把考场搬到了真实的建筑工地上。

• 什么是 "Sorry"？
  在数学家使用的一种叫 Lean 的编程语言中，当他们写下一个定理但还没想好怎么证明时，会先写一个占位符，叫 sorry（意思是“抱歉，这里还没写完”）。这就像工地上立了一块牌子：“此路不通，正在施工中”。
• SorryDB 是什么？
  它是一个动态更新的数据库，专门收集 GitHub 上 78 个正在进行的真实数学项目中所有带 sorry 的地方。
  • 比喻：想象有一个巨大的“工地巡查机器人”，它每天去巡视这些真实的数学项目，把所有还没修好的“坑”（sorry）都记录下来，形成一个不断更新的“修路任务清单”。
  • 特点：这些任务不是出题人编的，而是数学家们在真实研究中留下的。有的很难，有的很琐碎，有的依赖其他还没修好的路。

3. 测试过程：谁能把路修通？

作者们让各种 AI 模型（包括通用的聊天机器人、专门的数学 AI、以及会自我纠错的“智能体”）来尝试填补这些 sorry。

• 任务：AI 需要写出代码，把那个“抱歉”替换成真正的证明过程，让计算机能编译通过。
• 结果发现：
  1. 单打独斗不如团队合作：没有一种 AI 是万能的。有的擅长修简单的路（教学类项目），有的擅长修复杂的立交桥（高深数学）。如果把所有 AI 的结果加起来，能修好的路会多很多。
  2. “试错”比“死磕”更重要：最成功的 AI 不是那种一次就猜对答案的，而是**“自我修正”或“智能体”**模式。
     • 比喻：就像修路时，AI 先试着铺一段，如果计算机报错（路塌了），它看到错误信息，就回头调整方案再试一次。这种“尝试 - 报错 - 修改”的循环，比一次性猜对要有效得多。
  3. 通用模型表现惊人： surprisingly，像 Gemini 这样通用的聊天机器人，只要给它“试错”的机会，表现比专门训练过的数学 AI 还要好。这说明理解上下文和灵活调整比死记硬背数学公式更重要。

4. 为什么这很重要？

• 拒绝作弊：因为任务清单是实时更新的，AI 没法在训练数据里提前背答案。
• 真正有用：如果 AI 能解决这些真实的 sorry，说明它真的能帮数学家干活，而不仅仅是做做题。
• 永远在进化：随着 AI 越来越强，把 sorry 填平，剩下的 sorry 就会越来越难。这个数据库会像“打怪升级”一样，永远保持挑战性，不会像旧考题那样被“刷爆”。

总结

这篇论文就像是在说：

“别再让 AI 在模拟考卷上拿满分了，那没用。让我们把它扔到真实的数学工地上，看它能不能把那些还没修好的路（sorry）给修通。我们发现，那些懂得**‘犯错后立刻改正’**的 AI，才是真正能帮人类解决复杂问题的助手。”

SorryDB 就是那个让 AI 从“做题家”变成“实干家”的试金石。

技术摘要

1. 研究背景与问题 (Problem)

核心问题：
现有的自动定理证明（Automated Theorem Proving, ATP）评估基准（如 miniF2F, PutnamBench）主要基于数学竞赛题目。这些基准存在以下局限性：

• 与实际应用脱节： 竞赛题通常是独立的、上下文不依赖的，而现实世界的形式化项目（Formalization Projects）涉及复杂的依赖关系、特定的库定义和长上下文的代码库。
• 数据饱和与泄露： 许多竞赛题已被现有模型“刷爆”，且由于数据集公开，模型可能在训练数据中直接“记忆”了答案，导致评估结果无法反映真实的推理能力。
• 缺乏动态性： 静态基准无法反映数学形式化领域的最新进展和未解决的难题。

目标：
构建一个能够反映真实世界 Lean 形式化项目日常需求的动态基准，用于评估 AI 证明器在解决未完成的、真实的、具有上下文依赖的数学证明任务中的能力。

---

2. 方法论 (Methodology)

2.1 数据集构建：SorryDB

作者提出了 SorryDB，这是一个从 GitHub 上活跃的 Lean 开源项目中动态提取的基准数据集。

• 数据源： 从 Lean 包注册表（Reservoir）中的 78 个活跃仓库（过去 3 个月有提交记录）中提取。涵盖教学、工具、基准测试、库、形式化项目等 5 大类。
• 任务定义（Fill-in-the-sorry）：
  • 在 Lean 形式化过程中，未完成的证明通常用 sorry 占位符标记。
  • 任务不是证明整个定理，而是填补特定的 sorry 占位符，使其编译通过且逻辑正确。
  • 这要求模型理解局部证明上下文（Local Context）和全局项目依赖。
• 提取流程：
  1. 筛选： 选择符合开源许可证且活跃的仓库。
  2. 提取： 扫描所有分支（主分支及工作分支）中的 sorry 关键字。
  3. 过滤与验证： 确保任务可复现（项目能构建），且 sorry 确实需要证明（类型为 Prop，而非定义类型）。
  4. 去重： 保留同一任务最新的出现版本。
• 动态更新机制： 数据集是动态更新的。随着证明器能力的提升，旧的 sorry 被解决，新的未解决任务会不断加入，避免基准饱和。

2.2 评估框架

• 验证机制： 使用 LeanInteract 工具。将模型生成的代码替换 sorry，检查项目是否能成功编译，且最终状态中不再包含该 sorry 或类似的占位符。
• 评估指标： 平均成功率（Accuracy）。
• 实验设置： 选取了截至 2026 年 1 月的快照（SorryDB-2601），包含 5663 个任务。实验选取了最新的 1000 个任务作为测试集，以最大化仓库多样性。

2.3 评估模型与方法

论文对比了多种方法：

1. 确定性策略 (Deterministic Tactics)： 如 trivial, ring, linarith, grind 等。
2. 通用大语言模型 (General-purpose LLMs)： GPT-5.2, Claude Opus 4.5, Gemini Flash/Pro 3, Qwen 3 等。
3. 专用定理证明模型 (Specialized Models)： Kimina Prover, Goedel Prover V2（针对竞赛数学微调）。
4. 迭代与智能体方法 (Iterative & Agentic)：
   • 自修正 (Self-Correcting, SC)： 模型生成尝试，若编译失败，将错误信息反馈给模型进行修正（最多 16 次迭代）。
   • 智能体 (Agentic)： 基于 ReAct 架构，包含“提议者”（Proposer）和“审查者”（Reviewer），并集成 LeanSearch 工具库搜索。

---

3. 关键贡献 (Key Contributions)

1. SorryDB 数据集： 首个基于真实开源 Lean 项目中未完成证明（sorry）构建的动态基准。它填补了竞赛题与现实应用之间的空白，强调了对项目上下文和依赖关系的理解。
2. 自动化验证框架： 提供了一套自动化的验证管道，能够准确判断模型是否真正填补了证明漏洞，而不仅仅是生成了语法正确的代码。
3. 全面的基准测试与洞察：
   • 证明了迭代反馈（Iterative Feedback） 是提升性能的关键因素，远超单次尝试（Pass@k）。
   • 揭示了不同证明器之间的互补性：没有单一模型能解决所有问题，结合多种方法（确定性策略 + LLM + 智能体）能覆盖更多任务。
   • 指出了专用模型在通用形式化任务上的局限性（如版本不匹配、过度依赖竞赛数据）。

---

4. 实验结果 (Results)

基于 1000 个任务的快照评估结果如下：

• 总体性能：

  • 确定性策略： 表现有限（Tactics 约 8.4%），但能解决一些 LLM 无法处理的简单逻辑问题。
  • 通用 LLM (Pass@1)： 表现中等，Gemini Flash 3 和 Claude Opus 4.5 表现较好（约 10-11%）。
  • 专用模型： 表现不如通用模型（Kimina 8B 仅 1.0%，Goedel V2 约 2.7%），可能受限于训练数据（旧版 Lean 或仅限竞赛题）及任务类型不匹配（填 sorry vs 证全定理）。
  • 迭代/智能体方法 (最佳)：
    • Gemini Flash 3 (Agentic)： 达到 30.3% 的成功率，表现最佳。
    • Claude Opus 4.5 (SC)： 达到 27.1%。
    • 结论： 拥有项目环境访问权、能够编译并获取错误反馈的迭代方法，比单纯增加推理预算或微调更有效。

• 互补性分析 (Complementarity)：

  • 不同模型解决的子集差异巨大。如果将所有模型的结果合并（Combined），总解决率可达 35.7%。
  • 图 3b 显示，确定性策略解决了部分 LLM 无法解决的简单任务，而 LLM 解决了需要复杂推理的任务。

• 失败案例分析：

  • 工具依赖陷阱： 某些智能体模型过度依赖搜索工具（如 LeanSearch），反而忽略了直接构建证明项，导致在需要原创性构造的任务上失败（如布朗运动性质证明）。
  • 幻觉： 模型倾向于编造不存在的库函数（如 continuous_comp）。
  • 上下文理解： 模型难以处理复杂的局部定义和依赖链。

---

5. 意义与展望 (Significance)

• 对齐社区需求： SorryDB 直接反映了数学形式化社区当前的痛点（未完成的证明），评估结果更能指导开发“真正有用”的 AI 助手。
• 解决基准饱和： 通过动态更新机制，SorryDB 避免了传统竞赛基准的饱和问题，能够持续推动领域进步。
• 方法论启示：
  • 未来的定理证明研究应更重视迭代反馈循环和环境交互，而非单纯的提示工程或一次性生成。
  • 需要开发能够理解复杂项目依赖、处理版本差异的专用模型。
• 未来工作： 计划建立排行榜（Leaderboard），定期发布新快照，并引入 Elo 评分系统来更公平地比较不同模型在动态环境下的相对性能。

总结： 该论文通过引入 SorryDB，将自动定理证明的评估从“做数学题”转向了“做数学工程”，揭示了当前 AI 在真实世界形式化任务中的潜力与不足，强调了迭代修正和上下文感知在构建实用证明助手中的核心地位。