技術的サマリー：格子推論トランスフォーマー

問題定義

現在の大規模言語モデル（LLM）は、最終的な答えに到達するために中間的な推論トークンを生成する、思考の連鎖（chain-of-thought）パラダイムに大きく依存しています。多くのタスクにおいて有効である一方で、このアプローチは自動推論システムに見られる厳密な論理的妥当性を欠くことがよくあります。一方、従来の自動推論（SAT ソルバーなど）は、離散拡散モデルに類似した部分情報状態の反復的洗練を通じて動作しますが、これらの手法はしばしばニューラルアーキテクチャとは明確に区別されています。

著者らは、以下のギャップを指摘します：自動推論、特に抽象解釈の手法をニューラルアーキテクチャに統合して、論理的に妥当な推論を行うモデルを構築できるでしょうか？目標は、困難な論理問題において、正解を返すか、あるいは棄権するかのみを行い、誤った解を生成することなく、かつ従来の再帰的推論器や最先端の LLM に比べて大幅に少ないパラメータ数とトレーニングコストで動作するモデルを構築することです。

手法

格子推論トランスフォーマー（LDT）

核心的な貢献は、論理的に妥当な推論を近似するように設計された再帰的トランスフォーマーアーキテクチャである**格子推論トランスフォーマー（LDT）**です。

1. 抽象解釈フレームワーク：
このモデルは、推論を情報状態の格子を通じた降下として扱います。

• 具体ドメイン（$C$）： すべての有効な解の冪集合（例：すべての有効な数独グリッド）。
• 抽象ドメイン（$A$）： 各セルが viable な候補の集合を保持する「グリッド冪集合格子」。
  • 最上位（$\top$）： 情報がないことを表す（すべての候補が可能）。
  • 最下位（$\bot$）： 矛盾を表す（どの候補も不可能）。
• 推論： $\top$ からより情報豊かな状態へ移動するプロセス。ある状態が $\bot$ に収束することは、現在のブランチに有効な解が存在しないことを示します。

2. アーキテクチャ：

• 再帰的トランスフォーマー： 1 回のフォワードパスあたり 16 回の内部反復で展開される 4 層の注意層のスタックを使用します。
• 格子エンコーディング： 抽象状態はテンソルとしてエンコードされます。グリッド問題（数独など）の場合、これはマルチホットエンコーディングであり、各セルは特定の候補がまだ「生存」しているかについての信頼度を表すバイナリシグモイドを持ちます。
• 射影： フォワードパスの間、潜在状態は格子表現へと射影され、またそこから射影されます。これにより、すべてのフォワードパスが妥当な推論ステップとして機能することが強制されます。
• 矛盾検出： 専用の CLS トークンのシグモイドが矛盾（$\bot$）を予測し、モデルが充足不可能な状態を検出できるようにします。

3. トレーニング手順（オンポリシー解決ループ）：
トレーニングは推論プロセスを反映しており、モデルがテスト時に遭遇するのと同じ格子状態の分布を目にすることを保証します。

• 解決ループ： 確率的探索プロセスであり、以下の間を交互に行います：
  1. 推論： トランスフォーマーが格子状態を洗練させ（候補を排除）、
  2. 分岐： 状態が解でも矛盾でもない場合、モデルは確率的にランダムな多候補セルを単一の値に「固定」します（生存中の候補上のソフトマックスからサンプリング）。
• $\alpha$ 演算子による監督： 単一の正解（ground-truth）に対してトレーニングするのではなく、モデルは現在の状態と整合する有効な解の集合の抽象化に対して監督されます。
  • 目標 $\hat{y} = x \sqcap \alpha(\{y \in Y \mid y \text{ は } x \text{ と整合}\})$。
  • これにより、モデルは複数の有効な解から同時に学習（マルチソリューション監督）でき、複数の解が存在する際に任意の 1 つの正解にコミットすることによるペナルティを回避します。
• 損失関数： 以下の組み合わせ：
  • 候補排除のための非対称バイナリクロスエントロピー（BCE）（妥当性を確保するために誤った排除を厳しく罰する）。
  • 矛盾検出のための対称 BCE。
  • 単一候補に収束したセルのためのクロスエントロピー。

4. 推論：
推論は並列解決プロセスを実行します。複数のチェーンが同時に探索空間を探索します。あるチェーンが矛盾（格子状態または CLS トークンによって検出）に遭遇した場合、バックトラックするか、再起動します。このシステムは経験的に妥当になるように設計されています：答えを返す場合はそれが正しく、経路を見つけられない場合は棄権します。

主要な貢献

1. アーキテクチャ： 各反復で潜在状態を抽象格子に射影する再帰的トランスフォーマーであり、フォワードパスを妥当な推論ステップに変換します。
2. オンポリシートレーニング： 格子状態がモデル自身のフォワードパスの下で進化し、トレーニング状態を推論探索状態と分布内で一致させるトレーニング手順。
3. $\alpha$ 演算子： 現在の格子状態と整合する有効な解を集約する監督メカニズム。これにより、「オンポリシーでありながら、ドメイン非依存かつ状態依存の目標によって監督される」というレジームが生まれ、複数の有効な解を持つ問題を自然に処理します。
4. 計算トレードオフの特性評価： 追加のトレーニング計算が推論時の探索ステップ数を大幅に（桁違いに）短縮することを示す経験的証拠。負担をテスト時の探索からトレーニング時の学習へシフトさせます。

結果

著者らは、LDT を 3 つのベンチマークで評価し、最先端の LLM（Claude Opus 4.6、DeepSeek V4-Pro、GPT-5.4）および従来の再帰的推論器（HRM、TRM、Sotaku）と比較しました。

• Sudoku-Extreme：
  • 80 万パラメータの LDT が、Sudoku-Extreme および Snowflake Sudoku で100% の精度を達成しました。
  • 4,000 ステップのトレーニングで経験的妥当性（100% 正解または棄権）に達しました。
  • コスト： 単一の B200 GPU で約 15 分でトレーニングされ、従来の手法（例：TRM は 4 基の L40S GPU で 36 時間必要）のコストのほんの一部です。
  • 最先端 LLM： すべてのベンチマークで**0%**のスコアでした。
• Snowflake Sudoku：
  • モデルは、アーキテクチャの変更なしに、固定のカバリンググリッドとマスキングを使用して、可変トポロジーの六角形グリッド（次数 $n=4$ から $8$）に一般化しました。
  • 4 分のトレーニングで100% の精度を達成しました。
• Maze-Hard：
  • 180 万パラメータのバリアントが、複数の有効な最短経路を持つ 30x30 の迷路で99.9% の精度を達成しました。
  • マルチソリューション監督（$K=512$）は、単一ソリューション監督（$K=1$）よりも性能を向上させました。
  • 最先端 LLM は再び**0%**でした。

効率性： LDT は強力なトレードオフを示します：追加のトレーニング計算は、推論時に必要なフォワードパス数（探索ステップ）を劇的に減少させます。

意義と主張

この論文は、LDT が格子における固定点計算として推論を扱うことで、ニューラルネットワークと自動推論の間のギャップを成功裡に埋めたと主張しています。

• 妥当性： 幻覚を起こす可能性のある標準的な LLM と異なり、LDT は経験的に妥当になるように設計されています。検証済みの正解を返すか棄権するかのみを行い、偽陽性を返すことはありません。
• 効率性： この特定のオンポリシーで格子ベースのアプローチでトレーニングされた小規模モデル（200 万パラメータ未満）は、論理ベンチマークにおいて、はるかに大規模な再帰的推論器や失敗しない最先端 LLM を凌駕します。
• 一般化： このアプローチは、格子構造に関してドメイン非依存です。組み合わせパズル上でインスタンス化されていますが、アーキテクチャは理論的には推論演算子を許容する任意の抽象ドメインに適用可能です。
• 限界： 著者らは、LDT は現在、明確で固定された論理規則を持つタスクに最も適していることを指摘しています。少数ショットのデモンストレーションから規則自体を推論する必要がある ARC-AGI のようなタスクでは、事前に定義された推論演算子がないと矛盾ヘッドが信頼できなくなるため、困難に直面します。このギャップを埋めるには、より深い再帰構造や、解を生成するプログラム上の抽象ドメインが必要になるかもしれません。

要約すると、LDT は、抽象解釈を活用してニューラル探索を導くことで、構造化された論理問題に対する思考の連鎖推論に代わる、スケーラブルで妥当かつ効率的な代替手段を提供します。