証明付き認知：現実に基づく報酬による検証ギャップの解消

- 言語モデルの推論における検証ギャップを埋めるための「proof-carrying cognition」パラダイムを提案。 - 検証ギャップとは、形式領域外での推論に対するスケーラブルで不正不可能な報酬が存在しないこと。 - 理論、実証、パラダイム、ベンチマークの4つの貢献を行う。 - 理論では、best-of-N選択のjoint-Gaussianモデルにおいて、検証者と正解の相関rhoがテスト時計算と能力の交換レートであることを示す。 - 実証では、プログラム合成テストベッドで不健全な検証者がSoundness-under-Pressureを失うことを示す。 - パラダイムでは、推論ステップを型付き確率的クレームとして扱い、自己構築世界モデルで価格付けし、proper scoring rulesで決済する。 - ベンチマークとしてSoundness-under-Pressureを主要指標とする現実決済推論ベンチマークを指定。

- 先行研究では、推論トレースに対する強化学習が形式領域など安価で健全な検証者が存在する領域に集中している。 - 本研究は、検証ギャップという制約を明示し、現実に基づく決済（reality-settled reward）を提案することで、形式領域外への拡張を可能にする。 - 従来の凍結された検証者と比較して、現実に基づく決済がi.i.d.および敵対的圧力下で優れ、ハッキングギャップを約0.27から約0に駆逐する。 - また、on-policy決済はランダムラベリングより約10倍ラベル効率が高いことを示す。

- 理論：best-of-N選択のjoint-Gaussianモデルを構築し、検証者と正解の相関rhoを導入。不健全な検証者は多項式ペナルティN^(1/rho^2)を支払う。 - マージンフリーなコピュラ形式により、実際のLLM審判の健全性を中央値4%誤差で予測。 - 実証：プログラム合成テストベッドで実行可能な正解を使用。事前登録されたスケール複製を含む。 - 現実に基づく決済（reality-anchored settlement）を導入し、凍結検証者と比較。 - 実LLM審判とユニットテスト実行を正解として使用。 - 実GRPOトレーニング下で、凍結報酬モデルと10%決済ストリームで再適合したモデルを比較。 - パラダイム：推論ステップを型付き確率的クレームとして扱い、自己構築世界モデルをheld-out現実のみで訓練し、proper scoring rulesで決済。

- プログラム合成テストベッドで、不健全な検証者が最適化の進行に伴いSoundness-under-Pressureを0.94から0.32（N=4096）に低下させる一方、健全な検証者は単調に改善することを示す。 - 現実に基づく決済がi.i.d.および敵対的圧力下で凍結検証者を上回り、ハッキングギャップを約0.27から約0に駆逐することを示す。 - 健全性が決済ラベル数に対して対数線形にスケールし、on-policy決済がランダムラベリングより約10倍ラベル効率的であることを示す。 - 実LLM審判とユニットテスト実行を正解として、弱い審判がbest-of-Nで健全性を失う（p<0.001）、強い審判はより堅牢であること、選択のみで正直なサンプルから+0.53のハッキングギャップを生み出すことを示す。 - 実GRPOトレーニング下で、凍結報酬モデルが完全な過最適化曲線を描き（実行報酬が90%崩壊）、同じモデルを10%決済ストリームで再適合すると実行報酬を6倍保持することを示す。

- 検証ギャップが分野の拘束条件であると主張し、現実に基づく決済がその解決策となり得ることを議論。 - 不健全な検証者が最適化圧力下で健全性を失う一方、健全な検証者は改善することを示し、検証者の健全性の重要性を強調。 - 現実に基づく決済がハッキングギャップをほぼゼロにし、ラベル効率も高いことを示す。 - 実GRPOトレーニングでの過最適化問題に対し、決済ストリームによる再適合が有効であることを議論。 - 提案パラダイム「proof-carrying cognition」の可能性と、ベンチマーク指標「Soundness-under-Pressure」の意義を議論。 - 要旨からは、限界や未解決問題についての明示的な議論は不明。

- 要旨で参照/比較されている研究：best-of-N選択、GRPOトレーニング、LLM審判、プログラム合成テストベッド、proper scoring rules、copulaモデル。 - 関連手法：reality-settled reward、proof-carrying cognition、Soundness-under-Pressure。 - 同分野の定番：強化学習による推論（RL on reasoning traces）、検証器に基づく報酬（verifier-based reward）、形式検証（formal verification）。 - 具体的な論文名は要旨に明示されていないため、上記の手法や概念をキーワードに文献調査を行うことを推奨。