研究人员推出了SorryDB，这是一个新颖的基准，旨在评估AI在Lean数学证明助手完成现实世界形式化任务的能力。与静态基准不同，SorryDB会动态更新GitHub项目中的开放任务，目标是生产更符合社区需求并能处理复杂依赖关系的AI工具。初步评估表明，尽管使用Gemini Flash的代理方法表现最佳，但它并不严格优于其他大型语言模型、专业证明器或精选的Lean策略，这表明当前形式数学的AI方法之间存在互补性。 AI
影响 该基准可以加速能够为形式数学和复杂依赖推理做出贡献的AI代理的开发。
排序理由 该集群描述了一篇介绍AI研究新基准的新学术论文。[lever_c_demoted from research: ic=1 ai=1.0]
AI 生成摘要 · Google Gemini · 来自 1 个来源。 我们如何撰写摘要 →