技術要約：Theoria – 非形式的推論状態における書き換え・受容可能性の検証

1. 問題提起

本論文は、AIによる推論における「信頼の問題」に対処している。すなわち、AIが生成した回答が、いつ正当な信頼を生むべきかを区別することである。これは、特に安全性に関わる重要な分野（科学、法律、金融、医学）において極めて重要である。現在の手法は、以下の二項対立に直面している：

• 形式証明助手（例：Lean, Coq）： 数学的な確実性を提供するが、非形式的な自然言語の要求を自動形式化する際のコストと意味的な脆弱性が高いため、ほとんどの問題分布をカバーできない。
• スカラー値LLMジャッジ： 幅広いカバレッジを提供するが、スコアが不透明で監査不可能であり、LLM特有の整合性の問題を継承し、なぜ証明が不備なのか（例：隠れた前提、捏造された引用）を特定できない。

核心となる課題は、完全な形式化を必要とせずに非形式的な推論を検証しつつ、エラー（特に未記載の仮定や論理の飛躍）を可視化し、監査可能にすることである。

2. メソドロジー：Theoria アーキテクチャ

Theoriaは、ソルバーによる自然言語の回答を証明の証跡（proof witness）、すなわち「型付けされた状態遷移のシーケンス」へと書き換える検証アーキテクチャを導入する。

2.1 書き換えの枠組み

証明を文章の塊として扱うのではなく、Theoriaはそれを状態の軌跡 $(S_0, S_1, \dots, S_n)$ へと分解する。

• 状態 ($S_i$): 確立された事実と現在のゴールを表す文字列の順序付きリスト。
• 遷移: $S_{i-1}$ から $S_i$ へのステップは、特定の**正当化タイプ（justification type）**によってライセンス（許可）される。
  1. 引用 (Citation): 定理、定義、または推論規則。
  2. 計算 (Computation): 算術または記号的操作。
  3. 問題から与えられたもの (Problem Given): 問題文に明示的に記載されている事実。
• 変化の完全性不変量 (The Completeness-of-Change Invariant): $S_{i-1}$ と $S_i$ の間のすべての意味的な差異は、記載された正当化によって説明されなければならない。もし、ある前提が新しい状態を導出するために必要であるにもかかわらず、それが前の状態に含まれていない、あるいは正当化の中に存在しない場合、それは**無許可の変異（unlicensed mutation）**とみなされる。

2.2 検証パイプライン

システムは、Solve $\to$ Formalize $\to$ Judge $\to$ Filter $\to$ Repair のループで作動する。

1. Solver (ソルバー): 自然言語の解法を提案する（ウェブ検索などのツール拡張型）。
2. Formalizer (形式化器): 解法を「状態遷移の証跡」へと書き換える。これは、前提が使用される前に明示的であることを強制する。
3. 並列特化型ジャッジ (Parallel Specialized Judging):
   • 計算ジャッジ: ステップをゼロから再計算する。
   • 引用ジャッジ: 特定の状態差分（diff）に対して、引用された定理の存在と適用可能性を検証する。
   • 問題提示ジャッジ: 事実を元のテキストと照合する。
   • 初期状態ジャッジ: $S_0$ を監査し、開始時に正当化されていない前提が導入されていないかを確認する。
   • すべてのジャッジは、妥当性を確認するのではなく、エラーを見つけ出すように敵対的にプロンプトされる。
4. ペダンティズム・フィルター (Pedantry Filter): 実質的なエラーと、非形式的な表記や圧縮に関する過度な厳格さを区別する。
5. 慣習のリフトアップ (Convention Lift): 標準的で引用可能なドメインの慣習によって拒絶が解消される場合、その仮定が明示的に記録されていることを条件に、ステップの受理を許可する。
6. 認定または拒絶 (Certify-or-Decline): システムはバイナリの決定を出力する。すべてのステップが通過した（または慣習のリフトアップによって解決された）場合、その回答は認定 (Certified) される。ステップのいずれかが失敗し、範囲内で修復できない場合、その回答は拒絶 (Declined) される。

3. 主な貢献

本論文の主要な貢献は、複数のモデルの使用やステップチェック（これらは一般的である）ではなく、特定の**証跡フォーマット（witness format）**とその理論的保証にある：

• 露出保証 (Proposition 4.4): 「変化の完全性不変量」により、隠れた前提（hidden premises）（グローバルな推論のギャップ）が、ローカルで観察可能な無許可の変異へと変換される。隠れた前提は、新しい要素として状態に現れる（ライセンスチェックを誘発する）か、あるいは不変性を破るかのいずれかである。これにより、エラーがローカルなジャッジによって検出可能な表面へと強制的に引き出される。
• エラークラス予測 (Proposition 4.5): このフォーマットは、検証の優位性が以下に集中することを予測している：
  • 隠れた前提: 無許可の変異として露出される。
  • 捏造された引用: エビデンスが明示的に型付けされ、差分に対してチェックされるため、露出される。
  • 優位性なし: 算術エラーや定理の誤用（定理は存在するが適用が誤っている場合）については、構造的な露出の優位性は得られない。なぜなら、エラーは構造的ではなく意味的なものであるからである。
• 失敗の分解: 本論文は、露出の失敗 (Exposure Failure)（フォーマットがエラーを隠してしまう）とジャッジの失敗 (Judge Failure)（ジャッジが見逃したエラー）を区別する。Theoriaは前者を最小化することを目指しており、後者は経験的に対処すべき課題としている。

4. 実証結果

評価は、HLE-Verified Gold（185個の専門家向け問題）および GPQA Diamond（65個の大学院レベルの科学問題）を用いて行われた。

4.1 HLE-Verified Gold における性能

• 認定精度 (Certified Precision): 91.4% (105問中96問正解) で、95% Wilson CI は [84.5%, 95.4%]。
• カバレッジ (Coverage): 56.8% (185問中105問を認定)。
• 非対称性: 拒絶された回答は、認定された回答よりも誤っている確率が約5.0倍高かった（エラー率：42.5% vs 8.6%）。
• ソルバー単体との比較: ウェブ拡張型ソルバーは、100%のカバレッジで83.8%の精度を達成した。Theoriaのパイプラインはエラーの大部分をフィルタリングし、認定バケット内のエラー率を8.6%まで減少させた。
• ホリスティック・ジャッジとの比較: ホリスティックLLMジャッジ（単一の信頼度スコアを割り当てるもの）は、一致したカバレッジにおいて同等の精度（92.4–93.3%）を達成した。しかし、それらは異なる問題で失敗した（Jaccard指数 0.14–0.36）。これは、エラーのカバー範囲が補完的であることを示している。

4.2 敵対的堅牢性

95個の汚染された証明（特定の型のエラーを注入したもの）を用いたベンチマークにおいて：

• 全体的な検出: Theoriaは94.7% (95問中90問) を検出し、ホリスティックな判定の83.2% (95問中79問) を上回った ($p = 0.0017$)。
• エラークラス別の詳細:
  • 隠れた前提: Theoria 90.6% vs ホリスティック 62.5% (28 pp の差)。
  • 捏造された引用: Theoria 100% vs ホリスック 90%。
  • 算術/定理の誤用: パフォーマンスは同一であった（それぞれ約95%と約93%）。これは、このエラータイプにおいては構造的な優位性を持たないという理論的予測を裏付けている。

4.3 分布外 (GPQA Diamond)

• 認定精度: 97.1% (34問中33問正解)。
• カバレッジ: 52.3%。
• 異なるベンチマークにおける高い精度は、「認定または拒絶」の境界がベンチマーク固有のキャリブレーションではなく、推論の形式化可能性によって駆動されていることを示唆している。

4.4 アンサンブルの可能性

Theoriaとホリスティック・ジャッジが失敗する問題の集合が異なるため、アンサンブル戦略（例：多数決）を用いることで、単一の手法を凌駕する58.9%のカバレッジにおいて93.6%の精度を達成した。

5. 意義と主張

本論文は、Theoriaが、生のLLM出力と形式検証の間の溝を埋めるスケーラブルな監視 (scalable oversight) メカニズムを提供すると主張している。

• 監査可能性: スカラー値のスコアとは異なり、Theoriaは、各ステップを独立して検証できる、人間が読める証明トレースを生成する。
• 構造的優位性: システムは、ジャッジにプローズ（散文）から証明を再構成させることを目的としていない。代わりに、検証タスクをローカルな問いへと還元する。「この正当化は、この特定の状態変化をライセンスしているか？」
• 補完性: 本論文は、Theoriaがホリスティック・ジャッジの代替ではなく、補完的なアプローチであることを論じている。エラーのJaccard重複が低いことは、構造的に異なる検証アーキテクチャを組み合わせることが、より高い信頼性をもたらすことを示唆している。
• 限界: 著者らは、Theoriaが（観察可能な状態の変異を伴わない）エラー（例：$S_0$ における微妙な問題文の誤解）を検出できないこと、および現在はLLMジャッジに依存しているものの、形式的なバックエンド（LeanやSMTソルバーなど）と互換性を持つよう設計されていることを認めている。

要約すると、Theoriaは、非形式的な推論に対して変化の完全性不変量を強制することにより、標準的なホリスティック評価が見逃してしまう隠れた仮定や捏造されたエビデンスを表面化させ、AI生成の推論に対する信頼の厳格かつ監査可能な境界を提供できることを実証している。