DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent

以下は、論文「DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent」の詳細な技術的概要です。

1. 問題定義

大規模言語モデル（LLM）や Lean などの形式証明アシスタントの進展により、自動定理証明（ATP）は著しく進歩しました。しかし、現在の最先端システムは 2 つの決定的な限界に直面しています。

• 汎化性の欠如: ほとんどのアプローチは、各定理を孤立して扱います。問題を中間段階に分解する場合がありますが、これらの段階は個々の問題に極めて特化しており、異なる定理間で汎化されません。
• 非効率性: 既存の手法は、固定された静的な補題ライブラリに依存するか（適応性の制限）、各問題インスタンスごとに新しい中間補題を合成します。これにより、システムが過去の証明から学習した「スキル」（補題）を蓄積・再利用できないため、冗長な計算、長い証明の長さ、高いトークン使用量が生じます。

本論文は、現在のシステムが、数学者が新しい問題を効率的に解決するために、転移可能な補題のコアセットを体系的に蓄積、抽象化、再利用する人間の数学的実践を模倣できていないと主張しています。

2. 手法：DreamProver フレームワーク

DreamProver は、認知学習理論と DreamCoder アルゴリズムに触発された反復的な「ウェイク・スリープ」パラダイムを通じて、再利用可能な補題ライブラリを学習・進化させるように設計されたエージェント型フレームワークです。このシステムは交互のサイクルで動作します。

A. ウェイク段階（定理の発見と分解）

このフェーズでは、エージェントが現在の補題ライブラリを使用して、トレーニングセットからの定理の証明を試みます。

• 学習可能定理の特定: システムはライブラリを使用して定理を直接証明しようとします。成功した場合、その定理は「学習可能」とマークされ、ライブラリがそのドメインに対して十分であることを示します。
• 中間定理の発見: 定理を直接証明できない場合、システムはそれをより単純なサブ問題（サブ定理）に再帰的に分解します。
  • 形式証明のスケッチを生成します。
  • 証明されていない中間目標（sorry でマークされたもの）をスタンドアロンの定理として抽出します。
  • スケッチと新しい候補を使用して完全な証明を再構成しようとすることで、抽出された定理を検証します。
• 結果: システムは、トレーニングデータから導出された「学習可能定理」（中間結果）のセットを蓄積します。

B. スリープ段階（補題の抽象化とライブラリの最適化）

このフェーズでは、システムは蓄積された経験を処理して補題ライブラリを進化させます。

• セマンティッククラスタリング: システムは、収集された中間定理に自然言語の説明（サブドメイン、難易度、関連概念）を付与します。その後、これらの説明を埋め込み、セマンティック類似性に基づいて K-Means 法でクラスタリングします。
• 補題の抽象化: 各クラスタに対して、LLM がそのクラスタ内の特定の定理を一般化する候補補題を生成するようにプロンプトされます。
• 構造的検証: 抽象化された補題が適用可能であることを保証するため、システムは候補補題とクラスタ内の定理との間の構造的類似性（一次論理式ツリーに対するツリー編集距離を使用）を計算します。類似度しきい値を超える補題は保持されます。
• ライブラリの更新（忘却と重複排除）:
  • 重複排除: 新しい補題は、ツリー編集距離を使用して既存のライブラリと比較されます。非常に類似した（重複する）補題は破棄されます。
  • 忘却: コンパクトなライブラリを維持するために、システムは「Least Recently Used (LRU)」戦略を採用します。ライブラリが容量に達すると、最近のウェイク段階で頻繁に使用されていない補題は切り捨てられます。
  • 検証: 残りの候補補題は、証明可能であることを確認するために形式的に検証されます。

C. 推論

未見のテスト問題に対する推論中、DreamProver は進化させたライブラリを利用します。まず直接証明生成を試みます。それが失敗した場合、ライブラリを使用して証明スケッチの生成とサブゴールの解決を導く「スケッチ・アンド・証明」ワークフローを採用します。

3. 主な貢献

1. ATP 向けのウェイク・スリープパラダイム: 形式定理証明において転移可能な補題ライブラリを進化させるために、連続的かつ反復的なウェイク・スリープサイクルを適用した初の試み。
2. 転移可能な補題学習: 効果的な再利用の証明に苦労した以前の研究（LEGO-Prover など）とは異なり、DreamProver は中間結果を明示的にクラスタリングし、一般的な補題に抽象化することで、永続的で高品質な知識基盤を構築します。
3. 効率化メカニズム: 「忘却」メカニズム（LRU プルーニング）と構造的な重複排除の導入により、ライブラリをコンパクト（100 補題未満）に保ち、コンテキストウィンドウのオーバーフローを防ぎ、高い検索関連性を維持します。
4. ドメイン汎化: LLM のトレーニングデータで過小評価されているドメインを含む、多様な数学ドメインで機能するように設計されています。

4. 実験結果

著者らは、DreamProver を 5 つの数学ドメイン（不等式、数論、組合せ論、平面幾何学、機械学習理論）で評価しました。

• 性能向上:

  • DreamProver は、Hilbert や Goedel-Prover-V2 などの先行する最先端（SOTA）システムと比較して、証明成功率を平均**61%**向上させました。
  • 特定のドメインでは、改善は劇的でした：数論で114%、組合せ論で**50%**の向上です。
  • 過小評価されているドメイン（平面幾何学、ML 理論）では、DreamProver はプロプライエタリな LLM よりもはるかに多くのインスタンスを解決しました（例えば、ベースライン LLM が 0〜3 問しか解けなかったオリンピックレベルの幾何学問題 14〜16 問を解決）。

• 効率性と品質:

  • トークン削減: DreamProver は、SOTA エージェント型システムと比較して、出力トークン使用量を平均**48%**削減しました。
  • 証明の簡潔さ: 生成された証明は平均で**50%**短く、より高い品質と優れた構造を示しています。
  • 補題の再利用: 分析により、トレーニング中に生成された補題の**58%がテストセットで再利用され、成功して証明されたすべての定理の71%**に寄与していることが示されました。

• アブレーション研究:

  • 反復的なウェイク・スリープの洗練（単一パス進化）を除去すると、成功率は大幅に低下しました（解決された問題数が 104 から 76 に減少）。
  • セマンティッククラスタリングを除去すると、巨大で管理不能なライブラリが生じ、ライブラリなしのベースラインよりもさらに性能が低下しました。

5. 意義

DreamProver は、「ワンショット」または「静的ライブラリ」の定理証明から、継続的かつ自己改善的な学習への転換を表しています。

• ギャップの埋め合わせ: LLM の生きた推論能力と、複雑な数学的推論に必要な構造化された再利用可能な知識との間のギャップを効果的に埋めます。
• スケーラビリティ: コンパクトで転移可能なライブラリを学習することで、新しい定理を証明する計算コストを削減し、高度な形式検証をよりアクセスしやすくします。
• 人間のような学習: このフレームワークは、人間の認知プロセス（経験の獲得、原則の抽象化、無関係な詳細の忘却）を模倣しており、より堅牢で汎用性の高い AI 推論システムへの実現可能な道筋を示唆しています。

結論として、DreamProver は、再利用可能な補題のライブラリを明示的に学習し洗練することが、特に複雑でデータが不足している数学ドメインにおいて、自動定理証明における最先端の性能を達成するための決定的な要因であることを実証しています。