論文の概要: Masked Attention Pooling Is Invariant to Padding and Permutation: A Formal Proof in Lean

• arxiv url: http://arxiv.org/abs/2610.17132v1
• Date: Mon, 12 Oct 2026 17:20:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-18 03:08:01.491996
• Title: Masked Attention Pooling Is Invariant to Padding and Permutation: A Formal Proof in Lean
• Title（参考訳）: Masked Attention PoolingはPaddingとPermutationに不変である - リーンの形式的証明
• Abstract要約: バッチトレーニングでは、バッグは共通の長さにパディングされ、プールされた出力は、どれだけのパディングが追加されたか、インスタンスが格納された順序に依存しない。 マスクされた位置における値が無関係であること、および全マスクバッグが0にマップできることを証明した。 jax-lean証明書パイプラインを使用して、これらの定理をJAXカーネル自体からトレースされたJaxprに接続する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Attention-based multiple instance learning (MIL) pools a variable-size bag of instance embeddings into one vector. In batched training, bags are padded to a common length, and the pooled output is expected not to depend on how much padding was added or on the order in which instances are stored. This expectation holds only if padded rows are removed from both the numerator and the softmax normalizer. Common implementation idioms meet it only under side conditions. Zeroing padded features alone does not work. Masking logits with $-\infty$ fails on empty bags and on nonfinite padding. Masking with a large negative constant is exact only after floating-point underflow. We define masked attention pooling with a guarded normalizer and prove in Lean 4 with mathlib that it is invariant under any bijective reindexing of rows and under appending any finite number of masked rows with arbitrary real features and logits. We also prove that values at masked positions are irrelevant and that an all-masked bag maps to zero. The theorems hold for arbitrary finite index types and feature dimensions. Using the jax-lean certificate pipeline, we connect these theorems to the Jaxpr traced from the JAX kernel itself. Lean checks translation certificates for two concrete shapes, identifies the generated functions with the generic specification, and transfers both invariances to the imported Jaxpr's real-arithmetic semantics. All audited theorems depend only on Lean's three standard axioms. The results concern ideal real arithmetic. Floating-point execution, XLA, and the JAX tracer and importer remain outside the proof.
• Abstract（参考訳）: Attention-based multiple instance learning (MIL)は、インスタンスを1つのベクトルに埋め込んだ可変サイズのバッグをプールする。 バッチトレーニングでは、バッグは共通の長さにパディングされ、プールされた出力は、どれだけのパディングが追加されたか、インスタンスが格納された順序に依存しない。 この期待は、パッド付き行が数値演算子とソフトマックス正規化子の両方から取り除かれる場合にのみ成立する。 一般的な実装イディオムは、側面条件のみを満たす。 パッド付き機能のゼロ化だけでは機能しない。 $-\infty$のマスキングロジットは空のバッグや無限のパディングでは失敗する。 大きな負の定数を持つマスキングは、浮動小数点下流の後にのみ正確に行われる。 ガードされた正規化子によるマスク付きアテンションプーリングを定義し、Lean 4では、行の単射的な再インデックスや、任意の実特徴とロジットを持った有限数のマスク付き行の追加の下で不変であることを、Mathlibで証明しています。 また、マスクされた位置における値が無関係であること、および全マスクバッグが 0 に写像されることも証明する。 定理は任意の有限指数型と特徴次元に対して成り立つ。 jax-lean証明書パイプラインを使用して、これらの定理をJAXカーネル自体からトレースされたJaxprに接続する。 リーンは2つの具体的な形状の翻訳証明書をチェックし、生成した関数をジェネリック仕様で識別し、両方の不変性を輸入されたJaxprの現実的意味論に転送する。 監査されたすべての定理は、Leanの3つの標準公理にのみ依存する。 結果は理想実算術に関するものである。 浮動小数点実行、XLA、そしてJAXトレーサとインポートは、証明の外にあります。

関連論文リスト

• Counterfactual Probing for Parallel Unmasking with Hidden Forest Structure [50.58119214447535]
  マスク付き生成モデルは並列トークン予測を提供するが、正確な並列サンプリングはトークンを考慮しなければならない。 本研究は,発見を含む全評価がシーケンス長$N$のサブ線形であるかどうかを考察する。 本研究では, 森林構造を隠蔽した離散分布を, 固定された近似条件オラクルを通してアクセスする。
  論文  参考訳（メタデータ） (2026-09-29T15:39:50Z)
• Semantic Prefix Oracles for LLM Decoding: Contracts and Differential Validation [0.0]
  我々は、文脈自由曲面にそのような制約を付加し、アールレー降下時にそれらを実行する宣言的形式主義である意味文法仕様を提案する。 セマンティックな矛盾が継続によって修復できない接頭辞のみを拒絶する。 9つのモデルに対する一致セマンティック・リバース・シンタクティック・アブレーションを含む12モデル生成研究では、各モデル言語対について非負の観測セマンティック・ミナス・シンタクティック・ポイント推定を求める。
  論文  参考訳（メタデータ） (2026-09-28T15:34:59Z)
• Low-Rank Masking for Single-Server Matrix Multiplication [51.03944325005779]
  有限フィールド$mathbb F_q$の行列乗算を単一サーバにアウトソーシングする際の統計的プライバシーについて検討する。 独立な均一な$ntimes n$入力に対して、一様エンファンクボールマスクと独立な一様要因の積は、完全サーバビューに対して少なくとも$q-r$の最大相関機密を与えることを示す。
  論文  参考訳（メタデータ） (2026-09-16T16:12:28Z)
• From Attention Masks to Inert Zero-Vector Tokens: OAttention and O-Closure for Token Dynamics [0.0]
  アテンションマスクは、アテンションバウンダリで参加していない表現型トークン状態を提供しない。 OAttentionは、このルールの支持結合された注意深い実現である。 受信機出力を(p_i)でゲートし、(p_j)を(p_j)で重み付けする。 これによりゼロベクトルトークンはゼロ要素となり、正確なnull-受信子、nullソース挿入、自己アテンション挿入、空サポートプロパティが生成される。
  論文  参考訳（メタデータ） (2026-08-21T14:43:45Z)
• Contextual Slate GLM Bandits with Limited Adaptivity [1.8843687952462742]
  適応性に制限のある一般化線形報酬を用いた文脈スレートバンドイット問題について検討する。 Batched と (b) Rarely-Switching という2つの限定適応性設定の下でアルゴリズムを提案する。 我々のアルゴリズムは計算効率が良く、スレートが2(N)$であるにもかかわらず、1ラウンドあたりのtextpoly(N)$時間しか必要としない。
  論文  参考訳（メタデータ） (2026-06-30T10:24:37Z)
• Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware [0.0]
  量子後暗号(PQC)アクセラレーターは、$mathbbZ_q$を超えるパイプライン化された数理論変換ステージに依存している。 我々の以前の研究は大規模な構造依存解析を確立し、部分NTTマスキングのセキュリティマージンを定量化した。 マシンでチェックした3つの結果は、Lean 4でMathlibとともに紹介します。
  論文  参考訳（メタデータ） (2026-04-22T17:19:22Z)
• Unlocking Tokens as Data Points for Generalization Bounds on Larger Language Models [79.70436109672599]
  LLaMA2-70Bほどの大きさの大規模言語モデルの非空一般化境界を導出する。 我々の研究は、実際にデプロイされ、高品質なテキストを生成するモデルに対する最初の非空き境界を達成する。
  論文  参考訳（メタデータ） (2024-07-25T16:13:58Z)
• Provably Efficient High-Dimensional Bandit Learning with Batched Feedbacks [93.00280593719513]
  本稿では,オンラインインタラクションのT$ステップをバッチに分割したバッチフィードバックによる高次元マルチアームコンテキストバンドレットについて検討する。 具体的には、各バッチは以前のバッチに依存するポリシーに従ってデータを収集し、その報酬はバッチの最後にのみ明らかにする。 我々のアルゴリズムは,$mathcalO( log T)$ バッチで完全に逐次的に設定されたものに匹敵する後悔の限界を達成している。
  論文  参考訳（メタデータ） (2023-11-22T06:06:54Z)

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

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