APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
本論文は、実世界のレポジトリ規模のタスクを抽出することで、多様なエージェントの実装に対して構文上のコンパイルと意味論的な正当性の両方を検証するための統一されたハーネスを提供し、形式数学ライブラリにおける自動証明エンジニアリングを評価するための初の体系的なフレームワークおよびベンチマークであるAPE-Benchを紹介するものである。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
あなたは、膨大な数学的証明の「生きたライブラリ」であるMathlibのマスター・ライブラリアン（熟練司書）になるべく、ロボットに教えていると考えてください。このライブラリには数百万ページにおよぶページが含まれています。それは単なる静的な本ではありません。人間の専門家によって絶えず書き換えられ、拡張され、修正され続けているのです。
長い間、研究者たちは、ロボットが単一の孤立した数学パズル（例：「2+2=4であることを証明せよ」）を解く能力をテストしてきました。しかし、現実の世界において、数学者であるということは、単に一つのパズルを解くだけではありません。それは**証明エンジニアリング（proof engineering）**を行うことです。つまり、ライブラリ全体をナビゲートし、適切な道具を見つけ出し、壊れたページを修理し、自分の新しい追加分が、既存の数百万ものページと完璧に適合し、かつ他の部分を壊さないようにすることなのです。
本論文は、これらの現実世界のスキルをロボットにテストするための、新しい方法を紹介しています。以下に、シンプルな比喩を用いてその内容を解説します。
1. 問題点：「孤立したパズル」対「生きたライブラリ」
- 旧来の方法 (miniF2F): シェフにたった一枚のレシピカードを渡し、一つの料理を作るよう求めるテストだと想像してください。もし料理が美味しく作れたなら、そのシェフは合格です。しかし、これでは、そのシェフがレストラン全体の厨房を管理できるのか、食材を発注できるのか、あるいは壊れたオーブンを直せるのかまでは分かりません。
- 現実: 本物の数学の仕事は、そのレストランを運営することに似ています。他のシェフと連携し、特定の道具を使い、自分の新しい料理が既存のメニューを台無しにしないようにしなければなりません。
- ギャップ: 既存のテストは、ロボットが「単一の料理」を作れるかどうかだけをチェックしていました。ロボットが「現実の厨房の混乱」に対処できるかどうかはチェックしていなかったのです。
2. 解決策：APE-Bench（「生きたライブラリ」テスト）
著者らは、現実のライブラリのメンテナンスを模倣した新しいテスト環境、APE-Benchを作成しました。
- 仕組み: システムはロボットに架空のパズルを与えるのではなく、Mathlibライブラリの実際の履歴を参照します。システムは、人間の専門家が行った変更（「コミット」）を見つけ出し、その変更を隠した上で、ロボットにこう問いかけます。「これは変更前のライブラリです。そして、人間が何をしようとしていたかを示すメモがあります。この変更を行ってください。」
- ひねり: ロボットは単にコードが「実行可能か（構文）」だけで採点されるのではありません。以下の2つの要素で採点されます。
- コンパイル (Compilation): コードはエラーなくコンパイルされたか？（料理は焦げていないか？）
- 意味論的チェック (Semantic Check): ロボットは実際に指示された通りに作業を行ったか？（正しい問題を修正したのか、それとも単にランダムに行を書き換えただけなのか？）
3. インフラストラクチャ：APE-Harness（「ユニバーサルな厨房」）
これらのテストを公平に行うために、彼らはAPE-Harnessと呼ばれるシステムを構築しました。これはユニバーサルな厨房シミュレーターだと考えてください。
- 「契約 (The Contract)」: すべてのテストには厳格な契約が付随しています。それは、「あなたはこの特定のバージョンのライブラリの中にいます。触れてよいのはこれらのファイルのみです。そして、仕事をやり遂げたことを証明しなければなりません」というものです。
- 「足場 (The Scaffolds)」: このシステムは、異なるロボット（Claude Code、Codex、あるいは彼ら自身のAPE-Agentなど）を同じ厨房にプラグインできるように設計されています。厨房のルール（契約）が全員共通であるため、誰が運良く指示通りに動けたかではなく、誰が本当に優れたシェフであるかを公平に比較することができます。
- 「タイムトラベルのトリック」: ライブラリには67の異なるバージョン（本の異なる版のようなもの）があります。これらすべてを保存すると膨大な容量が必要になります。著者らは賢明な「重複排除（deduplication）」システムを構築しました。もしバージョン1とバージョン67でページが同じであれば、システムは一度だけ保存し、あとはそれを参照するようにします。これにより、ストレージ容量を85%、データ処理に必要なコストを98%削減できました。
4. 結果：誰がテストに合格したか？
彼らは、これら3つのトップティアのAIモデル（GPT-5.2、Gemini 3 Pro、Gemini 3 Flash）を、この新しい、より困難なテストで検証しました。
- 難易度: 新しいテストは、従来の「単一パズル」テストよりもはるかに困難でした。
- 旧来のテストでは、ロボットは80〜90%の正解率を叩き出していました。
- 今回の「ライブラリ・メンテナンス」テストでは、最強のロボットでも正解率はわずか**47%**でした。
- 勝者: Gemini 3 Flashが最も効率的でした。最小のコストで最も多くの問題を解決しました。他のモデルは、より熱心に試行錯誤（より多くの会話ターン）を行いましたが、完了する前に「予算」を使い果たしてしまいました。
- 教訓: ロボットは孤立した数学の問題を解くことは得意ですが、巨大で進化し続けるコードベースを管理するという、複雑で混沌としたタスクにはまだ苦戦しています。
5. なぜこれが重要なのか
本論文は、AIが「証明のためのソフトウェアエンジニアリング」ができるかどうかをテストするための、体系的かつ自動化された方法を初めて提示したと主張しています。
- これは、目標を「AIは数学の問題を解けるか？」から、「AIはチーム環境の中でプロの数学者として働けるか？」へとシフトさせるものです。
- また、異なるAIシステムが全く同じルールとツールを用いて比較できる、公平な競争の場を提供しています。
要約すると: 著者らは、巨大で混沌とした数学ライブラリのリアルなシミュレーションと、それをテストするためのルールを構築しました。その結果、AIは進化しているものの、複雑で現実的な数学プロジェクトを自律的に管理できるようになるには、まだ長い道のりがあることが明らかになりました。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。