技術的概要：MATHLIBPR – 形式数学ライブラリのレビュー準備性評価のためのベンチマーク

1. 問題定義

Lean と Mathlib のエコシステムは、大規模言語モデル（LLM）支援による形式推論の標準となり、オリンピックレベルの問題解決（MiniF2F）、競技数学（AlphaProof）、大規模形式化プロジェクト（Gauss agent）における最近の成功を収めています。しかし、これらのシステムは主に Mathlib を依存関係として「消費」するだけであり、それに対して「貢献」するものではありません。LLM が生成したコードは Lean カーネルによって正しさが検証可能ですが、その貢献が「マージ準備完了」であるか、すなわちコミュニティの慣習に準拠し、ライブラリの整合性を維持し、長期的な保守に適しているかどうかを判断するには、人間のレビューが必要です。

人間のレビューは現在、Mathlib の成長における主要なボトルネックとなっており、約 300 件のプルリクエスト（PR）が backlog として蓄積され、中央値の待ち時間は 2 週間です。本論文が扱う中心的な問いは以下の通りです：LLM は Mathlib の PR レビューを支援できるか？ 具体的には、それらはマージ準備完了のビルド通過コードと、修正が必要または却下されるビルド通過コードを区別できるでしょうか？

2. 手法

2.1 データセット構築：MATHLIBPR

著者は、実際の Mathlib4 の PR 履歴から構築されたベンチマーク MATHLIBPR を紹介します。

• ソース: leanprover-community/mathlib4 リポジトリのクローズドされた PR（2026 年 4 月 5 日時点）。
• 選択基準: ベンチマークは ビルド通過のスナップショット のみに焦点を当てます。これにより、構文エラーやコンパイル失敗に基づく自明な戦略を排除し、モデルにコードの品質と慣習に基づいた判断を迫ります。
• ラベル:
  • Merge Ready（マージ準備完了）: master ブランチに受け入れられたスナップショット。
  • Not Merge Ready（マージ準備未完了）: ビルドチェックを通過したが、受け入れ前に修正されたか、マージされなかった PR に属するスナップショット。
• 構成: 最終的なデータセットは、12,063 件の PR から 15,895 件のラベル付きスナップショットを含みます（11,409 件のマージ準備完了、4,486 件のマージ準備未完了）。また、修正の進展を認識するテストのために、3,687 件の PR 内ペア（より以前のビルド通過スナップショット対最終受け入れ版）が含まれています。

2.2 評価プロトコル

著者は、モデルに段階的により豊富な文脈を提供する 3 段階の評価プロトコル を提案します。

• ステージ 1: コードローカルの証拠（diff、変更されたファイル）と、Mathlib ガイドライン（命名、スタイル、ドキュメント）のコンパクトな要約。
• ステージ 2: 過去の GitHub チェック記録またはローカルで補完されたものから導出された構造化された診断情報（リンティング、インポート、宣言の配置、API 適合性）を追加。
• ステージ 3: 意図として明記された PR タイトルと説明を追加。

2.3 評価対象システム

ベンチマークは 2 種類のシステムを評価します。

1. LLM モデル: DeepSeek-R1-Distill-Qwen、Qwen3-8B、Mathlib で事前ファインチューニングされた Goedel-Prover-V2-32B、Kimina-Prover-Distill-8B。
2. LLM エージェント: Codex（GPT-5.4）と Claude Code（Claude Sonnet 4.6）。エージェントは読み取り専用のローカルリポジトリチェックアウトで動作し、ファイルの編集、ウェブへのアクセス、PR の結果の取得を制限されています。

2.4 出力スキーマと指標

システムは自由形式のテキストではなく、構造化された JSON レビューを出力する必要があります。スキーマには以下が含まれます。

• Verdict（判定）: merge_ready、not_merge_ready、または uncertain。
• Score（スコア）: マージ準備性のスカラースコア（$p_{merge\_ready}$）。
• Axes（軸）: 8 つのルブリック次元（命名、ドキュメント、ローカル構造、ファイル配置、インポート、証明の可読性、API 適合性、リポジトリの重複）にわたる評価。

指標:

• MR/NMR Recall: マージ準備完了クラスとマージ準備未完了クラスに対するリコール（uncertain および無効な出力をエラーとして扱う）。
• Balanced Accuracy: MR リコールと NMR リコールの平均。
• Valid-Output Rate: 実行時間予算内のスキーマ有効な出力の割合。
• AUROC: スカラースコアに基づく ROC 曲線下面積。

3. 主要な結果

3.1 全体的な性能

• 低い精度: いかなるシステムも、マージ準備完了とマージ準備未完了のスナップショットを確実に区別できませんでした。最高性能のモデル（DeepSeek）はステージ 3 で Balanced Accuracy 36.0% を達成しましたが、これはバランスの取れたタスクにおける 50% の偶然の基準を大幅に下回っています（データセットは不均衡ですが、リコール指標は失敗を浮き彫りにします）。
• クラスの非対称性: システムは merge_ready を予測する強いバイアスを示します。
  • DeepSeek（ステージ 3）: MR リコール 69.8%、しかし NMR リコールは 2.3%。
  • Qwen（ステージ 3）: MR リコール 48.3%、NMR リコールは 0.0%。
  • Codex（エージェント）: MR リコール 92.0%、しかし NMR リコールは 12.0%。
• 文脈の影響: 診断情報と PR の意図を追加すること（ステージ 2 および 3）は、限定的かつ不均一な改善をもたらしました。例えば、DeepSeek のバランスド精度は 18.1% から 36.0% に向上しましたが、マージ準備未完了のコードを特定する能力はほぼゼロのままでした。

3.2 エージェント対モデルの性能

• エージェント: Codex は高い運用信頼性（99.9% の有効出力率）と高い MR リコールを示しましたが、マージ準備未完了のコードを特定できませんでした。Claude Code は低い信頼性（56.4% の有効率）と同様に低い NMR リコールを示しました。
• 専門モデル: 形式証明でトレーニングされた Goedel と Kimina は、性能が低かったのです。Goedel の有効出力率はステージ 1 の 68.3% からステージ 3 の 13.5% に崩壊し、両モデルとも必要な JSON スキーマの代わりに散文やコードブロックを生成する無効な出力を頻繁に作成しました。

3.3 PR 内分析

同じ PR からのより以前のビルド通過スナップショット対最終受け入れスナップショットの制御された比較において：

• モデルは偶然をわずかに上回る程度でした。DeepSeek のペアワイズ精度はステージ 3 で 51.1% に頭打ちとなり、Qwen は 49.1% 付近にとどまりました。
• これは、モデルが同じ貢献の 2 つのバージョンを比較した場合でも、PR の受け入れにつながった具体的な改善を確実に検出できないことを示しています。

3.4 エラー分析

• 棄権: システムは、ドキュメントや証明の可読性の軸においてしばしば棄権（uncertain）します。
• 無効な出力: 専門モデル（Goedel、Kimina）とエージェント（Claude Code）からの出力の相当部分は、スキーマ違反、タイムアウト、または JSON 生成の失敗により無効でした。これは、モデルのトレーニング目的（定理証明）と構造化されたレビューインターフェースとの間のミスマッチを示唆しています。

4. 貢献

1. MATHLIBPR ベンチマーク: 実際の PR 履歴から派生し、ビルド通過した Mathlib 貢献のマージ準備性を評価する LLM 向けの最初のベンチマーク。
2. 段階的評価プロトコル: より豊富な文脈（診断情報、PR の意図）がレビュアーのような判断を改善するかどうかを体系的にテストするプロトコル。
3. 実証的研究: 現在の LLM とエージェントが、マージ準備完了のコードと修正を必要とするビルド通過コードを区別することに苦労していることを示す包括的な評価。これにより、コードの正しさとライブラリ統合の品質の間にギャップがあることが浮き彫りになりました。

5. 意義と主張

本論文は、MATHLIBPR が形式数学ライブラリ向けのレビュアー支援ツールや報酬モデルへの一歩を提供すると主張しています。

• 現状: 結果は、マージ準備性を判断することが、構文エラーやコンパイル失敗を検出するよりもはるかに困難な能力であることを示しています。現在のシステムは、統合された数学ライブラリをキュレートするために必要な微妙なレビュー規範を捉えることができていません。
• 将来の有用性: このベンチマークは、以下の目的で使用されることを意図しています。
  • レビュアー支援: 人間のレビュアーのためのトリアージと、潜在的なブロック要因の表面化。
  • 報酬モデリング: PR 内ペア構造（より以前のビルド通過スナップショットよりも最終受け入れスナップショットを好む）を用いて報酬モデルをトレーニングし、LLM が単に正しいだけでなく、保守可能でマージ準備完了のコードを生成するように誘導する。
• 限界: 著者は、ベンチマークが PR 履歴の選択されたスライスをカバーしており、ラベルは歴史的なメンテナーの決定（技術的ではない要因を含む可能性がある）から導出されていることを認めています。彼らは明確に、目標は人間のレビュアーを代替することではなく、助言的なシグナルを提供することであると述べています。

結論として、LLM は正しい証明を生成することに成功しましたが、Mathlib への貢献への移行には、コードスタイル、ドキュメント、ライブラリ適合性に関する判断が必要であり、現在のモデルはまだこれを習得していません。MATHLIBPR は、この方向性における進歩を測定するための基準を設定します。