論文の概要: MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries

• arxiv url: http://arxiv.org/abs/2605.07147v2
• Date: Wed, 13 May 2026 01:55:38 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-14 17:13:58.787107
• Title: MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries
• Title（参考訳）: MathlibPR: 形式的な数学的ライブラリのためのプルリクエストマージ可読ベンチマーク
• Authors: Zixuan Xie, Xinyu Liu, Shangtong Zhang,
• Abstract要約: 実際のMathlib4 PR履歴から構築したベンチマークであるMathlibPRを紹介する。 驚いたことに、LLMモデルとLLMエージェントは、マージ可能なPRとビルドパスするPRを区別するのに苦労している。 Mathlib PR履歴を教師付き信号に変換することで、MathlibPRはレビュアーアシスタントと報酬モデルへのステップを提供する。
• 参考スコア（独自算出の注目度）: 19.81737958703724
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.
• Abstract（参考訳）: LeanとMathlibのエコシステムは、大規模言語モデル(LLM)のデファクトスタンダードになっています。 しかしこれらの成功は、Mathlibを必須の依存関係としてのみ消費するが、直接的に貢献するものではない。 このプロセスでは、提案されたプルリクエスト(PR)がMathlibの規約に従っているかを判断し、共有された数学的インフラストラクチャの一部として統合する価値がある。 LLMはMathlib PRをレビューするのに役立ちますか? この目的のために、実際のMathlib4 PR履歴から構築されたベンチマークであるMathlibPRを紹介する。 さらに、段階評価プロトコルを提案し、LLMモデル(例:DeepSeek、Qwen、Goedel、Kimina)とLLMエージェント(例:Codex、Claude Code)の両方を評価する。 驚いたことに、LLMモデルとLLMエージェントはどちらも、マージ可能なPRと修正またはマージされないビルドパスPRを区別するのに苦労した。 Mathlib PRヒストリーを教師付き信号に変換することで、MathlibPRはレビューアアシスタントと報酬モデルへのステップを提供し、PRの評価とステアLSMをマージ可能なMathlibコントリビューションの生成に役立てることができる。

関連論文リスト

• TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib? [104.38098884163541]
  新たな定義枠組みに適用した場合の現在のATPシステムの堅牢性を評価する。 本稿では,terence Tao氏のAnalytic Iから派生した,学部レベルのベンチマークであるTaoBenchを紹介する。 公平な評価のために,各問題に対してコンパイル可能な自己完結型ローカル環境を自動的に抽出するエージェントパイプラインを構築した。
  論文  参考訳（メタデータ） (2026-03-13T07:39:47Z)
• MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
  数学的民俗補題の発見と形式化を自動化するLLMベースのマルチエージェントシステムであるMathlibLemmaを紹介する。 さらに、幅広い数学的領域にまたがる4,028の型チェックリーンステートメントスイートであるMathlibLemmaベンチマークを構築します。
  論文  参考訳（メタデータ） (2026-01-30T15:24:42Z)
• DotaMath: Decomposition of Thought with Code Assistance and Self-correction for Mathematical Reasoning [24.68321102981711]
  本稿では,数理推論にコードアシストと自己補正を併用した思考の分解を利用した大規模言語モデル(LLM)について紹介する。 DotaMathモデルは複雑な数学的タスクに対処し、それらをより単純な論理的なサブタスクに分解し、コードを利用してこれらのサブタスクを解決する。 そこで我々は,DotaMathQAの模倣学習を用いて,オープンソースのLLMと比較して優れた性能を示すDotaMathモデルを訓練した。
  論文  参考訳（メタデータ） (2024-07-04T17:39:16Z)
• Mathador-LM: A Dynamic Benchmark for Mathematical Reasoning on Large Language Models [34.814875040792344]
  大規模言語モデル(LLM)の数学的推論を評価するための新しいベンチマークであるMathador-LMを紹介する。 Mathador-LMはMathadorゲームにインスパイアされており、そのゲームの目的は、与えられた基本数の集合の基本的な算術演算を用いてターゲット数に到達することである。 先行するLLMに対して,目標の難易度に従って,ベンチマークインスタンスを動的に生成しながら,安定した平均性能が得られることを示す。
  論文  参考訳（メタデータ） (2024-06-18T13:02:12Z)
• ChatGLM-Math: Improving Math Problem-Solving in Large Language Models with a Self-Critique Pipeline [42.61538071832468]
  大規模言語モデル(LLM)は、人間の言語の優れた習得を示すが、数学的な問題解決を必要とする現実世界のアプリケーションでは依然として苦戦している。 LLMアライメントのフィードバック学習段階における課題に対処する自己批判パイプラインを調整します。
  論文  参考訳（メタデータ） (2024-04-03T17:51:18Z)
• GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solvers [68.77382332826167]
  大規模言語モデル (LLM) は、様々な数学的推論ベンチマークで顕著な性能を達成している。 1つの必須かつ頻繁な証拠は、数学の質問がわずかに変更されたとき、LLMは誤って振る舞うことができることである。 このことは, LLMの数学推論能力の頑健性を評価するために, 幅広い質問のバリエーションを試すことによるものである。
  論文  参考訳（メタデータ） (2024-02-29T15:26:14Z)
• InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning [98.53491178426492]
  InternLM2から事前学習を継続するILMs InternLM-Mathをオープンソースとして公開する。 我々は、連鎖推論、報酬モデリング、形式推論、データ拡張、コードインタプリタを、統一されたSeq2seqフォーマットで統一する。 我々の事前学習モデルは、微調整なしでMiniF2Fテストセットで30.3を達成する。
  論文  参考訳（メタデータ） (2024-02-09T11:22:08Z)
• MARLlib: A Scalable and Efficient Multi-agent Reinforcement Learning Library [82.77446613763809]
  本稿では,マルチエージェントタスクとアルゴリズムの組み合わせを高速に開発するためのライブラリであるMARLlibを紹介する。 MARLlibは、マルチエージェントタスクとアルゴリズムの学習過程を効果的に切り離すことができる。 ライブラリのソースコードはGitHubで公開されている。
  論文  参考訳（メタデータ） (2022-10-11T03:11:12Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。