MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries
本文介绍了 MathlibPR，这是一个源自真实 Lean/Mathlib4 拉取请求历史的基准测试，用于评估大语言模型和智能体区分可合并贡献与非合并贡献的能力，揭示了它们当前面临的困难，并凸显了该基准测试在开发评审助手和奖励模型方面的潜力。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一个名为Mathlib的庞大、活生生的数学图书馆。它不仅仅是一本书；它是一个巨大的、共享的施工现场，数学家和计算机科学家在此为所有数学构建一个完美、无错误的基础。为了保持这个图书馆的安全和实用，每一段新代码（即“拉取请求”或 PR）都必须通过两项测试：
- “它能运行吗？”测试：代码是否真的能在不崩溃的情况下运行？（由计算机检查）。
- “它是否是好公民？”测试：代码是否与图书馆的其他部分契合？它的编写风格是否正确？是否足够清晰，供他人使用？（由人类检查）。
长期以来，人工智能（AI）在通过第一项测试方面表现出色。它能编写出完美运行的代码。但第二项测试——人工审查——已成为瓶颈。提交的数量太多，而能够检查代码是否真正准备好合并入库的人类审查者却不足。
这篇论文提出了一个简单的问题：AI 能否学会成为审查者？ 一个 AI 能否查看一段已经能运行的代码，并判断它是否“已准备好合并”，或者是否还需要更多工作？
为了找出答案，作者们创建了一个名为MATHLIBPR的新测试。
实验：代码的“盲测”
将 MATHLIBPR 想象成对新食谱的盲测。
- 设置：研究人员收集了 Mathlib 图书馆的真实历史数据。他们汇集了数千份已经通过“它能运行吗？”测试（即编译成功）的代码提交。
- 挑战：他们将这些代码片段提供给各种 AI 模型（如 DeepSeek、Qwen 等），并问道：“这份代码是否已准备好发布到图书馆中，还是应该被退回修改？”
- 关键点：AI 不知道最终结果。它不能询问人类审查者：“你喜欢这个吗？”它必须仅像人类审查者那样， solely 基于代码本身进行判断。
他们分三轮测试了 AI，给予它越来越多的线索：
- 第一轮：仅提供代码变更和少量风格指南。
- 第二轮：代码加上自动“代码检查”（linting）错误列表（类似于代码的拼写检查器）。
- 第三轮：代码、错误信息，以及作者对其意图的描述。
结果：AI 陷入了困境
结果令人惊讶，也让 AI 社区感到有些失望。
- AI 无法区分。即使有了所有额外的线索，AI 模型仍难以区分最终被接受的代码与被拒绝或退回修复的代码。
- “是”的偏见：大多数 AI 过于乐观。即使代码实际上很混乱或不符合图书馆的风格，它们也倾向于说：“是的，这很棒！”它们很少会说：“不，这需要工作。”
- “我不知道”选项：一些模型在面对艰难决定时，只是说“我不确定”。虽然诚实，但这无助于推动图书馆向前发展。
- 更多上下文帮助不大：给予 AI 更多信息（如作者的意图或自动错误报告）并未显著提高其做出正确判断的能力。
一个有趣的发现是，即使 AI 在两个不同时间点查看同一个项目（一次是在它混乱时，另一次是在它被修复并被接受后），它往往也无法分辨哪个版本是“更好”的。这就像一个学生在考他们学过的主题，却未能注意到草稿与最终文章之间的区别。
为何这很重要
论文结论指出，虽然 AI 在编写能运行的代码方面表现出色，但目前它在审查代码以判断其是否属于高质量图书馆方面非常糟糕。
作者们并非主张 AI 应取代人类审查者。相反，他们将这个基准（MATHLIBPR）视为一个起点。它是一个工具，旨在帮助训练未来的 AI 系统成为更好的“辅助审查者”。目标是构建一个 AI，它能通过发现明显的风格问题或缺失的文档来协助人类，充当第一道防线，从而使人类审查者能够专注于工作中最困难、最具创造性的部分。
简而言之：AI 是一位出色的建设者，但目前，它是一位糟糕的检查员。这篇论文提供了第一个真正的测试，以精确衡量它究竟有多糟糕，以便我们教导它做得更好。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。