技術要約：厳密なステップレベル検証による研究レベルの数学的証明の評価

問題定義

大規模言語モデル（LLM）やAIエージェントは、数学的問題解決において顕著な能力を示しているが、複雑な研究レベルの証明を厳密に検証することには苦慮している。標準的なグローバル評価アプローチは、「コンテキスト・ポイズニング（文脈汚染）」の問題に陥る。これは、一見もっともらしい記述が微細な論理的欠陥を隠蔽してしまう現象であり、その結果、エージェントが妥当性を幻覚（ハルシネーション）として認めたり、あるいは過度な懐疑心を示したりする原因となる。形式検証システム（Leanなど）は絶対的な保証を提供するが、その適用は人間によるインフラ構築や手動で維持されるライブラリによってボトルネックが生じており、自然言語による新規または最先端の数学を検証する上での有用性が制限されている。現在のエージェントには、外部の形式化に依存することなく、探索フェーズにおいて、妥当な推論と欠陥のある論理を区別する固有の能力が欠けている。

メソドロジー

本論文は、グローバルな異常検知から、構成的な精緻化（constructive elaboration）による厳密なステップレベルの検証への転換を提案する。コアとなるメソドロジーは、検証タスクを再定義することである。すなわち、エージェントに対し、単一のモノリシックなテキスト内の欠陥を見つけるよう求めるのではなく、あらゆる演繹ステップをより微細な導出へと明示的に展開させるタスクを与える。

三部構成の説明フレームワーク

厳密性を強制し、幻覚を防ぐために、本フレームワークは、任意の演繹ステップ $s_i$ の論理的依存関係を三部構成のアーキテクチャ $(\Gamma_i, \Sigma_i, T_i)$ を用いてモデル化する：

1. ローカル・コンテキスト ($\Gamma_i$): 証明テキスト $S$ から直接由来する、定理、定義、仮定などの有限の文集合。
2. 外部知識 ($\Sigma_i$): 外部文献や確立されたドメインのコンセンサスから引き出される非自明な記述。エージェントは、存在しない定理の幻覚を防ぐために、これらを明示的に引用または証明しなければならない。
3. 背景理論 ($T_i$): 自明な記述、基本的な論理公理（例：モーダス・ポネンス）、および構文的導出に必要な書き換え規則。このコンポーネントにより、厳格な代数的階層に縛られることなく、健全な記述を直接操作することが可能になる。

ステップは、$\Gamma_i \cup \Sigma_i \vdash_{T_i} a_i$（ここで $a_i$ はステップのアサーション）を満たす説明が存在する場合にのみ、妥当であるとみなされる。

ステート駆動型エージェント・ワークフロー

検証プロセスは、各ステップに対して離散的な認知状態 $c_i \in \{OPEN, VERIFIED, FLAWED\}$ 上で作動する、自律的なステート駆動型エージェントとして実装される：

• 初期化: すべてのステップは $OPEN$ から開始される。
• 精緻化（Elaboration）: エージェントは、$OPEN$のステップを詳細な導出へと展開することを試み、$(\Gamma_i, \Sigma_i, T_i)$ を明示的に抽出する。
• 状態遷移:
  • $OPEN \to VERIFIED$: 精緻化が論理的に閉じており、$\Sigma_i$ 内のすべての外部項目が直接的な副証明または正確な引用によって支持されている場合にのみ発生する。
  • $OPEN \to FLAWED$: 明示的な「欠陥の証拠」（例：誤った記述、無効な推論、または適用ミスのある定理）が特定された場合にのみ発生する。
  • 欠陥の確認: 些末な過剰拒絶を防ぐため、予備的な $FLAWED$状態は敵対的な調査をトリガーする。もし感知された欠陥が、論理的な崩壊ではなく、エピステミックな曖昧さ（例：明文化されていないドメインの慣習）であると判断された場合、ステップは$OPEN$ に戻る。
• 停止基準: プロセスは、グローバルな受理（すべてのステップが $VERIFIED$）、決定的な拒絶（欠陥が確認された）、または枯渇（進展のない5回の連続イテレーション）のいずれかによって終了する。

エージェントは**定理台帳（Theorem Ledger）**を維持し、外部の主張のステータスを追跡することで、未検証の仮定に基づいてダウンストリームの推論が検証されないようにする。

主な貢献

1. メソドロジーのパラダイムシフト: 本論文は、自然言語による証明検証を、ブラックボックス的な異常検察から構成的な精緻化へと再定義する。エージェントに対し、$(\Gamma_i, \Sigma_i, T_i)$ フレームワークを通じて論理的依存関係を明示的に追跡させることで、表層的なパターンマッチングとコンテキスト・ポイズニングを緩和する。
2. 自律的検証ワークフロー: 固定された確認フェーズと堅牢な停止基準を備え、論理的完全性よりも論理的健全性を優先する、ステート駆動型のエージェント・フレームワークを提案する。これにより、推論時計算量（inference-time compute）を活用して、微細なエラーを孤立させることに成功している。
3. マイクロベンチマークによる実証的知見: 明確なグラウンドトゥルースを持つ、21件の研究グレードの証明（FirstProofチャレンジより抽出）からなる精選された診断スイートを導入する。評価の結果、標準的なベースラインが、無効な証明におけるカモフラージュされたエラーの検出に失敗する一方で、提案手法は偽の受理（False Acceptance）をゼロに抑えられることが明らかになった。逆に、有効な証明の拒絶は、主に「ペダンティックな過剰厳格さ（pedantic hyper-rigor）」に起因しており、これは未記載のドメイン慣習に関するものであり、検証ロジックの失敗ではなく、ベースモデルの脆弱性を浮き彫りにしている。

結果

フレームワークは、11の有効な証明と10の無効な証明を含む21件の証明スイートを用いて評価された。

• ベースラインの性能: 標準的なグローバル評価器（Global GPT-5.4, Global Codex）および文単位のアブレーションは、深刻なシステム的脆弱性を示した。これらは、構造的には厳格だが数学的には空虚なテキストに欺かれることにより、無効な証明を頻繁に受理（偽陰性）し、また標準的な記法慣習のギャップを幻覚することで、有効な証明を拒絶（偽陽性）した。
• エージェントの性能: 構成的検証エージェントは、**無効な証明の100%**において致命的な演繹的欠陥を特定し、孤立させることに成功した。有効な証明については、11件中8件を正しく検証した。3件の有効な証明の拒絶は、論理的な欠陥によるものではなく、人間がデフォルトで想定するような、暗黙のドメイン慣習（例：特定のリー群の文脈における部分群の線形性）を推論できないことに起因していた。
• 堅牢性: バリアンスを示したベースラインとは異なり、エージェントはマクロレベルの整合性を示し、独立した実行間で同一の最終判定をもたらした。

意義と主張

本論文は、エージェントに慎重で人間数学者に近い方法で検証ノートを整理させるプロンプトが、厳密な証明と欠陥のある証明を区別する能力を大幅に向上させると主張している。主な意義は、詳細な精緻化そのものが、標準的な推論が見落としがちな微細な論理的エラーを発見するためのメカニズムとして機能することを示した点にある。

著者らは、本研究は形式的証明助手や数学的語彙（Mathematical Vernacular; MV）を再発明することを目的としていないことを強調している。むしろ、自然言語で動作する自動証明レビューシステムのための理論的基礎を確立するものである。本研究の知見は、モデルに基礎的な詳細を明示的に書き出させることで、エージェントがデッドエンドを効果的に刈り取り、最先端の数学的概念における幻覚を減少させられることを示唆している。結論として、ベースモデルは未記載の慣習に対して脆弱なままであるものの、提案されたフレームワークは、将来の自然言語数学エージェントの内部推論プロセスに厳密なステップレベルの検証を統合するための、汎用化可能なパラダイムを提供すると述べている。