論文の概要: Towards Verifiable Transformers: Solver-Checkable Circuit Explanations

• arxiv url: http://arxiv.org/abs/2605.24033v1
• Date: Thu, 21 May 2026 05:21:40 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-26 19:50:17.546535
• Title: Towards Verifiable Transformers: Solver-Checkable Circuit Explanations
• Title（参考訳）: 変圧器の検証に向けて:ソルバーチェッカブル回路の説明
• Authors: Neel Somani,
• Abstract要約: 本稿では,タスクローカライズされたトランスフォーマー回路を有界,ソルバチェック可能なクレームに変換するためのフレームワークであるVerifiable Transformersを紹介する。 署名付きL1 BandNorm、スパースマックスアテンション、LeakyReLUを用いて、GPTスタイルのアーキテクチャで直接検証を行う。 また,タスクローカライズされた回路上でのサロゲートによる検証も行った。
• 参考スコア（独自算出の注目度）: 0.23689955632456092
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Mechanistic interpretability often identifies circuits inside Transformer models, but explanations of those circuits are usually validated through examples, ablations, and manual reasoning. This leaves a gap between finding a plausible circuit and proving what the circuit does. We introduce Verifiable Transformers, a framework for converting task-localized Transformer circuits into bounded, solver-checkable claims. Given a behavior, a finite task domain, and a candidate-token projection, we extract a task circuit and verify properties such as projected functional equivalence, edge necessity, task-relevant invariance, and final-residual robustness. Direct verification encodes the extracted circuit itself into an SMT solver. When a circuit contains operators that are not exactly or tractably encodable, surrogate-mediated verification fits an SMT-encodable surrogate, validates it against the extracted circuit over the bounded domain, and verifies symbolic explanations against the surrogate. We instantiate direct verification with a GPT-style architecture using Signed L1 BandNorm, sparsemax attention, and LeakyReLU. On small symbolic sequence tasks, we train an SMT-representable Transformer, extract sparse circuits for quote closing and bracket type tracking, and exhaustively verify projected functional equivalence, content invariance, edge necessity, and final-residual robustness. At GPT-2 scale, the same operator stack trains stably on OpenWebText, although naive direct SMT verification remains intractable. We also demonstrate surrogate-mediated verification on task-localized circuits with hard-to-encode attention, showing both verified symbolic explanations and solver-generated counterexamples. The goal is not full-model verification, but a concrete path for turning mechanistic circuit explanations into formal propositions that can be proven or refuted.
• Abstract（参考訳）: 機械的解釈可能性はしばしばトランスフォーマーモデル内の回路を識別するが、それらの回路の説明は通常、例、説明、手動推論によって検証される。 このことは、可算回路を見つけることと、回路が何をするかを証明することの間のギャップを残している。 本稿では,タスクローカライズされたトランスフォーマー回路を有界,ソルバチェック可能なクレームに変換するためのフレームワークであるVerifiable Transformersを紹介する。 振舞い、有限タスク領域、および候補tokenプロジェクションが与えられた場合、タスク回路を抽出し、投影された機能等価性、エッジの必要性、タスク関連不変性、最終的な残留ロバスト性などの特性を検証する。 直接検証は、抽出された回路自体をSMTソルバに符号化する。 回路が正確にあるいは引き込み可能でない演算子を含む場合、代理による検証はSMT符号化可能なサロゲートに適合し、有界領域上の抽出回路に対して検証し、サロゲートに対する記号的説明を検証する。 署名付きL1 BandNorm、スパースマックスアテンション、LeakyReLUを用いて、GPTスタイルのアーキテクチャで直接検証を行う。 小型の記号列タスクでは,SMT表現可能な変換器を訓練し,クローズドとブラケット型追跡のためのスパース回路を抽出し,予測された機能的等価性,コンテンツ不変性,エッジ必要性,最終的な残留ロバスト性を徹底的に検証する。 GPT-2スケールでは、同じオペレータスタックが安定してOpenWebTextでトレーニングされる。 また,タスクローカライズド・サーキットにおけるサロゲートによる検証も行なっており,シンボル的説明と解法的反例の両方が示されている。 目標は、完全なモデル検証ではなく、機械回路の説明を証明または否定できる正式な命題に変換する具体的な経路である。

関連論文リスト

• Seeing Through Circuits: Faithful Mechanistic Interpretability for Vision Transformers [54.2202951543048]
  視覚変換器の計算グラフから有用なメカニスティック回路を同定できるかどうかを検討する。 分類のためのクラス固有の回路を復元するビジュアル・サーキット・ディスカバリー(Vi-CD)の効果的な手法を提案する。 これらのモデルの内部計算に透明性を加えることで、視覚変換器から洞察に富み、行動可能なエッジベース回路を復元できることが判明した。
  論文  参考訳（メタデータ） (2026-04-15T23:25:46Z)
• Residual Connections and the Causal Shift: Uncovering a Structural Misalignment in Transformers [9.617245548268437]
  大規模言語モデル(LLM)は、自動回帰変換器で実装された次世代の予測で訓練される。 残余接続は現在のトークンとアクティベーションを結び付け、監督は次のトークンをターゲットとします。 固定層介入や学習可能なゲーティング機構として実装された残差減衰に基づく軽量残差経路緩和法を提案する。
  論文  参考訳（メタデータ） (2026-02-16T14:04:42Z)
• Explaining the Explainer: Understanding the Inner Workings of Transformer-based Symbolic Regression Models [3.7957452405531265]
  PATCHESは,シンボル回帰のためのコンパクトかつ正しい回路を識別する進化的回路探索アルゴリズムである。 PATCHESを用いて28個の回路を分離し,SRトランスの回路レベルの特性化を行う。
  論文  参考訳（メタデータ） (2026-02-03T13:27:10Z)
• Weights to Code: Extracting Interpretable Algorithms from the Discrete Transformer [65.38883376379812]
  本稿では,連続表現と離散記号論理のギャップを埋めるアーキテクチャである離散変換器を提案する。 実証的には、Discrete TransformerはRNNベースのベースラインに匹敵するパフォーマンスを達成するだけでなく、連続的な変数ドメインへの解釈可能性を大幅に拡張する。
  論文  参考訳（メタデータ） (2026-01-09T12:49:41Z)
• Measuring Uncertainty in Transformer Circuits with Effective Information Consistency [0.0]
  本研究では,トランスフォーマー回路のシャーフ/コホモロジーと因果出現の視点を開発する。 EICSは(i)局所ジャコビアンとアクティベーションから計算された正規化棚の不整合と(ii)回路レベルの因果発生のためのガウスEIプロキシを組み合わせる。 本稿では,スコアの解釈,計算オーバーヘッド(高速かつ高精度なモード),およびおもちゃの健全性チェック分析に関する実践的ガイダンスを提供する。
  論文  参考訳（メタデータ） (2025-09-08T18:54:56Z)
• Position-aware Automatic Circuit Discovery [59.64762573617173]
  我々は既存の回路探索手法のギャップを同定し、モデル成分を入力位置間で等しく関連するものとして扱う。 可変長例を含むタスクであっても,回路に位置性を組み込むための2つの改良を提案する。 提案手法により, 位置感応回路の完全自動検出が可能となり, 従来よりも回路サイズと忠実度とのトレードオフが良好になる。
  論文  参考訳（メタデータ） (2025-02-07T00:18:20Z)
• Complex Event Recognition with Symbolic Register Transducers: Extended Technical Report [51.86861492527722]
  本稿では,オートマトンに基づく複合イベント認識システムを提案する。 本システムは,記号とレジスタオートマトンを組み合わせたオートマトンモデルに基づいている。 我々は、イベントストリーム上のパターンを検出するために、SRTをCERでどのように使用できるかを示す。
  論文  参考訳（メタデータ） (2024-07-03T07:59:13Z)
• Circuit Transformer: A Transformer That Preserves Logical Equivalence [20.8279111910994]
  生成型ニューラルモデル "Circuit Transformer" を導入し,論理回路を与えられたブール関数と厳密に等価に生成する。 回路の特定の目的を最適化するためにマルコフ決定過程の定式化も提案されている。
  論文  参考訳（メタデータ） (2024-03-14T03:24:14Z)
• Learning Bounded Context-Free-Grammar via LSTM and the Transformer:Difference and Explanations [51.77000472945441]
  Long Short-Term Memory (LSTM) と Transformer は、自然言語処理タスクに使用される2つの一般的なニューラルネットワークアーキテクチャである。 実際には、トランスフォーマーモデルの方がLSTMよりも表現力が高いことがよく見られる。 本研究では,LSTMとTransformerの実践的差異について検討し,その潜在空間分解パターンに基づく説明を提案する。
  論文  参考訳（メタデータ） (2021-12-16T19:56:44Z)
• On the Power of Saturated Transformers: A View from Circuit Complexity [87.20342701232869]
  飽和変圧器はハードアテンション変圧器の限界を超越していることを示す。 硬度から飽和度へのジャンプは、変換器の有効回路深さを$O(log n)$の係数で増加させると解釈できる。
  論文  参考訳（メタデータ） (2021-06-30T17:09:47Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。