技術要約：理性の幾何学：妥当な数学的推論のスペクトル署名

1. 問題提起

大規模言語モデル（LLM）が、真の論理的推論を行っているのか、それとも単に高度なパターンマッチングを行っているのかを検証することは、依然として重要な課題である。現在の検証手法には以下の2つのカテゴリがあり、いずれも重大な限界を抱えている：

• 出力ベースの検証： プローフ・アシスタント（Lean、Coqなど）を用いて、証明がコンパイル可能かどうかを確認する。これは、論理的な妥当性と構文的な許容性を混同している。つまり、技術的な問題（タイムアウト、インポートの欠落）により妥当な証明が拒絶される一方で、型チェックの隙を突いた不備のある証明が通過してしまう可能性がある。
• 学習ベースの検証： モデルの内部状態や出力特徴量に対して分類器を学習させる。これらの手法は、大量のラベル付きデータを必要とし、偽相関を学習するリスクがあり、異なるモデルアーキテクチャ間での汎用性に欠けることが多い。

本論文は、妥当な数学的推論は、コンパイラの受理や特定のモデル学習の副産物とは明確に区別される、トランスフォーマーの注意機構（アテンション・メカニズム）内に、測定可能な学習フリーの「スペクトル署名」を誘発すると主張している。

2. 手法

提案されたフレームワークは、トランスフォーマーの自己注意機構を、トークン上の動的な重み付きグラフとして扱う。スペクトルグラフ理論を適用することで、パラメータの学習を行うことなく、情報の流れに関する幾何学的特性を抽出する。

2.1. 動的グラフとしての注意（Attention）

$L$ 個のレイヤーと $H$ 個のヘッドを持ち、$N$ 個のトークンを処理するトランスフォーマーについて：

1. グラフ構築： 各レイヤー $\ell$ およびヘッド $h$ において、ポストソフトマックスの注意行列 $A^{(\ell,h)}$ を有向重み付きグラフとして解釈する。スペクトル解析を可能にするため、これを対称化する：$W^{(\ell,h)} = \frac{1}{2}(A^{(\ell,h)} + (A^{(\ell,h)})^\top)$。
2. 集約： 注意行列を、アテンション・マス・ウェイトを用いて、レイヤーごとの単一のグラフへと集約する：$\bar{W}^{(\ell)} = \sum_{h=1}^H \alpha_h^{(\ell)} W^{(\ell,h)}$。
3. ラプラシアン： 組合せ論的グラフ・ラプラシアンを計算する：$L^{(\ell)} = \bar{D}^{(\ell)} - \bar{W}^{(\ell)}$。ここで $\bar{D}$ は次数行列である。

2.2. スペクトル診断

隠れ状態行列 $X^{(\ell)}$ をグラフ信号として扱う。グラフフーリエ変換（GFT）を用いて、これらの状態をラプラシアンの固有基底に投影する。各レイヤーから4つの診断指標を抽出する：

• 高周波エネルギー比（HFER）： 高周波スペクトル成分における信号エネルギーの割合を測定する。HFERが低いことは、エネルギーが滑らかな低周波モードに集中していることを示す。
• フィードラー値（$\lambda_2$）： ラプラシアンの第2最小固有値であり、代数的連結性を測定する。高い値は、効率的な情報流を持つ、よく結合されたグラフであることを示す。
• スペクトルエントロピー： スペクトルモード全体におけるエネルギーの分布を定量化する。
• 滑らかさ（Smoothness）： ディリクレ・エネルギーの正規化された尺度であり、値が1に近い場合は滑らかな信号を、0に近い（または負の）場合は粗い信号を示す。

2.3. 分類

選択された指標（例：レイヤー30におけるHFER）に対して、単一閾値分類器を適用する。閾値は、少量のホールドアウト・セットで較正される。この手法は学習パラメータを必要とせず、注意の構造に直接作用する。

3. 主な貢献

1. 学習フリーのフレームワーク： 推論の妥当性検出のためのスペクトル解析フレームワークの導入。これは、入れ子状の交差検証下で82.8～85.9%の精度を達成し、較正された閾値を用いることで最大95.6%に達する。
2. クロスアーキテクチャの普遍性： 4つのアーキテクチャ・ファミリー（Meta Llama, Alibaba Qwen, Microsoft Phi, Mistral AI）に属する7つのモデルにおいて、スペクトル署名が普遍的であることを実証。効果量（Cohen's $d$）は2.09から3.30の範囲にある（$p < 10^{-47}$）。
3. プラトン的妥当性： スペクトル手法が、コンパイラの受理ではなく、論理的一貫性（「プラトン的妥当性」）を検出することを発見。本手法は、技術的な失敗（例：タイムアウト）により形式システムから拒絶された数学的に健全な証明を正しく分類できる。この区別は、手動監査（$\kappa = 0.82$）によって確認されている。
4. アーキテクチャ決定論： 推論の質を符号化する特定のスペクトル特徴が、注意メカニズムに依存することを特定。標準的なグローバル・アテンションではHFERが支配的であるが、スライディング・ウィンドウ・アテンション（Mistral-7B）では、識別的な特徴が「滑らかさ」へとシフトする。
5. ダウンストリームへの有用性： Best-of-16の証明探索におけるゼロショット・リランカーとしてHFERを適用し、Pass@1を4.4～6.6%向上させ、ラベルなしの教師ありプローブのAUCの98%に匹敵する性能を実現した。

4. 実験結果

実験は、MiniF2Fベンチマーク（形式化されたLeanの証明）を用い、488の問題に対して行われた。

• 統計的有意性： 全ての7つのモデルにおいて、極めて高い統計的有意性を示した（$p_{MW} < 10^{-47}$）。
• 効果量： 妥当な証明と不適切な証明の分離は非常に大きかった。例えば、Phi-3.5-miniは $d = 3.30$、Llama-3.2-1Bは $d = 3.02$ を達成した。
• 精度： 単一閾値分類器は、学習なしで85.9～94.9%の精度を達成した。入れ子状の交差検証による精度は82.8～85.9%であった。
• 頑健性：
  • 難易度： シグナルは全ての難易度層で持続しており、複雑な証明においても $d \ge 1.31$ を維持している。
  • 長さ： 精度は証明の長さに関わらず安定しており（87～100%）、手法が長さをプロキシとして利用していないことを示している。
  • 汎用性： 方法論は非形式的な思考の連鎖（Chain-of-Thought）の推論（MATHデータセット）にも汎用できるが、効果量は減衰する（$d = 0.78$）。
• アブレーション：
  • コントロール1： シグナルは、人間対モデルの比較だけでなく、モデル生成された妥当な証明と不適切な証明をも区別する。
  • コントロール2： 論理を破壊しつつスタイルを維持する人間による摂動を加えると、スペクトルシグナルは著しく低下する。これは、手法が論理的一貫性を追跡していることを裏付けている。
  • アーキテクチャ： Mistral-7B（スライディング・ウィンドウ・アテンション）はHFERではなく「滑らかさ」に依存しており、注意のデザインがスペクトル・チャネルを規定していることが確認された。

5. 意義と主張

本論文は、妥当な数学的推論には、結合された低周波のアテンション・グラフが必要であり、論理的な異常は測定可能なスペクトルの不連続性として現れるという「幾何学的原理」を確立したと主張している。

• 原理的な検証： 本研究は、古典的な数学的枠組み（スペクトルグラフ理論）が、ラベルなしでニューラルネットワークの推論を検証するための、アーキテクチャに依存した実用的なツールを提供できることを示している。
• プラトン的妥当性： 論理的一貫性とコンパイラの受理を区別できる能力は、検証に対する新しい視点を提供する。これは、技術的には拒絶されているが数学的には正しい「回収可能な」証明を特定できる可能性を示唆している。
• 効率性： 本手法は、注意グラフの固有値分解（計算量 $O(N^3)$ または Lanczos 法による $O(kN^2)$）のみを必要とするため、学習ベースの検証器に代わる計算効率の高い選択肢となる。これは、典型的な証明の長さに対して無視できる程度のオーバーヘッドである。

著者らは、このスペクトル署名がモデルの認識状態を反映しており、潜在的に「自信満々な誤答」（低スペクトルエネルギー）と「真の認知的努力」（高スペクトルエネルギー）を区別できると結論付けている。これは、難易度推定や過信検出への道を開くものである。