論文の概要: Formally Verified Autoresearch for Analyzing the Expressivity of Multi-Head Attention

• arxiv url: http://arxiv.org/abs/2610.25341v1
• Date: Sun, 18 Oct 2026 15:36:13 GMT
• ステータス: 情報取得中
• システム内更新日: 2026-10-20 22:09:30.005321
• Title: Formally Verified Autoresearch for Analyzing the Expressivity of Multi-Head Attention
• Title（参考訳）: 多面的注意の表現性分析のための形式的検証自動検索
• Abstract要約: 付加的な位置埋め込みを施した一層型アテンションオンリー変圧器について検討する。 ブール関数のヘッド複雑性$Hast(f)$を、それを表現するのに必要なアテンションヘッドの最小数として定義する。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: Multi-head attention is a central component of the transformer architecture, yet how its expressivity depends on the number of heads remains poorly understood. We study a one-layer, attention-only transformer with additive positional embeddings and define the head complexity $H^\ast(f)$ of a Boolean function $f$ as the minimum number of attention heads required to represent it. We derive an exact linear-fractional normal form for head complexity, prove a general threshold-degree lower bound, and give an explicit ten-bit function for which this bound is strict. For symmetric Boolean functions, we independently show that head complexity equals the number of times the function changes value between consecutive Hamming-weight levels, even when positional embeddings are allowed. This agrees with the concurrent characterization of Hsu and Xu (arXiv:2608.04243) in a model without positional embeddings. The symmetric lower bound combines our general threshold-degree bound with the classical result of Aspnes et al. (1994). These results were discovered and formalized by a frontier model through conjecture generation, theorem proving, and machine verification, while human researchers asked the high-level questions and reviewed the generated theorems. We make the Lean formalization and research traces publicly available to support agent-assisted theorem proving and formal verification in mechanistic interpretability. This work provides a proof of concept for using the capabilities of frontier models, grounded by formal verification, to develop an understanding of transformer architectures.
• Abstract（参考訳）: マルチヘッドアテンションはトランスアーキテクチャの中心的な構成要素であるが、その表現性がヘッドの数に依存するかはよく分かっていない。 付加的な位置埋め込みを持つ一層型アテンションのみ変換器について検討し、その表現に必要なアテンションヘッドの最小数としてブール関数 $f$ のヘッド複雑性 $H^\ast(f)$ を定義する。 我々は、頭部の複雑さに対する正確な線形摩擦正規形式を導出し、一般的なしきい値の下界を証明し、この境界が厳密な明示的な10ビット関数を与える。 対称ブール関数に対して、頭部の複雑さは、位置埋め込みが許される場合でも、連続ハミング重みの間の関数の値が変動する回数と独立に等しいことを示す。 これは、位置埋め込みのないモデルでHsuとXu(arXiv:2608.04243)を同時に特徴づけることと一致する。 対称下界は、Aspnes et al (1994) の古典的な結果と一般しきい値境界を結びつける。 これらの結果は、予想生成、定理証明、機械検証を通じてフロンティアモデルによって発見され、形式化された。 我々は、エージェント支援定理の証明と機械的解釈可能性の形式的検証を支援するために、リーンの形式化と研究トレースを公開します。 この研究は、フォーマルな検証に基づくフロンティアモデルの能力を使用して、トランスフォーマーアーキテクチャの理解を開発するための概念実証を提供する。

関連論文リスト

• Partial Identification under Causal Orders by Linear Programming [46.16293902963101]
  反事実探索が関連する変数に対する部分的トポロジカル順序を誘導することを示す。 これにより、任意の反ファクトクエリとネストされた反ファクトクエリのバウンダリングが可能になる。
  論文  参考訳（メタデータ） (2026-08-25T11:42:38Z)
• A Compositional Theory of Causally Masked Transformers [50.88598486616582]
  モデルが実装した力学から直接表現性を導出する形式化を開発する。 各アテンションヘッドは、レイヤ内で独立して自身の状態を更新する。 修正されたソフトアテンションは、不可逆なチェックリストのような状態をサポートする。
  論文  参考訳（メタデータ） (2026-07-29T14:47:19Z)
• Geometric Factual Recall in Transformers [57.48371649045765]
  一般的な見解では、内部の重み行列は埋め込みのペアに対する連想記憶として捉えられ、事実の数と線形にスケールする記憶数を必要とする。 我々は、学習した埋め込みが直接構造を符号化する、別のエンフェロメトリックな形態の記憶の理論的、実証的な説明を開発する。 単層変圧器が被写体から共有属性集合へのランダムベクトルを記憶しなければならない制御環境では、対数埋め込み次元が十分であることを示す。 これらの結果をマルチホップ設定に拡張し、証明可能なチェーン・オブ・シークレットによる構築を提供する。
  論文  参考訳（メタデータ） (2026-05-12T17:22:22Z)
• Decidable By Construction: Design-Time Verification for Trustworthy AI [0.0]
  機械学習における一般的な仮定は、モデル正しさは事実の後に強制されなければならないというものである。 我々は,AIモデルが数値的に安定しているか,計算的に正しいか,あるいは物理領域と整合しているかを決定する特性が,必ずしもポストホック強制を要求するとは限らないことを観察する。
  論文  参考訳（メタデータ） (2026-03-26T13:09:36Z)
• TensorLens: End-to-End Transformer Analysis via High-Order Attention Tensors [53.891337639229285]
  高次アテンション・インタラクション接続を通して表現された入力依存線形演算子として変換器全体をキャプチャする新しい定式化である attentionLens を導入する。 本実験は,注目テンソルが,解釈可能性とモデル理解を目的としたツール開発のための強力な基盤となることを実証した。
  論文  参考訳（メタデータ） (2026-01-25T19:21:25Z)
• Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem [0.2599882743586163]
  我々はシグモイド関数の形式化を示し、その単調性、滑らか性、高階微分を証明した。 本稿では、シグモダルアクティベーション関数を持つニューラルネットワークが、任意の連続関数をコンパクトな間隔で近似できることを示すユニバーサル近似定理の構成的証明を提案する。 我々の研究はニューラルネットワークの信頼性を高め、検証され信頼性の高い機械学習というより広い目標に貢献する。
  論文  参考訳（メタデータ） (2025-12-03T10:16:02Z)
• The Effect of Attention Head Count on Transformer Approximation [26.943083432025926]
  変圧器の近似特性について検討し,特に注目点数の役割に着目した。 具体的には、十分な数の頭を持つ変圧器は効率的な近似を許容するが、多くの頭を持つ場合、パラメータの数は少なくとも$O(1/epsiloncT)$で、一定の$c$とシーケンス長$T$でスケールしなければならない。
  論文  参考訳（メタデータ） (2025-10-08T05:27:25Z)
• Transformers Are Universally Consistent [14.904264782690639]
  ソフトマックスに基づく非線形アテンションを備えたトランスフォーマーは,最小二乗の回帰処理を行う場合,一様に整合性を示す。 我々は経験的誤差の上限を導出し、この条件下では$mathcalO(t-1/2d)$の証明可能な速度で減衰し、$t$は入力トークンの数を表し、$d$は埋め込み次元を表す。
  論文  参考訳（メタデータ） (2025-05-30T12:39:26Z)
• DIFFormer: Scalable (Graph) Transformers Induced by Energy Constrained Diffusion [66.21290235237808]
  本稿では,データセットからのインスタンスのバッチを進化状態にエンコードするエネルギー制約拡散モデルを提案する。 任意のインスタンス対間の対拡散強度に対する閉形式最適推定を示唆する厳密な理論を提供する。 各種タスクにおいて優れた性能を有する汎用エンコーダバックボーンとして,本モデルの適用性を示す実験を行った。
  論文  参考訳（メタデータ） (2023-01-23T15:18:54Z)
• ER: Equivariance Regularizer for Knowledge Graph Completion [107.51609402963072]
  我々は、新しい正規化器、すなわち等分散正規化器(ER)を提案する。 ERは、頭と尾のエンティティ間の意味的等価性を利用することで、モデルの一般化能力を高めることができる。 実験結果から,最先端関係予測法よりも明確かつ実質的な改善が示された。
  論文  参考訳（メタデータ） (2022-06-24T08:18:05Z)

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

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