MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries

📄 arXiv: 2605.07147v1 📥 PDF

作者: Zixuan Xie, Xinyu Liu, Shangtong Zhang

分类: cs.LO, cs.AI, cs.LG

发布日期: 2026-05-08

💡 一句话要点

提出MathlibPR基准测试，旨在利用大语言模型辅助形式化数学库的Pull Request评审

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化验证 大语言模型 代码评审 Mathlib 基准测试 自动化软件工程

📋 核心要点

  1. 核心问题：Mathlib的快速增长受限于人工评审瓶颈，现有LLM难以判断PR是否符合社区规范及是否具备被合并的价值。
  2. 方法要点：构建了基于真实Mathlib4 PR历史的MathlibPR基准，并设计了分阶段评估协议，将PR历史转化为监督信号。
  3. 实验效果：研究发现当前主流LLM和智能体在区分“可合并”与“仅通过构建”的PR方面表现不佳，揭示了该任务的挑战性。

📝 摘要（中文）

Lean与Mathlib生态系统已成为大语言模型（LLM）辅助形式化推理的事实标准。然而，现有研究多将Mathlib视为依赖项，而非贡献对象。Mathlib的增长目前受限于人工评审瓶颈，评审员需判断PR是否符合规范并具备整合价值。为此，本文提出了MathlibPR，这是一个基于真实Mathlib4 PR历史构建的基准测试。通过分阶段评估协议，研究评估了DeepSeek、Qwen等模型及Codex、Claude Code等智能体。结果显示，现有模型难以区分“可合并”与“仅通过构建但未被采纳”的PR。MathlibPR将PR历史转化为监督信号，为开发评审辅助工具及奖励模型提供了基础，助力LLM生成高质量、可合并的数学贡献。

🔬 方法详解

问题定义：论文旨在解决形式化数学库（如Mathlib4）中Pull Request（PR）评审效率低下的问题。现有痛点在于，虽然LLM能辅助生成代码，但无法判断生成的代码是否符合Mathlib的严格规范，导致大量PR无法被合并，增加了人工维护负担。

核心思路：将PR评审视为一个分类或决策任务，利用历史PR数据作为监督信号。通过构建基准测试，量化模型对“可合并性”的判断能力，从而为训练评审辅助模型或奖励模型提供数据支撑。

技术框架：MathlibPR基准包含数据收集、预处理和分阶段评估协议。首先从GitHub抓取Mathlib4的PR历史，提取代码差异（diff）、评审意见及最终合并状态；随后构建评估流水线，要求模型在给定上下文的情况下预测PR是否会被合并。

关键创新：首次将形式化数学库的PR评审过程形式化为机器学习任务。与以往仅关注代码生成不同，该研究关注代码的“质量评估”与“合规性”，填补了形式化验证领域在自动化评审方面的空白。

关键设计：采用了分阶段评估策略，从简单的二分类任务（是否合并）扩展到更复杂的评审建议生成。利用真实历史数据中的“通过构建但未合并”与“最终合并”的PR作为负样本与正样本，构建了具有挑战性的评估集。

📊 实验亮点

实验评估了DeepSeek、Qwen、Goedel、Kimina等模型及Codex、Claude Code智能体。结果表明，即使是顶尖模型在区分“可合并”与“仅通过构建”的PR时表现依然吃力，准确率接近随机水平。这一发现量化了当前模型在理解复杂数学库规范与工程标准方面的局限性，为后续研究提供了明确的性能基线。

🎯 应用场景

该研究主要应用于形式化数学与软件工程交叉领域。其核心价值在于构建自动化评审辅助工具，减轻Mathlib等大型开源项目的维护负担。未来可扩展至其他形式化验证语言（如Coq、Isabelle）的社区贡献流程，提升LLM在复杂代码库中的协作与贡献能力。

📄 摘要（原文）

The ecosystem of Lean and Mathlib has become the de facto standard for large language model (LLM) assisted formal reasoning with remarkable successes in recent years. Those successes, however, only consume Mathlib as an essential dependency but do not directly contribute to it. In the meantime, the growth of Mathlib has recently been bottlenecked by the review process, which requires human reviewers to judge whether proposed pull requests (PRs) follow the Mathlib's conventions and are worth integrating as part of a shared mathematical infrastructure. This leads to our central question: can LLMs help review Mathlib PRs? To this end, we introduce MathlibPR, a benchmark built from real Mathlib4 PR histories. We further propose a staged evaluation protocol and use it to evaluate both LLM models (e.g., DeepSeek, Qwen, Goedel, and Kimina) and LLM agents (e.g., Codex and Claude Code). Surprisingly, both LLM models and LLM agents struggle to distinguish merge-ready PRs from build-passing PRs that were revised or never merged. By turning Mathlib PR histories into a supervised signal, MathlibPR provides a step toward reviewer assistants and reward models that could help evaluate PRs and steer LLMs toward producing merge-ready Mathlib contributions.