💬 NLP

Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving

本論文は、数学的テキストから抽出された知識グラフを汎用大規模言語モデルに統合することで自動定理証明を強化し、追加の微調整を必要とせずに複数のデータセットで顕著な性能向上を実現する新たなフレームワーク「KG-prover」を提案する。

原著者： Vincent Li, Tim Knappe, Yule Fu, Kevin Han, Kevin Zhu

公開日 2026-05-26

📖 1 分で読めます☕ さくっと読める

原著者： Vincent Li, Tim Knappe, Yule Fu, Kevin Han, Kevin Zhu

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

論文「Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving」の説明を、簡単な概念と創造的な比喩を用いて分解して以下に示します。

大きなアイデア：数学モデルに「カンニングペーパー」を与える

非常に難しい数学のパズルを解こうとしていると想像してください。あなたは数学に精通した超賢い友人（大規模言語モデル、LLM）を持っていますが、特定の規則を思い出せなかったり、2 つの異なるアイデアがどのように結びつくのか見抜けなかったりするため、ときどき行き詰まることがあります。

通常、これらの友人をより賢くするためには、彼らを何年ものトレーニング（ファインチューニング）のために学校に戻さなければなりません。しかし、この論文はこう言います。「追加の学校は不要だ！」代わりに、彼らが問題に取り組んでいる最中に、より良い地図とより良い図書館を与えるだけでよいのです。

著者たちはKG-Proverと呼ばれるシステムを構築しました。これは、あなたの賢い友人に数学的事実の巨大で相互接続されたウェブ（知識グラフ）を与え、パズルを解こうとしている最中にリアルタイムで正しい手がかりを「検索」させるようなものです。

仕組み：探偵の比喩

AI を犯罪（数学の定理）を解決しようとする探偵だと考えてみましょう。

犯罪現場（問題）：探偵は真実であることを証明する必要がある声明を与えられます。
図書館（知識グラフ）：著者たちはProofWiki（数学的証明でいっぱいのウェブサイト）から膨大な図書館を構築しました。この図書館を、すべての数学的概念がノードであり、それらを結ぶ線がそれらの関係を示す（例：「定理 A は定義 B を使用する」）巨大な蜘蛛の巣に変換しました。
捜査（探索）：
- 推測する代わりに、探偵は蜘蛛の巣を見ます。
- 彼らは犯罪現場から始め、「これに関連する者は誰か？」と尋ねます。
- 彼らは線に沿って進み、類似した概念、定義、以前の証明を見つけます。
- 行き詰まっても諦めず、隠された手がかりを見つけるためにさらに多くの線を追ってウェブの奥深くへ進みます。これは「テスト時計算の拡張」と呼ばれ、基本的に答えを見つけるために捜査中に時間と労力をより多く費やすことを意味します。
草案（非公式な証明）：探偵は発見した手がかりを用いて、平易な英語（自然言語）で解決策のラフな草案を書きます。
翻訳（形式化）：専門の翻訳者（別の AI）がその英語の草案を受け取り、厳格でコンピュータが読み取れるコード（Lean 4）に変換します。
審判（検証）：厳格な審判がコードをチェックします。間違っていれば、探偵は何が間違っていたかについてのヒントを受け取り、蜘蛛の巣に戻って新しい手がかりを見つけ、再度挑戦します。

機能する「カンニング」

この論文は、この「検索と取得」のプロセスを行うことで、AI モデルを再トレーニングする必要がなかったと主張しています。彼らは既存の汎用モデル（GPT-4o-mini や Llama 3 など）を使用し、地図を利用させるだけで済ませました。

結果：

スコアの向上：この「蜘蛛の巣の地図」を追加したところ、数学問題における AI の成功率は大幅に向上しました（テストに応じて 2% から 21% 増加）。
「深掘り」効果：AI がグラフの奥深く（より多くの接続を追って）検索することを許容されればされるほど、難しい問題を解く能力は向上しました。これは、「1 分で解けなければ、10 分かけて図書館のすべての関連書籍を見て回れ」と言っているようなものです。
追加トレーニングなし：最大の勝ちは、新しいモデルをトレーニングするために数百万ドルを費やす必要がなかったことです。彼らは単に、古いモデルに作業中に使用するより良いツールを与えただけでした。

限界（探偵が行き詰まる場所）

この論文は、この手法が失敗する場所について率直に述べています。

翻訳のギャップ：探偵が完璧な英語の説明を書いても、翻訳者がそれを厳格なコードに変換する際に失敗することがあります。数学的な論理は正しかったものの、コンピュータ言語の「文法」が間違っていたのです。
欠落した手がかり：答えに ProofWiki には含まれていない非常に難解な数学的事実が必要な場合、探偵がどれだけ深く検索しても、それを見つけることはできません。
ノイズの多さ：蜘蛛の巣があまりにも散らかっていると、探偵は無関係な情報に混乱させられる可能性があります。

まとめ

この論文は、AI 数学の専門家たちを再トレーニングすることなく賢くする方法を紹介しています。これは、天才的な学生に完璧で相互接続された百科事典を搭載したスマートフォンを与え、「時間をかけて、必要なすべての関連事実を検索し、証明を書け」と伝えるようなものです。テスト中に AI に「より深く考えさせ」、知識グラフの奥深くまで検索させることで、より多くの問題を正しく解決できるようになります。

技術的概要：自動定理証明のための自然言語グラフベース推論時計算の拡張

問題定義

大規模言語モデル（LLM）は多段階の論理的推論において能力を示しているが、自動定理証明は依然として課題を抱えている。具体的な障壁には、重要な数学的概念の正確な特定、それらの相互関係の理解、自然言語または形式システム内での証明の適切な形式化が含まれる。既存のアプローチは、しばしば集中的なファインチューニング、専門家の反復、または大規模な形式データ（例：Lean）を用いた学習に依存しており、リソース集約的であり、モデルがより広範な非公式数学的知識を活用する能力を制限する可能性がある。さらに、純粋に形式的なアプローチは自然な推論の柔軟性に苦しみ、純粋に自然言語のアプローチは形式検証システムへの変換時に曖昧さに直面する。

手法：KG-Prover

著者は、証明の構築と形式化のために信頼性の高い数学テキスト（具体的には ProofWiki）から抽出された知識グラフ（KG）を汎用 LLM に付加する新しいフレームワーク KG-Prover を導入する。このシステムは、ベース LLM の追加ファインチューニングなしに動作し、代わりに推論時計算の拡張と検索拡張生成（RAG）に依存する。

中核コンポーネント

知識グラフの構築:
- ソース: グラフは ProofWiki を解析して構築され、「定義」「公理」「証明」などの名前空間からノードを抽出する。
- 構造: 各ノードは、自己完結型の数学的命題（定理の命題や定義など）を表す。エッジはテキスト内で発見されたハイパーリンクを表し、依存関係や概念的関係を捉える。
- 規模: 生成されたグラフは 6 万を超えるノードと 30 万を超えるエッジを含む。
- 埋め込み: ノードは、意味的検索を容易にするために、事前計算された埋め込みベクトル（text-embedding-3-large を使用）で拡張される。
推論パイプライン:
- 検索とトラバース: 命題 $P$ が与えられると、システムはその埋め込みを計算し、最も類似した上位 $k$ 個のノードを検索する。初期の証明試行が失敗した場合、システムはグラフを深度 $d$ までトラバースして文脈を反復的に拡張し、以前に訪問したノードの上位 $k$ 個の隣接ノードを選択する。
- 非公式証明の生成: LLM は、検索された文脈を使用して、非公式の自然言語証明を生成する。これは、モデルの創発的な推論能力と KG に存在する広範な非公式証明のコーパスを活用する。
- 自動形式化: 別のモデル（DeepSeek-Prover-V1.5）が、非公式証明を Lean 4 コードに変換する。
- 検証と洗練: 生成された Lean コードは Lean 4 定理証明器で検証される。検証が失敗した場合、エラーメッセージは洗練のために自動形式化モデルにフィードバックされる。証明が依然として失敗する場合、システムはグラフトラバースの深度を増加させたり、探索戦略を採用したりする可能性がある。
拡張戦略（推論時計算）:
- Best-of-N: システムは $n$ 個の独立した非公式証明を生成し、それらを自動形式化し、正しさと明瞭さに基づいてそれらをスコアリングする専用の「ジャッジ」モデルを使用して、最高スコアの候補を選択する。
- ビームサーチ: 証明候補は幅 $w$ のビームに編成される。各ステップで、候補は検証器のフィードバックに基づいて拡張され、スコアリングされ、上位 $k$ 個が次の反復のために保持される。これは、多様な証明経路の探索と検証駆動型の洗練のバランスを取る。

主要な貢献

KG-Prover フレームワーク: 非公式証明の自然言語生成を、反復的な知識グラフベースのトラバースと LLM-as-a-judge メカニズムと統合し、専門的なトレーニングや専門家の反復を不要にするシステム。
大規模数学 KG: 数学的概念間の複雑な関係をモデル化する 6 万を超えるノードと 30 万を超えるエッジを持つ ProofWiki からの知識グラフの構築。
反復的洗練システム: ベースラインに対して最大 26.4%、非拡張 KG-Prover 構成に対して 21.8% の性能向上をもたらすヒューリスティック評価とビームサーチメカニズム。
推論時スケーリングの証明: 基礎モデルの再トレーニングなしに、グラフトラバース深度の調整と探索戦略（Best-of-N、ビームサーチ）の採用が性能を大幅に向上させるという証拠。

実験結果

このフレームワークは、miniF2F-test、ProofNet、MUSTARDSAUCE の 3 つのベンチマークで評価された。

性能向上:
- KG-Prover は、すべてのデータセットにおいてベースラインシステムおよび標準的な検索拡張生成（RAG）を一貫して上回った。
- 複数のモデル（Llama 3.1 8B、GPT-4o、o1-mini など）において、ベースラインに対して 2% から 11% の改善が見られた。
- miniF2F-test において、汎用 LLM は KG-Prover と組み合わせることで最大 21% 改善した。
- o4-mini を用いた KG-Prover の構成は、miniF2F-test で 50% の合格率达到した。
- 最高レベルの拡張構成では、ベースラインに対して 26.4% の改善に達した。
スケーリング効果:
- トラバース深度: 精度はトラバース深度（ $r$ ）の増加に伴い向上し、特に Llama 3.1 8B などの小規模パラメータモデルで顕著であった。最初の数回の深度増加が最も大きな利益をもたらした。
- 探索戦略: KG にビームサーチと Best-of-N サンプリングを組み合わせることで精度がさらに向上し、ProofNet で 10.75%、MUSTARDSAUCE で 50.40% を達成した。
- ファインチューニング済みモデル: Lean 用に既にファインチューニングされたモデル（TheoremLlama、DeepSeek-Prover-V1.5 など）に適用した場合でも、KG-Prover は追加の性能向上をもたらした（例：miniF2F においてファインチューニング済みベースラインに対して +1.85%）。

意義と主張

本論文は、KG-Prover が追加のファインチューニングや集中的な専門家の反復を必要としない、有望でスケーラブルな自動定理証明のアプローチを提供すると主張している。汎用 LLM の組み込み自然言語推論能力を活用し、構造化されたグラフ検索情報によってそれを拡張することで、このフレームワークは非公式推論と形式検証の間のギャップを効果的に埋める。

著者は、この手法により、既存の基盤モデルが推論中に関連概念を注入するだけで、専門的なファインチューニング済みシステムと同等かそれ以上の性能を達成できることを強調している。この研究は、複雑な推論タスクにおいてモデルパラメータの拡張に代わる viable な代替手段として、推論時計算のスケーリング（グラフトラバース深度の調整と探索戦略の採用）の可能性を浮き彫りにしている。このアプローチは非公式から形式への翻訳段階に課題をもたらすが、グラフ検索によって支援される 2 エージェントシステム（生成＋自動形式化）はこれらの問題を効果的に緩和し、解釈可能な推論トレースと証明生成の新しい戦略を提供している。