MathlibPR：形式数学库拉取请求合并结果基准

论文提出基于 Mathlib4 PR 历史的合并结果基准 MathlibPR。

资讯摘要

论文提出 MathlibPR，一个基于真实 Mathlib4 PR 历史构建的基准，并设计分阶段评估协议，用于检验 LLM 能否辅助审查 Mathlib 拉取请求。作者报告，DeepSeek、Qwen、Goedel、Kimina 等模型以及 Codex、Claude Code 等智能体都难以区分可合并的 PR 与仅通过构建但被修改或从未合并的 PR。论文希望借此为审查助手和奖励模型提供监督信号。

要点速读

1. MathlibPR 基于真实 Mathlib4 PR 历史构建，并提出分阶段评估协议。
2. 作者报告，所测 LLM 模型与 LLM 智能体均难以区分可合并 PR 与仅通过构建的 PR。
3. 论文称该基准可为审查助手与奖励模型提供监督信号。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/11/5 08:00:38（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。