TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

この論文は、標準的な MathLib 定義に依存せず分析学をゼロから構築した新しいベンチマーク「TaoBench」を導入し、最先端の自動定理証明モデルが MathLib 環境では高い性能を発揮する一方で、定義の枠組みが異なる同等の問題では約 26% 性能が低下することを示し、現在の ATP システムの課題がタスクの難易度ではなく定義枠組みへの汎化能力の限界にあることを明らかにしています。

要約

この論文は、**「AI が数学の証明をする能力は、本当に『汎用的』なのか、それとも特定の『教科書』に依存しているだけなのか？」**という重要な問いに答える研究です。

タイトルは**「TAOBENCH: 自動定理証明 AI は MathLib（標準数学ライブラリ）の枠を超えて一般化できるか？」**です。

以下に、専門用語を排し、日常の例え話を使ってわかりやすく解説します。

---

🏫 1. 背景：AI は「決まった教科書」しか読めない？

現在の AI（特に数学証明ができる AI）は、**「MathLib」という、Lean 4 というプログラミング言語で書かれた「巨大な標準数学の教科書」**で訓練されています。
この教科書には、集合や実数などの定義が、世界中の研究者が合意した「標準的な書き方」で書かれています。

• 現状の AI： この「標準教科書」の問題なら、すごい成績を収めます。
• 問題点： でも、実際の数学者（例えばタオ教授）が新しい研究をするとき、既存の教科書にはない**「自分だけの定義」や「新しい書き方」**を使うことがあります。
  • これを**「独自のカスタム教科書」**と呼びましょう。

疑問： 「標準教科書」で勉強した AI は、「カスタム教科書」の問題も解けるのでしょうか？それとも、書き方が少し違うだけでパニックになってしまうのでしょうか？

🧪 2. 実験：タオ教授の「オリジナル教科書」で試す

研究者たちは、ノーベル賞級の数学者であるテリー・タオ教授が書いた『解析学 I』の Lean 形式化データを使いました。
タオ教授の書き方は、数学的には正しいですが、「MathLib（標準教科書）」とは全く異なる独自の定義や書き方を採用しています。

彼らはこのデータを使って、2 つのテストセットを作りました。

1. TAOBENCH（タオ版）： タオ教授の「オリジナルの書き方」そのもの。
2. TAOBENCHMATHLIB（標準版）： 同じ数学的な問題を、AI が慣れ親しんだ「標準教科書（MathLib）」の書き方に翻訳したもの。

実験の目的：
「同じ数学の問題」を、「書き方（定義の枠組み）」だけ変えて AI に解かせ、どちらが解けるか比較することです。

📉 3. 結果：驚きの「書き方依存症」

結果は非常に明確でした。

• 標準版（MathLib）： AI はよく解けました（正解率 60〜70% 以上）。
• タオ版（オリジナル）： 同じ問題なのに、AI の正解率は平均で 26% も低下しました。

これは何を意味するのでしょうか？
AI が「数学が難しいから」解けなかったのではなく、「教科書の書き方が違うから」解けなかったということです。

🍳 料理の例え：

• 標準版： 「卵焼き」のレシピ（卵、醤油、砂糖、油）。AI はこれを完璧に作れます。
• タオ版： 同じ「卵焼き」ですが、レシピの書き方が「卵を『黄身と白身』に分け、調味料を『甘味料』と呼び、油を『脂質』と呼ぶ」ように書かれています。
• AI の反応： 「卵って何だ？甘味料って何だ？脂質は油のことか？……わからない！作れない！」となって失敗します。

AI は「卵焼きを作る技術（数学的推論）」そのものよりも、「レシピの書き方（定義の形式）」に強く依存していることがわかりました。

🔍 4. 深入り：なぜこうなるのか？

研究チームは、なぜ AI が失敗するのかを詳しく分析しました。

• 文脈（コンテキスト）の罠：
  AI は、問題文と一緒に「必要な定義」を渡されても、それが「見慣れない書き方」だと、それをうまく使いこなせません。
  • 例え話：AI は「新しい道具」を渡されても、「その道具の使い方が教科書に載っていない」と、その道具を無視して、昔から知っている「別の道具」で無理やり解決しようとして失敗します。
• 文脈なしの方がマシな場合も：
  面白いことに、あえて「新しい定義」を渡さず、AI が知っている「標準的な定義」だけで解かせたほうが、かえって正解率が上がることがありました。AI は「新しいルール」を覚えるよりも、「古いルール」で済ませるほうを好む傾向があるようです。

💡 5. 結論と示唆：AI は「研究者」にはなれるか？

この研究の結論は少し寂しいですが、重要です。

「現在の AI は、既存の教科書（MathLib）の中では天才だが、新しい分野（研究数学）で独自の定義を使うと、すぐに能力を発揮できなくなる」

実際の数学の研究現場では、既存の定義に当てはまらない新しい概念を次々と生み出します。もし AI が「書き方」が変わるだけで動けなくなってしまうなら、「研究のパートナー」としては使えないことになります。

今後の課題：
AI を本当に「数学の研究者」として使うためには、特定の教科書の書き方に依存せず、**「どんな定義の書き方でも理解し、使いこなせる力（汎化能力）」**を身につけさせる必要があります。

🌟 まとめ

この論文は、**「AI の数学能力は、実は『暗記』と『慣れ』に支えられており、本質的な理解にはまだ遠い」**という警鐘を鳴らしています。

• 今の AI： 決まった教科書のテストなら満点。
• 本当の天才： 教科書がなくても、新しいルールで遊べる。

これから AI を研究に役立てるには、この「教科書依存症」を治すことが次の大きなステップです。

技術概要

TAOBENCH: 自動化定理証明 LLM は MathLib を超えて一般化できるか？

技術的サマリー

本論文は、現在の自動化定理証明（ATP）用大規模言語モデル（LLM）が、トレーニングデータとして使用されている標準的な数学ライブラリ（MathLib）の定義枠組みを超えた、新しい定義枠組みにおいてどの程度汎用性（一般化能力）を持っているかを検証した研究です。

1. 研究の背景と問題設定

• 現状の課題: 現在の ATP ベンチマーク（MiniF2F など）やトレーニングデータは、Lean 4 の事実上の標準ライブラリである「MathLib」の定義体系に強く依存しています。
• 研究の動機: 最先端の数学研究（探索的数学）では、標準ライブラリに依存せず、問題固有の定義や構成（プロトタイピング）を行うことが頻繁にあります。しかし、MathLib で訓練されたモデルが、MathLib 以外の定義体系（例えば、Terence Tao による『Analysis I』の Lean 形式化のように、基礎から再構築された定義）に対してどの程度頑健（ロバスト）であるかは不明でした。
• 核心的な問い: 数学的な難易度が同等であっても、定義の枠組み（定義の書き方や構造）が変わるだけで、ATP モデルの性能はどの程度低下するか？

2. 提案手法：TAOBENCH と構築パイプライン

著者らは、この問題を評価するための新しいベンチマーク「TAOBENCH」と、それを構築・評価するためのエージェント型パイプラインを提案しました。

2.1 TAOBENCH ベンチマーク

• ソース: Terence Tao の『Analysis I』の Lean 形式化（150 問の演習問題）に基づいています。
• 特徴:
  • Tao 版 (TAOBENCH): 標準的な MathLib の定義に頼らず、集合論、自然数、実数などの核心概念を「ゼロから（from-scratch）」構築した独自の定義体系で記述された問題。
  • MathLib 版 (TAOBENCHMATHLIB): 上記の Tao 版の問題を、数学的に同等な MathLib の標準定義を用いて書き直した対照群（ペアデータ）。
• 目的: 数学的な難易度を一定に保ちながら、「定義の枠組みの違い」のみがモデル性能に与える影響を隔離して評価すること。

2.2 自動構築パイプライン（Agentic Pipeline）

大規模な形式化テキストブックから、コンパイル可能な独立した環境を自動抽出する技術を開発しました。

• コンテキスト抽出: 各問題に対して、必要な最小限の定義、補題、記法を再帰的に取得し、外部依存なしでコンパイル可能なローカル環境を構築します。
• ツール: 「JiXia」という静的解析ツールと、ファイル検索ツール、Lean コンパイラを備えたエージェント（GPT-5 等）を使用。
• 翻訳パイプライン: Tao 版から MathLib 版への翻訳には、2 段階のプロセスを採用しました。
  1. 書き換え: Web 検索機能付きの LLM が MathLib の標準定義を用いて再記述。
  2. 等価性チェック: 両者の証明目標状態（Goal State）を比較し、数学的に同等であることを確認（JiXia と LLM による検証）。
• 人間による検証: 専門家が 33 件の微細な不整合を修正し、最終的なベンチマークの品質を担保しました。

3. 実験結果

複数の最先端 ATP モデル（DeepSeek-Prover-V2, Goedel-Prover-V2, Kimina-Prover など）およびフロンティア基盤モデル（GPT-5.1, Gemini 3 Pro）を評価しました。

• 性能の大幅な低下:
  • MathLib 版（TAOBENCHMATHLIB）では、多くのモデルが 65%〜70% 以上の成功率（Pass@128）を達成しました。
  • 一方、Tao 版（TAOBENCH）では、同じ問題でも平均して約 26% 低下し、多くのモデルで 30%〜40% 台の成功率に留まりました。
  • 例：Goedel-Prover-V2-32B は MathLib 版で 72.67% でしたが、Tao 版では 49.33% でした。
• コンテキスト長の影響:
  • 問題文に含まれる「局所的な定義の数」が増えるにつれて、Tao 版の性能は急激に低下しました（定義数 10 以上で 6% 台まで低下）。
  • 一方、MathLib 版では定義数が増えても性能の低下は緩やかでした。
  • これは、モデルが「文脈内の新しい定義」を適切に統合・推論する能力が不足していることを示唆しています。
• モデルの特性:
  • 専門特化型の ATP モデルは MathLib 枠組みに特化しており、枠組みが変わると性能が崩壊します。
  • 汎用的なフロンティアモデル（GPT-5.1 など）は、ATP 特化モデルよりも Tao 版で高い性能を示しましたが、それでも MathLib 版には及びませんでした。これは、汎用モデルが「文脈内の例（In-context examples）」を扱う能力に優れているためです。

4. 主要な貢献

1. TAOBENCH の提案: MathLib 以外の定義枠組みへの一般化を測定する初の Lean ベンチマーク。
2. TAOBENCHMATHLIB の提供: 数学的に同等な MathLib 版のペアデータを提供し、既存モデルの一般化ギャップを定量的に明らかにした。
3. 自動構築パイプラインの確立: 大規模形式化プロジェクトから、コンパイル可能な独立環境と等価な MathLib 表現を自動生成するスケーラブルな手法を提示。

5. 結論と意義

• 結論: 現在の SOTA ATP モデルは、MathLib 定義枠組み内では高い性能を発揮しますが、定義体系が異なる環境（研究数学でよく見られる状況）では、数学的な難易度が同等であっても性能が著しく低下します。ボトルネックは「問題の難しさ」ではなく、「定義枠組みの一般化能力の欠如」にあります。
• 意義:
  • 現在のベンチマークは、モデルの「数学的推論能力」と「特定のライブラリへの慣れ」を混同している可能性を示唆しています。
  • 実世界の数学研究（探索的・プロトタイピング的）に AI を適用するためには、特定の定義体系に依存しない、より頑健な定理証明モデルの開発が急務であることを浮き彫りにしました。
  • 本論文のデータセットと手法は、将来の研究数学に適合する ATP モデルの開発と評価のための具体的な基盤を提供します。

この研究は、AI による数学的推論の次の段階が、単なる「正解を出す」ことではなく、「未知の定義体系の中で推論する」能力の獲得にあることを示しています。