SorryDB: Can AI Provers Complete Real-World Lean Theorems?
作者: Austin Letson, Leopoldo Sarra, Auguste Poiroux, Oliver Dressler, Paul Lezeau, Dhyan Aranha, Frederick Pu, Aaron Hill, Miguel Corredera Hidalgo, Julian Berman, George Tsoukalas, Lenny Taelman
分类: cs.AI, cs.LG
发布日期: 2026-03-03
💡 一句话要点
提出SorryDB：一个动态更新的Lean定理证明基准，用于评估AI证明器的能力。
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: Lean定理证明 AI证明器 动态基准 形式化验证 大型语言模型
📋 核心要点
- 现有Lean定理证明基准多为静态竞赛题，难以反映真实数学形式化需求，且易受测试集污染。
- SorryDB通过收集GitHub上真实Lean项目任务，并动态更新，构建更贴近实际、更具挑战性的基准。
- 实验表明，现有方法（包括LLM和专用证明器）各有优劣，集成多种方法可能更有效。
📝 摘要（中文）
本文提出了SorryDB，一个动态更新的Lean任务基准，这些任务来自GitHub上78个真实世界的形式化项目。与现有的静态基准（通常由竞赛问题组成）不同，SorryDB基准的持续更新将产生更符合社区需求、更易于数学家使用、并且更能理解复杂依赖关系的工具。此外，通过提供持续更新的任务流，SorryDB减轻了测试集污染，并为评估智能体在新的形式数学项目中做出贡献的能力提供了一个可靠的指标。作者评估了一系列方法，包括通用大型语言模型、智能体方法和专用符号证明器，使用SorryDB中选定的1000个任务快照。结果表明，当前的方法是互补的：尽管基于Gemini Flash的智能体方法性能最佳，但它并不比其他现成的语言模型、专用证明器，甚至精心策划的Lean策略列表更好。
🔬 方法详解
问题定义：论文旨在解决AI证明器在真实世界Lean定理证明任务中的能力评估问题。现有静态基准测试集存在两个主要痛点：一是数据集与实际数学形式化需求脱节，二是容易受到测试集污染，导致评估结果失真。
核心思路：论文的核心思路是构建一个动态更新的Lean定理证明基准，该基准的数据来源于GitHub上真实的Lean形式化项目。通过持续添加新的任务，可以避免测试集污染，并确保基准能够反映最新的数学形式化进展。
技术框架：SorryDB的整体框架包括以下几个主要组成部分：1) 数据收集模块：负责从GitHub上的Lean项目中自动提取定理证明任务。2) 数据清洗和预处理模块：对提取的任务进行清洗和格式化，使其能够被不同的AI证明器使用。3) 评估模块：提供统一的接口，用于评估不同AI证明器在SorryDB上的性能。4) 动态更新模块：定期从GitHub上收集新的Lean项目，并将其中的定理证明任务添加到SorryDB中。
关键创新：SorryDB的关键创新在于其动态更新的特性。与传统的静态基准测试集不同，SorryDB能够持续地反映最新的数学形式化进展，并避免测试集污染。此外，SorryDB的数据来源于真实的Lean项目，因此更贴近实际应用场景。
关键设计：SorryDB的关键设计包括：1) 任务选择策略：选择具有代表性和挑战性的定理证明任务。2) 评估指标：使用多种指标来评估AI证明器的性能，包括证明成功率、证明时间等。3) 更新频率：定期从GitHub上收集新的Lean项目，并将其中的定理证明任务添加到SorryDB中。
🖼️ 关键图片
📊 实验亮点
在SorryDB的1000个任务快照上，基于Gemini Flash的智能体方法表现最佳，但其性能提升并非绝对优势，与其他LLM、专用证明器和人工策略相比，各有优劣，表明集成多种方法具有潜力。该结果强调了当前AI证明器在复杂数学形式化任务中仍有提升空间。
🎯 应用场景
SorryDB可用于评估和比较不同的AI证明器在真实世界Lean定理证明任务中的能力。它有助于推动AI自动定理证明技术的发展，并促进数学形式化的自动化。此外，SorryDB还可以作为教育资源，帮助学生学习和理解Lean定理证明。
📄 摘要（原文）
We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed of competition problems, hillclimbing the SorryDB benchmark will yield tools that are aligned to the community needs, more usable by mathematicians, and more capable of understanding complex dependencies. Moreover, by providing a continuously updated stream of tasks, SorryDB mitigates test-set contamination and offers a robust metric for an agent's ability to contribute to novel formal mathematics projects. We evaluate a collection of approaches, including generalist large language models, agentic approaches, and specialized symbolic provers, over a selected snapshot of 1000 tasks from SorryDB. We show that current approaches are complementary: even though an agentic approach based on Gemini Flash is the most performant, it is not strictly better than other off-the-shelf large-language models, specialized provers, or even a curated list of Lean tactics.