🤖 machine learning

VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving

本論文は、Best-of-Nおよびクリティック誘導型MCTSプロトコルによる二段階のプロセスを通じて、豊かな検証器信号を探索プロセスへと回帰させることで形式的な定理証明を強化するゼロショットフレームワークであるVERITASを紹介しており、miniF2Fや新たな組合せ論データセットといったベンチマークにおいて最先端の性能を達成している。

原著者： Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang

公開日 2026-06-19

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

CC BY 4.0

原著者： Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, Yifan Zhang

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

あなたは、非常に難しいパズル（複雑な数学の問題など）を解こうとしているところだと想像してください。しかし、あなたはAIアシスタントのチームと一緒にその問題に取り組んでいます。通常、これらのAIアシスタントが問題を解こうとする際、彼らは解決策を推測し、それが機能するかどうかを確認しますが、もし失敗した場合、単に「いいえ、やり直してください」という単純な信号を受け取るだけです。彼らは、なぜ失敗したのかという詳細な理由をすべて捨て去ってしまうのです。

VERITASは、このゲームのルールを変える新しいシステムです。単に「ノー」と言う代わりに、それは証明が失敗した具体的な理由を聞き取り、その理由を用いて次の推測を導きます。これは、単に「容疑者は無実です」と言うのではなく、「容疑者は午後5時に店にいたので無実です。ですから、他に店にいた人を探しましょう」と言う探偵のようなものです。

VERITASの仕組みを、シンプルな要素に分解して説明します：

1. 4人のスペシャリストによるチーム

VERITASは、単一のAIの脳に頼るのではなく、互いに連携する4つの特化した「エージェント」を使用します。

ストラテジスト（戦略家）: 問題を解く前に、このエージェントは高度な計画を決定します（例：「ケース分けをして分解してみよう」や「背理法で証明してみよう」など）。これにより、探索範囲を絞り込み、悪いアイデアに時間を浪費しないようにします。
リトリーバー（検索者）: このエージェントは図書館員のようです。現在のステップを解決するのに役立つ可能性のある、正しい参照書（数学の規則や補題）を素早く見つけ出します。
タクティシャン（戦術家）: これがメインの作業員です。実際の証明のステップを書こうと試みます。極めて重要なのは、これが以前の失敗した試行のリストを確認することです。もし以前の試行が、ルールの名前を間違えたために失敗した場合、タクティシャンには「その名前を二度と使わないでください。ここにエラーメッセージがあります」と伝えられます。
クリティック（批評家）: このエージェントはコーチのような役割を果たします。コンピュータによる数学のチェックに基づき、「近づいていますよ」あるいは「行き止まりに向かっていますよ」といったフィードバックを行い、進捗を監視します。

2. 2段階のゲームプラン

システムは効率化のために、2つの明確なラウンドでゲームを進めます。

フェーズ1：「クイック・スウィープ（素早い掃射）」（Best-of-N）
チームは、独立した5つの素早い解決策を提示します。もしそのうちの一つがうまくいけば、素晴らしい！そこで終了します。これは高速であり、「簡単な」問題に対処するためのものです。
フェーズ2：「ディープ・ダイブ（深い探索）」（Critic-Guided Search）
クイック・スウィープが失敗した場合、システムはより慎重なモードに切り替わります。フェーズ1から得られたすべてのミスを取り込み、それを「負の例」としてタクティシャンにフィードバックします。
- 比喩: 鍵のかかったドアを開けようとしている場面を想像してください。フェーズ1では、5つの異なる鍵を素早く試します。どれも合いません。フェーズ2では、単にランダムに鍵を試すのではなく、5つの鍵がどのように鍵穴に詰まったのかを正確に観察し、その情報を使って、鍵穴の特定の形状に合う新しい鍵を作り出すのです。

3. なぜこれが重要なのか：「組合せ論」の問題

論文では、このシステムを2種類の数学問題でテストしました。

標準的な数学問題: VERITASは、従来の手法よりも多くの問題を解決しました（40.6% 対 36.9%）。
組合せ論（数え上げの問題）: ここでVERITASは真価を発揮しました。これらの問題では、数学の規則に対して非常に具体的かつ正確な名前を使う必要があります。
- 問題点: 標準的なAIの推測は、存在しないルールの名前を「ハルシネーション（幻覚）」として作り上げてしまうことがあります。AIが架空のルール名を推測した場合、標準的なシステムは単に「失敗」と表示して次に進むだけです。
- VERITASによる解決: VERITASは、エラーメッセージ（例：「未知の定数 'X'」）を読み取るため、リアルタイムで「'X' は存在しない」ということを学習します。そして、正しい名前が見つかるまで反復的に修正を行います。
- 結果: 標準的な推測は、試行を重ねるほど（架空の名前を作り続けるため）成績が悪化しましたが、VERITASは失敗から学ぶことで、成績が向上しました。

4. 「単調性」の保証

著者たちは、VERITASが一度見つけた解決策を失わないように設計しました。

保証: もし「クイック・スウィープ（フェーズ1）」が問題を解決した場合、VERITASはその解決策を保持し、手を触れません。「ディープ・ダイブ（フェーズ2）」は、フェーズ1が解決できなかった問題に対してのみ動作します。
なぜ重要か: これにより、VERITASが達成した追加の成功が、単なるランダムな試行回数の増加によるものではなく、フィードバック駆動型のスマートな探索によるものであることが証明されます。

5. 「バッチ」のトリック

論文における巧妙なエンジニアリングのトリックの一つは、答えの確認方法です。

古い方法: 1つの推測をチェックし、コンピュータが「ノー」と言うのを待ち、次の推測をチェックし、待つ……という方法です。これは非常に遅いです。
VERITASの方法: 6つの推測を1つのファイルにまとめ、コンピュータにそれらを一度にまとめてチェックさせます。これにより、システムは約10倍から20倍速くなり、時間とコストを大幅に節約できます。

まとめ

VERITASは、コンピュータのエラーメッセージを単なる「停止信号」ではなく、**「地図」**として扱うシステムです。証明が失敗した具体的な理由（構文エラー、型の不一致、ステップの欠落など）を読み取り、その情報を次の試行へとフィードバックすることで、他のシステムが諦めてしまうような困難な数学問題を解決することができます。これは、高速な「試行錯誤」のアプローチと、スマートな「失敗から学ぶ」アプローチを組み合わせたものです。

技術要約: VERITAS: ゼロショット形式定理証明のための検証器誘導型証明探索

問題提起

現在の大規模言語モデル（LLM）ベースの形式的定理証明器は、形式的検証器（Lean 4など）からの豊かで構造化された信号を、通常、バイナリのパス/失敗という結果へと崩壊させてしまいます。検証器は、構文エラー、型不一致、部分的なゴールの進捗、および証明の完了ステータスを含む粒度の高いフィードバックを提供します。しかし、標準的なパイプラインでは、これらの中間生成物を要約してスカラー報酬に変換するか、あるいは完全に破棄してしまいます。これにより、探索アルゴリズムは、検証器がすでに明示的に提供している情報を「再学習」することを強いられます。この制限は、各ステップの正当性が前のステップによるゴールへの影響に依存するような、連鎖的なタクティクスの連鎖を必要とする証明において、特にコストが高くなります。

手法: VERITAS フレームワーク

VERITASは、すべての検証器信号を証明生成プロセスへとルーティングするように設計された、ゼロショット・フレームワークです。これは、共有された証明状態と2フェーズの探索プロトコルによって調整される、4エージェント・アーキテクチャを採用しています。

1. 特化した4つのエージェント

すべてのエージェントは、定理、現在のゴール、仮定、タクティクス履歴、およびLeanからの4つの構造化された信号を含む共有の ProofState 上で動作します。

Strategist（戦略家）: 証明状態を6つの高レベルな戦略（直接、帰納、矛盾、ケース分け、書き換え、lemma_apply）のいずれかにマッピングし、深さを推定することで、探索範囲を関連する部分空間に制限します。
Retriever（リトリーバー）: ゴール・トークン、レマ名、およびシグネチャに対するキーワードの重複スコアに基づき、関連するMathlibの前提を提示します。
Critic（批評家）: 部分的な証明状態をスコアリングする軽量モデルであり、次のタクティクスを提案し、枝刈りの推奨を行います。これは、MCTSにおけるランダムなロールアウトを、Leanの4方向のフィードバックを統合した価値推定に置き換えるものです。
Tactician（タクティシャン）: 戦略、リトリーブされた前提、Criticのガイダンス、そして決定的な要素として、特定のLeanエラーメッセージを負例として注入された「過去に失敗したタクティクスのリスト」を条件として、 $K$ 個のタクティクス候補を生成します。

2. 単調性を保証する2フェーズ・プロトコル

このフレームワークは、フィードバック駆動型の探索による利得を明確にするために、保守的な2フェーズ・プロトコルを利用します。

フェーズ1 (Best-of-N): 標準的なBest-of-Nスイープ（例： $N=5$ ）を行い、一括でタクティクスを生成します。いずれかが成功した場合、直ちに定理は解決されます。
フェーズ2 (Critic-Guided MCTS): フェーズ1が失敗した場合にのみ起動します。フェーズ1の失敗集合（タクティクスとそのエラー）は、負例としてTacticianのシステムプロンプトに注入されます。Criticは以下の要素を含むモンテカルロ木探索（MCTS）をガイドします。
- 選択 (Selection): Criticの価値と戦略の一致度を組み込んだ拡張されたUCB公式を使用します。
- 展開 (Expansion): エージェントは逐次的に実行され、候補はバッチ化されたLean検証 (Batched Lean Validation) によって検証されます。
- シミュレーション (Simulation): ランダムなロールアウトを、構造化された信号（ $\sigma_A$ 構文、 $\sigma_B$ 型、 $\sigma_C$ 進捗、 $\sigma_D$ 完了）によって増強されたCriticの価値に置き換えます。
- バックプロパゲーション (Backpropagation): バイナリの勝敗に集約するのではなく、構造化された信号を上方へ伝播させることで、部分的な進捗に対するクレジットを保持します。

バッチ化されたLean検証: 展開ごとにLeanを $K$ 回呼び出す代わりに、候補を単一の .lean ファイル内のプライベートな定理としてコンパイルし、一度の呼び出しで検証します。これにより、検証コストを $O(K)$ から $O(1)$ に削減し、約10倍の高速化を実現します。

単調性: このプロトコルは、最終的な解決済み定理の集合がフェーズ1のみで解決された集合の超集合となること（ $S \supseteq S_1$ ）を保証します。これにより、フェーズ2の貢献を分離し、追加の解決が厳密に検証器によるMCTSによるものであることを保証します。

主な貢献

ゼロショット4エージェント・フレームワーク: トレース・ファインチューニングなしに、構造化されたLeanのフィードバック（構文、型、進捗、完了）をすべての生成決定にルーティングするシステム。
2フェーズ・プロトコル: フェーズ1の単独での解決による貢献を明確に分離できる、内部的な単調性保証を備えた Best-of-N $\to$ Critic-MCTS 設計。
効率化の最適化: 検証オーバーヘッドを約10倍削減するバッチ化されたLean検証トリック。
VERITAS-CombiBench: アンガイドなサンプリングの限界を露呈するためにリリースされた、Lean 4による55個の著者検証済み、難解な組合せ論定理からなる新しいベンチマーク。
属性分析: 11個のminiF2F定理が、フラットなサンプリングでは到達できなかったMCTSフェーズによってのみ一意に解決可能であったという実証的証拠。

実験結果

実験は miniF2F (244定理) および VERITAS-CombiBench (55定理) に対して行われました。

miniF2F の性能: VERITASは 40.6% の解決率（99/244）を達成し、独立したBest-of-5ベースライン（36.9%）および手作りのポートフォリオ（26.2%）を上回りました。
- フェーズ2は、主に2〜4つの依存的なタクティクスを必要とする問題において、フラットなサンプリングでは到達できなかった11個の一意の解決に貢献しました。
- 「困難な」non-sorry問題において、VERITASは28.9%に達し、Best-of-5の25.9%を上回りました。
VERITAS-CombiBench の性能: このベンチマークは、アンガイドなサンプリングの失敗を浮き彫りにしました。Best-of-5は、LLMが誤ったMathlibのレマ名を幻覚（ハルシネーション）したため、ポートフォリオ（3.6%）を下回る 1.8% しか達成できませんでした。VERITASは、Leanのエラーフィードバックを用いてこれらの名前を反復的に修正することにより、7.3% に到達しました。
効率性: VERITASは推論のみの手法におけるパレート境界を支配しており、APIコストが1スィープあたり約$150、1定理あたり約27回のLean呼び出しで40.6%の解決率を達成しています。
失敗モード: 失敗の32%は構文レベル（名前の幻覚）、17%は型は正しいが誤っているもの、そして10%は「ニアミス」（部分的なゴール進捗）であり、これらはCriticが高価値なガイダンスを提供できる領域でした。

意義と主張

本論文は、一般的な設計原則を提示しています：決定論的な検証器が構造化された中間信号を放出する場合、それらを生成へと折り返すことは、追加のサンプリングを行うよりも大幅にLLMを増幅させる。

VERITASは以下を実証しています：

検証器信号は「状態」である: 決定論的な検証器信号は、単なる最終チェックではなく、推論時の「状態」として機能し得ます。
コンポーネントの相乗効果: 検証器と生成を密接に結合することは、LLMまたは探索コンポーネントのいずれかを単独でスケールさせるよりも効果的です。
反復的な修正: 精密なレマのリトリー（組合せ論のような領域）を必要とするドメインでは、フラットなサンプリング（語彙的に誤った名前を幻覚する傾向がある）よりも、検証器のエラーからの反復的な修正の方が優れています。

著者らは、VERITASがIMOレベルの創造性やインタラクティブなレイテンシに対する特効薬ではないものの、その主要な貢献は「ルーティング」にあると結論付けています。すなわち、フェーズ1で容易な証明を効率的に収集し、検証器の失敗が次のタクティクスを導ける場合にのみ、フェーズ2で計算予算を費やすことです。今後の課題として、リトリーバルの改善、より安価なCriticの作成、およびフェーズ2のトレースを蒸留して、残りの困難な問題群に対してこの原理をスケールアップさせることが挙げられています。