摘要
本文提出 SorryDB，这是一个动态更新的基准测试集，包含来自 GitHub 上 78 个真实世界形式化项目的开放 Lean 任务。与由竞赛题组成的静态基准不同，SorryDB 旨在推动开发更符合社区需求、更具实用性且能理解复杂依赖关系的工具。通过提供持续更新的任务流，该基准有效缓解了测试集污染问题，为评估智能体在新型形式化数学项目中的贡献能力提供了稳健指标。研究评估了通用大语言模型、智能体方法及专用符号证明器在 1000 个任务快照上的表现，结果表明当前各类方法具有互补性。
AI 推荐理由
论文核心评估 AI 在形式化数学定理证明中的推理能力，属于逻辑与数学推理的典型研究。
研究机构
Axiomatix AI
Imperial College
University of Amsterdam
Math, Inc.
The London School of Geometry and Number Theory
Côte d'Azur University
论文信息