SorryDB：AI 证明器能否完成真实世界的 Lean 定理？
人工智能
2026-03-04 v1 机器学习
摘要
我们提出 SorryDB，这是一个动态更新的基准，来源于 GitHub 上 78 个真实世界形式化项目中的开放 Lean 任务。不同于现有静态基准（常由竞赛问题组成），hillclimbing SorryDB 基准将产生与社区需求相匹配、更易被数学家使用的工具，能够处理复杂依赖关系。此外，通过提供持续更新的任务流，SorryDB 缓解了测试集污染问题，为评估代理在新形式数学项目中的贡献能力提供了稳健的指标。我们对来自 SorryDB 精选 1000 个任务的若干方法进行评估，包括通用大型语言模型、代理方法以及专用符号证明器。我们表明当前方法是互补的：尽管基于 Gemini Flash 的代理方法最具表现力，但它并不一定优于其他即插即用大型语言模型、专用证明器，甚至是精选的 Lean 战术列表。
关键词
引用
@article{arxiv.2603.02668,
title = {SorryDB: Can AI Provers Complete Real-World Lean Theorems?},
author = {Austin Letson and Leopoldo Sarra and Auguste Poiroux and Oliver Dressler and Paul Lezeau and Dhyan Aranha and Frederick Pu and Aaron Hill and Miguel Corredera Hidalgo and Julian Berman and George Tsoukalas and Lenny Taelman},
journal= {arXiv preprint arXiv:2603.02668},
year = {2026}
}