APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
本文介绍了 APE-Bench，这是首个用于评估形式化数学库中自动化证明工程的系统性框架与基准测试，它通过提取真实的仓库级任务，并提供一个统一的测试平台，来验证不同智能体实现方案在语法编译与语义正确性方面的表现。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正试图教一个机器人如何成为一个庞大且充满活力的数学证明库——Mathlib——的顶级图书管理员。这个图书馆包含数百万页的内容。它不仅仅是一本静态的书；它正不断地被人类专家重新编写、扩展和修复。
长期以来，研究人员一直在测试机器人在解决孤立的单一数学谜题（例如“证明 2+2=4”）方面的能力。但在现实世界中，成为一名数学家不仅仅是解决一个谜题；这涉及到证明工程（proof engineering）。这意味着要能够浏览整个图书馆，找到合适的工具，修复损坏的页面，并确保你的新内容能完美地融入已有的数百万页内容中，而不会破坏任何其他部分。
这篇论文介绍了一种新的方法，用于测试机器人在这些现实世界技能方面的表现。以下是使用简单类比进行的详细拆解：
1. 问题所在：“孤立的谜题” vs. “活着的图书馆”
- 旧方法 (miniF2F)： 想象一下，通过给厨师一张单张食谱卡并要求他们做一道菜来测试他们。如果菜的味道好，他们就算通过了。但这并不能告诉你他们是否能管理整个餐厅厨房、订购食材或修理坏掉的烤箱。
- 现实情况： 真正的数学工作就像经营那家餐厅。你必须与其他厨师协作，使用特定的工具，并确保你的新菜品不会毁掉整份菜单。
- 差距： 现有的测试只检查机器人是否能做出那道单项菜。它们没有检查机器人是否能应对真实厨房中的混乱局面。
2. 解决方案：APE-Bench（“活着的图书馆”测试）
作者创建了 APE-Bench，这是一个模拟现实生活中的图书馆维护工作的全新测试场。
- 运作方式： 系统不再给机器人一个虚假的谜题，而是观察 Mathlib 库的真实历史。它找到人类专家做出更改（即一次“提交/commit”）的时刻，隐藏该更改，然后询问机器人：“这是更改发生前的库。这里有一条关于人类想要做什么的说明。你能完成那个更改吗？”
- 转折点： 机器人不仅根据代码是否能“运行”（语法）来评分。它还根据两件事进行评分：
- 编译（Compilation）： 代码是否能实际编译且没有错误？（菜是不是烧焦了？）
- 语义检查（Semantic Check）： 机器人是否真的完成了要求的任务？（他们是修复了正确的问题，还是只是随机修改了几行代码？）
3. 基础设施：APE-Harness（“通用厨房”）
为了公平地运行这些测试，他们构建了一个名为 APE-Harness 的系统。你可以把它看作是一个通用厨房模拟器。
- “契约”： 每个测试都附带一份严格的契约。它规定：“你处于这个特定版本的库中。你只能触碰这些文件。你必须证明你完成了工作。”
- “脚手架”： 该系统旨在让你可以将不同的机器人（如 Claude Code、Codex 或他们自己的 APE-Agent）接入同一个厨房。因为厨房规则（契约）对所有人都是一致的，所以你可以公平地比较谁才是真正的优秀厨师，而不是仅仅看谁在阅读指令时运气更好。
- “时间旅行”技巧： 这个库有 67 个不同的版本（就像 67 个不同版本的书籍）。存储所有版本会占用巨大的空间。作者构建了一个聪明的“去重”系统。如果某一页在版本 1 和版本 67 中是相同的，系统只会存储一次，并进行指向。这为他们节省了 85% 的存储空间和 98% 处理数据所需的资金。
4. 结果：谁通过了测试？
他们在这种更难的新测试上测试了三个顶尖的 AI 模型（GPT-5.2、Gemini 3 Pro 和 Gemini 3 Flash）。
- 难度： 新测试比旧的“单一谜题”测试要难得多。
- 在旧测试中，机器人的正确率在 80–90%。
- 在这个新的“库维护”测试中，表现最好的机器人也仅达到了 47% 的正确率。
- 赢家： Gemini 3 Flash 是效率最高的。它以最低的成本解决了最多的问题。其他模型尝试得更多（对话轮数更多），但由于没能及时完成任务，在结束前就耗尽了它们的“预算”。
- 教训： 机器人擅长解决孤立的数学问题，但在处理管理庞大且不断演进的代码库这一杂乱且复杂的任务时，仍然显得力不从心。
5. 为什么这很重要
论文声称，这是首次有了系统化、自动化的方法来测试 AI 是否能够进行“证明软件工程”。
- 它将目标从“AI 能否解决一个数学问题？”提升到了“AI 能否在团队环境中担任专业的数学家？”
- 它提供了一个公平的竞技场，让不同的 AI 系统可以使用完全相同的规则和工具进行比较。
简而言之： 作者构建了一个真实的、混乱的巨大数学库模拟器，并设定了一套规则来测试 AI 是否能修复它。他们发现，虽然 AI 正在变得越来越好，但在能够可靠地独立管理复杂的现实数学项目方面，仍有很长的路要走。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。