FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?

本論文は、大学院レベルの数学問題に対して AI モデルが Lean 4 形式で検証可能な証明を生成できるかを評価するプライベートベンチマーク「FormalProofBench」を提案し、最先端モデルでも最高で 33.5% の精度にとどまり、その性能と課題を包括的に分析したものである。

要約

FormalProofBench の解説：AI は「数学の博士号」レベルの証明を、本当に正しく書けるのか？

この論文は、人工知能（AI）が「数学の証明」をどれだけ上手に書けるかを測る、新しいテスト「FormalProofBench（フォーマル・プローフ・ベンチ）」について紹介しています。

これをわかりやすく説明するために、いくつかのアナロジー（例え話）を使ってみましょう。

1. 従来のテスト vs 新しいテスト：「作文」か「プログラミング」か？

これまでの AI の数学テスト（MATH など）は、**「作文コンテスト」**に似ています。
AI が「答えは 5 です。なぜなら〜という理由があるからです」という説得力のある文章を書けば、人間が「なるほど、正しそうだ」と判断して点数をくれました。
しかし、ここには大きな落とし穴があります。AI は「もっともらしい嘘」をつくのが得意です。論理の飛躍があっても、文章が滑らかなら見逃されてしまうことがあります。

今回の「FormalProofBench」は、**「厳格なプログラミングコンテスト」です。
AI に求められているのは、美しい文章ではなく、「コンパイラ（翻訳機）が通るコード」**です。

• ルール: Lean 4 という特殊な言語で証明を書く。
• 判定: 人間が「うまいね」と言うのではなく、コンピューターが「エラーなしで通ったか（True）」か「エラーが出たか（False）」でしか判断しません。
• 結果: 1 ミリの論理の隙間でもあれば、即座に「不合格（エラー）」になります。これは、AI が「なんとなく正しそう」という嘘をつけない、究極のテストです。

2. テストの内容：大学院生レベルの「難問」

このテストの問題は、高校の数学オリンピックレベルではありません。
**「大学院生が資格試験や専門書で解くような、高度な数学」**です。

• 分野: 解析学、代数、確率論、論理学など。
• 出題元: 実際の大学の資格試験や、有名な教科書から選ばれています。
• 問題数: 200 問。すべて、数学の専門家と Lean の使い手によって、AI が解けるように「正しく翻訳」されたものです。

3. AI の挑戦：「探偵」と「実験室」を駆使する

AI は、ただ答えを出力するだけではありません。このテストでは、AI に**「エージェント（助手）」**のような役割を与えています。
AI は 40 回までの「ターン（試行回数）」を使って、以下の道具を使いながら証明を完成させます。

• 辞書検索（lean_loogle）: 必要な定理や定義を Mathlib（数学の巨大な図書館）から探す。
• 実験室（lean_run_code）: 書いた証明の一部を実際に実行して、「エラーが出たか」「どこが間違っているか」を確認する。
• 提出（submit_proof）: 最終的に完成した証明を提出する。

成功の秘訣は「実験」です。
良い AI は、いきなり完璧な答えを出そうとせず、まず小さなコードを書いて実行し、「あ、ここが間違っていた」というフィードバックを得て、それを修正しながらゴールを目指します。逆に、悪い AI は辞書検索ばかりして、実際に試すことをせず、堂々巡りをして失敗します。

4. 結果：AI はどこまでできるのか？

最新の最強 AI モデルたちをこのテストに挑戦させたところ、結果は以下のようになりました。

• 1 位は Claude Opus 4.5（Thinking）: 正解率は33.5%。
  • これは「100 問中 33 問」しか解けなかったことになります。つまり、6 割以上は失敗しています。
• 2 位以下: 18%、17%、15%... と急激に成績が落ちます。
• 最下位: 3% 台のモデルもいます。

結論:
「すごい AI」であっても、大学院レベルの数学証明を「完全に正しく」書くのは、まだ非常に難しいことがわかりました。33.5% という数字は、AI が「天才」の領域に近づきつつあることを示していますが、まだ「完璧な数学者」にはほど遠い、という現実を浮き彫りにしています。

5. なぜこのテストが重要なのか？

このテストは、AI の「数学力」を測るだけでなく、**「AI が人間の仕事（研究者）のパートナーになれるか」**を測る重要な指標です。

• 信頼性: 人間が「たぶん正しい」と思っても、AI が「厳密に正しい」と証明できなければ、科学の進歩には使えません。
• 未来: もし AI がこのテストで 100% できるようになれば、数学者は「証明のチェック」を AI に任せ、より新しいアイデアの発見に集中できるようになります。

まとめ

この論文は、**「AI は数学の天才になりつつあるが、まだ『厳密さ』という壁にぶち当たっている」**と伝えています。
FormalProofBench は、AI が「もっともらしい嘘」をつけないよう、厳しく、しかし公平に能力を測るための「新しい物差し」なのです。

AI が「大学院生レベルの証明」を完璧にこなせる日は、数学の未来が劇的に変わる瞬間になるでしょう。そのために、このベンチマークが重要な役割を果たしています。

技術概要

FormalProofBench: 大学院レベルの数学証明を形式検証可能な形で記述できるか？

論文の技術的サマリー

本論文は、ICLR 2026 で発表された「FormalProofBench」に関する研究報告です。これは、AI モデルが大学院レベルの数学問題に対して、人間が読める自然言語による解答ではなく、形式検証（Formal Verification）が可能で、機械的に正しさが証明される Lean 4 による証明を生成できるかを評価するためのベンチマークを提案したものです。

以下に、問題定義、手法、主要な貢献、結果、および意義について詳細をまとめます。

---

1. 問題定義と背景

従来の数学的推論のベンチマーク（MATH, GSM8K など）は自然言語による解答を評価対象としており、論理的な飛躍や誤りが人間や他の LLM による評価者に見逃されやすいという課題がありました。また、形式数学の分野では、ProofNet や MiniF2F などのベンチマークが存在しますが、これらは主に高校数学や学部初級レベルに焦点を当てており、より高度な研究レベルの数学を網羅的に評価するものは不足していました。

FormalProofBench は、以下の要件を満たす新しい評価基準を確立することを目的としています。

• 難易度: 大学院レベルの数学（測度論、解析学、代数学、確率論など）。
• 評価の厳密性: 自然言語の「説得力」ではなく、Lean 4 のカーネルによる**コンパイル成功（型チェックの通過）**を正解の唯一の基準とする。
• データ汚染の防止: ベンチマーク問題を非公開（Private）に保持し、学習データへの混入を防ぐ。

2. 手法とベンチマーク構成

データ収集と形式化

• 問題ソース: 資格試験（Qualifying Exams）や標準的な教科書から選定された 200 問。
• 分野: 実解析（56 問）、確率論・確率解析（34 問）、関数解析（26 問）、数論（23 問）、論理・モデル理論（21 問）、代数学（18 問）、代数幾何（15 問）、線形代数（7 問）など。
• 形式化プロセス: 6 名の Lean 4 専門家（PhD 学生やドメインエキスパート）が自然言語の問題を Lean 4 の形式記述に変換。その後、GitHub 上のコードレビュープロセスを通じて、元の意図と形式記述の整合性を確認する「二次レビュー」を実施し、誤形式化（Misformalization）を防ぎました。

評価環境（エージェント・ハarness）

モデルは単発で証明を生成するのではなく、マルチターン・エージェントとして評価されます。

• 入力: 自然言語の問題文、対応する Lean 4 の形式記述（ヘッダーと文脈を含む）。
• ツール:
  • lean_loogle: Mathlib 内の定理や定義を検索。
  • lean_run_code: Lean コードを実行し、エラーメッセージ、未解決のゴール、型不一致などのフィードバックを取得。
  • submit_proof: 最終証明を提出。
• 制限: 問題あたり最大 40 ターン。各ターンで最大 6 回のツール呼び出しが可能。
• 成功条件: submit_proof が呼び出され、提出された証明が Lean 4 カーネル（v4.25.2）によって完全に検証（コンパイル）されること。sorry や公理の乱用は禁止。

3. 主要な貢献

1. 新しいベンチマークの提案: 大学院レベルの数学に特化し、決定論的かつ汚染耐性のある（Contamination-resistant）形式定理証明ベンチマークを構築。
2. 最先端モデルの包括的評価: 200 問の厳密に形式化された問題を用いて、OpenAI、Anthropic、Google、xAI などの最先端モデルを評価。
3. 実用的なエージェント評価: 検索ツールやコード実行ツールを備えたリアルなマルチターン環境におけるコスト、レイテンシ、ツール使用パターンの分析。
4. ツール使用と性能の相関分析: コード実行による反復が成功に寄与し、検索のみの過剰使用が失敗の原因となることを実証。

4. 結果と分析

性能結果

評価されたモデルの中で最高性能を記録したのは Anthropic の Claude Opus 4.5 (Thinking) であり、正解率 33.5% を達成しました。

• 2 位は Gemini 3 Pro (18.5%)、3 位は Claude Sonnet 4.5 (18.0%)。
• 33.5% を超えるモデルは存在せず、その後は性能が急激に低下しました。
• 多くのモデルが 10% 未満の正解率にとどまっており、大学院レベルの形式証明は依然として極めて困難なタスクであることが示されました。

ツール使用パターンの分析

• コード実行の重要性: 成功したモデルは、証明の途中段階で頻繁に lean_run_code を使用し、エラーフィードバックを得て証明を修正・反復する傾向がありました。
• 検索の罠: 失敗したモデルは、存在しない補題を探すために lean_loogle を過剰に呼び出し、スパイラルに陥る傾向が見られました。
• 相関: コード実行の回数が多ければ多いほど、正解率との間に正の相関（ただし modest）が見られました。

コストとレイテンシ

• 1 問題あたりの平均コストは 10 セントから 1 ドル以上と幅広いです。
• レイテンシ（壁時計時間）は、モデルによっては 1 時間以上（平均約 4000 秒〜11000 秒）を要する場合があり、実用的なツールとしての導入にはまだ時間とコストの最適化が必要です。

5. 意義と将来展望

数学的実践への影響

FormalProofBench の結果は、AI が数学者の作業に実用的なツールとなり得る「閾値」に近づきつつあることを示唆しています。形式検証が可能になれば、証明戦略の迅速な探索や、証明助手の専門知識を持たない研究者への形式手法の民主化、研究レベルの数学の形式化加速が期待されます。

今後の課題

• ツールの改良: 現在の検索ツール（Loogle）よりも、意味検索やローカルコードベースの grep、タクティクスレベルのツールが有効かどうかの検証。
• インフォーマル記述の除去: 自然言語のヒントなしで、形式記述のみから証明を生成できるか（翻訳能力と証明生成能力の分離）。
• 研究レベルへの拡張: 現在の Mathlib の限界を超え、より最先端の研究レベルの定理への挑戦。

結論

FormalProofBench は、AI モデルが「それらしい」自然言語の証明ではなく、機械的に検証可能な厳密な証明を生成できる能力を測定するための重要なマイルストーンです。現時点では最高モデルでも 33.5% の正解率にとどまっており、完全な自動化にはまだ課題が残っていますが、コード実行による反復学習が鍵となることが明らかになりました。このベンチマークは、形式数学における AI の進歩を追跡し、将来的に数学研究の標準的なツールとして定着させるための基盤を提供します。