ニール・ソマニ氏 (Neel Somani) は5月21日(現地時間)、Transformerモデルの回路説明を検証可能にする新フレームワーク「Verifiable Transformers」を導入した。arXiv cs.LGが同日付で報じた。これは、Transformerモデル内のメカニスティックな解釈可能性において、回路を発見することと、その回路の機能を厳密に証明することとの間に存在するギャップを埋めることを目指す。
Verifiable Transformersは、タスクに局所化されたTransformer回路を、境界が定められ、ソルバーでチェック可能な主張へと変換するフレームワークだ。特定の挙動、有限のタスクドメイン、候補トークン射影が与えられた場合、タスク回路を抽出し、射影された機能的同等性、エッジの必要性、タスク関連不変性、最終残差の堅牢性といった特性を検証する。
検証手法は二つ存在する。一つは直接検証 (Direct verification)であり、抽出された回路自体をSMTソルバーにエンコードする。もう一つは代理媒介検証 (surrogate-mediated verification)で、回路が正確または扱いやすくエンコードできない演算子を含む場合に用いられる。この方法では、SMTエンコード可能な代理モデルを適合させ、それを制限されたドメインで抽出された回路に対して検証し、代理モデルに対して記号的な説明を検証する。
GPTスタイルのアーキテクチャにSigned L1 BandNorm、sparsemax attention、LeakyReLUを用いた直接検証が実施された。小規模なシンボリックシーケンスタスクでは、SMTで表現可能なTransformerを訓練し、引用符閉じや括弧型追跡のためのスパース回路を抽出し、射影された機能的等価性、内容不変性、エッジの必要性、最終残差の堅牢性を網羅的に検証した。
GPT-2スケールでは、同じ演算子スタックがOpenWebTextで安定して訓練されたが、単純な直接SMT検証は困難であるとされた。また、エンコードが困難なアテンションを持つタスクに局所化された回路に対して、代理媒介検証も実証され、検証済みの記号説明とソルバー生成の反例が示されている。この研究は、メカニスティックな回路説明を形式的な命題に変え、それを証明または反証できる具体的な道筋を示すことを目指すものだ。
参考: arXiv cs.LG — 2026年5月26日 13:00 (JST)
原文ハイライト"a framework for converting task-localized Transformer circuits into bounded, solver-checkable claims."