技術要約：形式的公理系における自己教師あり定理発見

問題提起

近年のAIシステム、特に大規模言語モデル（LLM）は数学的推論において顕著な進歩を示しているが、それらは主に数学的テキスト、コード、既存の定理ライブラリといった人間が提供した事前知識に依存している。極めて重要な未解決の問いが残されている。それは、**「エージェントは、人間による事前知識、既存の定理ライブラリ、あるいは訓練用の問題セットに一切アクセスすることなく、形式的公理系の原始的な規則のみから、有用な定理を自律的に発見できるか？」**という点である。

現在の手法の多くは、推論のブートストラップを行うために、人間が構築した知識に依存している。公理的領域における自己改善型エージェントでさえ、発見された定理の有用性を評価するために外部の判定器に依存することが多い。本論文では、エージェントが単に定理を発見するだけでなく、公理と推論規則のみを用いて、自身の証明探索および外部の推論システムの性能を向上させるために「有用な」定理を特定し、活用できるかどうかを調査する。

手法

1. 形式的設定：スタックマシンとしてのヒルベルト体系

著者らは、問題を命題論理のためのヒルベルト公理系の中に具体化している。このシステムは意図的に最小限の構成となっており、以下で構成される：

• 3つの公理:
  • $Ax1: A \to (B \to A)$ （弱化）
  • $Ax2: (A \to (B \to C)) \to ((A \to B) \to (A \to C))$ （分配）
  • $Ax3: (\neg A \to \neg B) \to (B \to A)$ （対偶）
• 1つの推論規則: モドゥス・ポネンス（MP）、すなわち $X$ と $X \to Y$ から $Y$ を導出する。

学習を容易にするため、著者らは定理証明を決定論的で目標条件付きのスタックマシン決定プロセス $(S, A, s_0, P)$ として定式化している：

• 状態 ($S$): 数式の有限のスタック。
• アクション ($A$): $Ax1, Ax2, Ax3$ のインスタンスをスタックにプッシュする、またはモドゥス・ポネンス（MP）を適用する。
• メカニズム: MPアクションはヒンリー・ミルナー型単一化（unification）を使用する。もしスタックの最上部要素が $X \to Y$ と単一化でき、その下の要素が $X$ と単一化できる場合、両方をポップし、$Y$ をプッシュする。
• 成功: スタックにターゲットとなる目標と一致する単一の数式が含まれていれば、証明は成功とする。

2. 自己教師あり定理発見アルゴリズム

コアとなる貢献は、証明探索と有用な定理の抽出を交互に行い、将来の探索のためのレマ（補題）として機能する定理ライブラリを構築するアルゴリズムである。

A. 目標条件付き方策学習

エージェントは、現在のスタック $S$ と目標 $g$ が与えられたときに次のアクションを予測する方策 $\pi_\theta(A|S, g)$ を学習する。

• ヒンサイト学習（Hindsight Learning）: 探索エピソード中、スタックに単一の数式 $f_t$ が含まれるすべての状態は、それが元の目標であったかに関わらず、「到達した定理」として扱われる。
• 訓練シグナル: $f_t$ に至るアクションの接頭辞（prefix）は、$f_t$ の証明として扱われる。これらの接頭辞は訓練セット $D_{train}$ に追加され、クロスエントロピー損失を介して方策を更新するために使用される。
• 目標バッファ ($G$): バッファは発見された定理を保持する。エージェントは、後続の探索エピソードのために $G$ から一様に目標をサンプリングし、実質的に自身のカリキュラムをブートストラップする。

B. 有用な定理の抽出

ライブラリが些細な、あるいは冗長な定理で膨張するのを防ぐため、アルゴリズムは以下の2つの基準に基づいて発見された定理をフィルタリングする。

1. 汎用性: 定理は、他の候補の特殊化に過ぎないものを排除するためにフィルタリングされる。システムは、数式の代入によって定義される半順序の下での「最小」の要素（すなわち、最も一般的な形式）のみを保持する。
2. 再証明可能性: システムは、現在の方策が現在の定理を再証明できる確率を推定する。ベイズ事後平均（Beta(1,1) 事前分布）を使用し、発見されたものの、再証明が信頼性を持って困難な定理を優先する。これらの「再証明が難しい」定理は、それらをレマとして追加することで困難な証明経路を圧縮できるため、価値が高い。

C. 多世代ライブラリ拡張

プロセスは世代（generation）ごとに動作する：

1. 方策学習: 現在のアクション空間（初期状態では公理とMPのみ）で方策を訓練する。
2. 抽出: 汎用性と再証明可能性に基づいて、発見された定理を特定する。
3. アクション空間の拡張: 抽出された定理を新しいライブラリ・アクション（例：$Thm_1, Thm_2$）として追加する。これらが選択されると、対応する定理をスタックにプッシュし、検証済みのレマとして機能する。
4. 反復: プロセスを繰り返し、エージェントが以前に発見された定理を使用して、より複雑な新しい定理を見つけられるようにする。

主な貢献

1. 定式化: ヒルベット公理と推論規則に直接基づき、スタックマシン決定プロセスとして命題定理証明を定式化しており、外部の証明コーパスへの依存を回避している。
2. アルゴリズム: 原始的な規則のみから定理ライブラリを成長させる、自己教師あり定理発見アルゴリズムを提案している。これは、抽出された定理を後続の証明探索のためのレマとして再利用する。
3. 自律的発見: エージェントは数万個の定理を発見し、人間が作成したベンチマーク問題に対して、人間による事前知識なしに証明を見つけ出す。
4. 転移可能性: 抽出された定理は効果的な外部知識として機能し、それらをプロンプトのレマとして提供された際のLLMの証明性能を向上させる。

実験結果

1. 定理発見とカバー率

• 成長: 発見された定理の数は6世代にわたって増加しており、エージェントが自律的に知識ベースを拡張できる能力を示している。
• ベンチマーク性能: エージェントは、人間が作成したベンチマークセット（クリーネの教科書から派生）の**30%**に対してヒルベルト体系の証明に成功した。
• 比較: 最も強力なベースラインであるGPT-5-highは、支援なしではこれらのベンチマークに対して約23%の精度しか達成していない。エージェントが30%の証明を見つけ出したことは、人間にとって意味のある非自明な証明を発見していることを示唆している。

2. LLMの推論への影響

• プロンプト・レマ: 抽出された定理をGPT-4oやGPT-5のバリアントにプロンプト・レマとして提供すると、ベンチマーク問題に対する証明成功率が大幅に向上する。
• 定性的分析:
  • 発見された定理の中には、よく知られた原理（例：爆発原理 $\neg A \to (A \to B)$）に対応するものがあり、これらは容易に解釈可能である。
  • 他の定理（例：複雑な含意の持ち上げ）は、人間には直ちに明白ではないが、LLMの証明において効果的なサポート知識として機能する。
  • これは、エージェントが人間が明示的に提供していない有用なレマを浮上させることができ、これらのレマが異なる推論アーキテクチャ間（エージェントからLLMへ）で転移可能であることを示している。

意義と主張

本論文は、人間が提供した定理ライブラリに依存することなく、証明探索から有用な定理が創発できるという証拠を提供している。

• 自己進化型AI: 本研究は、すべての発見が公理と推論規則に基づいて厳密に検証可能であることを保証しながら、証明探索を通じて自律的に形式的知識を拡張できる、数学のための自己進化型AIシステムへの道を示唆している。
• 形式的検証可能性: ハルシネーション（もっともらしい誤った記述）を起こす可能性があるLLMとは異なり、エージェントの発見はヒルベルト体系の公理と推論規則に厳密に基づいている。
• 謙虚な姿勢: 著者らは、一般的な推論において最先端のLLMを凌駕したと主張しているのではない。代わりに、制約された形式的な設定において、エージェントが高度なLLMにとっても困難な問題を解決するために、自身の知識を発見・活用する方法を学習できること、そしてその自己発見された知識が外部システムを増強できることを実証している。

本研究は単一の公理系（ヒルベルト命題論理）に限定されているが、著者らはこのフレームワークが、一階述語論理や集合論のようなより豊かな体系にも一般化可能であると考えており、それが今後の研究の方向性となっている。