AlphaProof
Google DeepMindが開発した「AlphaProof」およびそれを応用した「AlphaProof Nexus」は、大規模言語モデル（LLM）の推論能力と、数学的論理を厳密にチェックする形式言語環境を組み合わせることで機能しています。
AlphaProof
LLMがアイデアを形式証明として生成します。
自動定理証明にかけて妥当なものを選別します。
選別結果で、LLMを強化学習します。
これにより、LLMは数学証明という課題に自律適応します。
AlphaProof Nexus
複雑な問題では、そもそも形式的に妥当な推論を導けない可能性があります。
そこで、推論中の仮説を認め、その仮説の証明を次の問題とする分解を導入します。
また、仮説の有望さを別の審査役LLMと進化計算で評価し、より筋の良い仮説生成を行えるようにします。
https://gyazo.com/690b73c22b846a9531083ef970efbd59
G. Tsoukalas et al., 2026, arXiv preprint arXiv:2605.22763.
Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
1. AlphaProof ：強化学習による数学的推論
AlphaProofは、ボードゲーム（チェスや囲碁など）で棋譜に頼らず人間を打ち破った「AlphaZero」に着想を得ており、数学の証明をゲームのように解く仕組みを持ちます。
具体的には、以下のような仕組みです。
1. LLMがアイデアを生み出し、形式証明として記述します。
2. それらを自動定理証明にかけて妥当なものを選別します。
3. 形式証明を突破できたものを用いて、LLMの推論過程を強化学習により調整します。
4. これにより、LLMは数学問題の証明という課題に対して自律的に適応します。
1.1. Leanによる「証明のゲーム化」
数学の証明は「Lean」という形式言語のプログラミング環境で行われます。 この環境では、現在の仮説や未解決の目標を「状態」、証明を進めるためのLeanコード（tactic）を「行動」と見なします。 より短いステップで証明できた場合に高い報酬が与えられる設定になっており、AIは試行錯誤を通じて最適な手順を探します。
1.2. 証明ネットワークと木探索
AlphaProofの中心には、現在の状態を分析し、「次にどのような手順（tactic）が有望か」と「その証明はどれくらいで解けそうか」を予測するニューラルネットワーク（証明ネットワーク）があります。
このネットワークの予測を基に、複数の手順の先読みを繰り返す「木探索」を行い、証明の正解ルートを見つけ出します。
https://gyazo.com/980b8b898140dae299cf29d1a98f384e
Hubert, T., Mehta, R., Sartran, L. et al. Nature 651, 607–613 (2026).
Creative Commons Attribution 4.0 International License
1.3. データベース作成とLLMの強化学習
自然言語で書かれた約100万の数学の問題をLLMを使ってLeanのコードに自動翻訳（自動形式化）し、約8,000万問の膨大なデータセットを作成しました。
AIはこれらの問題を解く（または反証する）経験を積み重ねることで、自らの能力を強化していきます。
1.4. テスト時強化学習（TTRL）
通常の探索では解けない超難問に直面した際、AIはその問題に関連するバリエーション（条件を少し変えた問題など）を大量に自動生成し、その場で即座に専用の強化学習を行います。
これにより、その特定の問題を解くための高度な適応能力を獲得します。
https://gyazo.com/8b689bf9154a865cd6807acba032d729
Hubert, T., Mehta, R., Sartran, L. et al. Nature 651, 607–613 (2026).
Creative Commons Attribution 4.0 International License
2. AlphaProof Nexus ：進化計算による仮説生成 + Alpha Proofによる証明
AlphaProofは強化学習の枠組みにより、正解に辿り着く最短の手筋を適応的に導きます。
しかし、成功に囚われない突飛なアイデアを生成したり、不正解だが筋の良いアイデアを深掘りしたりする仕組みはありません。
AlphaProof Nexuxは、より困難な問題ではこれらを戦略的に行う必要があるという発想のもと、進化計算に基づく問題分解エージェントを作成し、AlphaProofを証明ツールとして与えるという方策をとります。
具体的には、以下のような背景を持ちます。
1. 複雑で推論ツリーが長くなる問題では、形式的な妥当性を評価できる推論ツリーをそもそも作れない可能性があります。
2. そこで、推論途中に仮説の混入を認め、その仮説の証明を次の問題とする問題分解を導入します。
3. また、仮説の有望さを別の審査役LLMで評価し、進化計算にかけることで、より筋の良い仮説生成を行えるようにします。
AlphaProofが「厳密なルールの中で、正しい論理の道筋を探索する仕組み」としたら、AlphaProof Nexusは「LLMの柔軟な推論力と進化アルゴリズムによるアイデアの選別を用いて、未知の研究課題をAlphaProofが解ける形に分解・整理するシステム」といえます。
2.1. 対話型の証明ループ（Prover Subagent）
（1）Nexusの中心となる証明エージェント（Prover Subagent）はLLMにより構成されます。エージェントは「sorry」というプレースホルダー（まだ証明されていない部分）を含む不完全なLeanのコードを受け取り、それを修正していきます。
（2）Lean（Proof Validator）でコンパイルエラーが出た場合は、そのエラーメッセージを読み取り、論理を修正するという対話的なループを繰り返します。
https://gyazo.com/690b73c22b846a9531083ef970efbd59
G. Tsoukalas et al., 2026, arXiv preprint arXiv:2605.22763.
Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
2.2. AlphaProofのツール化
エージェントが大きな問題を小さな目標（サブゴール）に分割できた場合、そのサブゴールを解くための「ツール」としてAlphaProofを呼び出します。
これにより、複雑な推論はLLMが行い、細かい論理の証明はAlphaProofに任せるといった役割分担が可能になります。
2.3. 未完成な証明を評価する方法
2.3.1. 評価の難しさ
AIが「未完成の証明（アイデア）」を少しずつ進化させて正解にたどり着くための仕組みとして、「ポピュレーションデータベース（Population Database）」と「Eloレーティング（Elo Rating）」を用います。
通常の進化的アルゴリズムでは、「ゴールにどれくらい近づいているか」をスコア化（例：ゴールまであと10%だから90点）して、点数の高いものを残していきます。
しかし、形式言語（Lean）による数学の証明では、「まだ完成していないが、とても筋が良い証明のアイデア」も「筋の悪いアイデア」もLeanは等しく不正解とするため、自動評価が困難でした。
2.3.2. 進化的探索と評価（Eloレーティング）
この問題を解決するために導入されたのが、ポピューレーションデータベースとEloレーティングです。
まず、（3）複数のエージェントが並行して証明のアイデア（スケッチ）を作成し、それらをデータベースに蓄積します。
次に、（4）評価専用エージェントが、それらのアイデアの「明確さ」や「成功の可能性」を比較・評価します。
ポピュレーションデータベース：仮説の蓄積
安全なアイデアの保管場所です。
複数のAIエージェントが並行して証明に挑戦し、「sorry（後で証明する）」が含まれる未完成の証明を大量に作成します。
作成されたスケッチのうち、コンパイルエラーが出ず、元の問題の前提条件などを不正に書き換えていない（安全である）と確認されたものだけが、このデータベースに登録されていき、後で相対評価をつけるために使われます。
Eloレーティング：相対評価
アイデアの「有望さ」を相対評価する仕組みです。
評価に特化した別のAIエージェントの「審査員」を用いて、仮説同士を戦わせて評価をつけます。
審査員AIは、データベースから複数のスケッチをランダムに取り出し、それらを比較してよさそうな方を選びます。
評価基準: 審査員AIは、以下の3つの基準でスケッチを比較し、順位をつけます。
1. 証明戦略の明確さ (clarity of the proof strategy)
2. 残された目標の解決可能性・妥当性 (plausibility of remaining goals)
3. 数学的なアプローチの斬新さ (mathematical novelty)
この「対戦」を何度も繰り返すことで、勝率（評価）が高いスケッチほどEloレーティングが高くなり、逆に筋が悪いスケッチはレーティングが下がっていきます。
2.4. 進化アルゴリズムの適用
アイデアを貯める（データベース）」→「AI審査員が対戦形式で筋の良さを採点する（Eloレーティング）」→「高得点のアイデアをベースにさらに考える」というサイクルを繰り返すことで、正解に近づいていきます。
基本動作
算出されたレーティングに基づき、最も有望なアイデアを選択し、それを親としてさらに新しい証明のアイデアを生成（進化）させていきます。このプロセスを繰り返すことで、AIは徐々に正解（完全にsorryがないコード）へと近づいていきます。
i) 優秀な親を選ぶ
AIは次の証明に挑戦する際、データベースの中からEloレーティングが上位（トップ64など）の優秀なスケッチを「親」として選び出します。
このとき、単に一番スコアが高いものばかり選ぶのではなく、たまにはスコアが低くても新しく追加されたアイデアを試すような工夫（P-UCBという手法）が取り入れられています。 ii) アイデアを拡張する
AIはその「親」のスケッチをベースにして、足りない部分（sorry）を埋めようと新しいコードを書き足します。
iii) データベースへ戻す
新しいスケッチ（子）がコンパイルを通れば、再びポピュレーションデータベースに登録されます。
iv) 再び審査される
審査員AIがその新しいスケッチを他のスケッチと比較し、新たなEloレーティングを与えます。