设计输入可证明变压器模型在特定条件下完全失效
Provably Overwhelming Transformer Models with Designed Inputs
- 通过构造输入序列，证明模型输出对后续输入完全不敏感
- 算法时间复杂度为 $ ilde{O}(n_{fix}^2 + n_{free}^3)$，可验证模型失效条件
- 首次用计算机辅助证明实现对模型行为的可操作性保证，适合安全研究者
我们提出一个算法，给定训练好的Transformer模型 $/mathcal{M}$、固定长度 $n_{fix}$ 的词元串 $s$ 及整数 $n_{free}$，可在 $ ilde{O}(n_{fix}^2 + n_{free}^3)$ 的时间和空间内生成数学证明：$/mathcal{M}$ 被 $s$ “ overwhelm”。当任意附加串 $t$ 满足 $\text{length}(t) \leq n_{free}$ 时，模型输出 $/mathcal{M}(s + t)$ 完全不受 $t$ 影响。该现象源于一种强形式的“过挤压”（over-squashing）特性，我们据此建立了模型行为的上界。实验在单层含注意力头、层归一化、MLP/ReLU和RoPE位置编码的Transformer上验证了该算法。本工作为获取训练后模型的可信保证迈出了关键一步。
原文摘要 · Abstract (English)
We develop an algorithm which, given a trained transformer model $\mathcal{M}$ as input, as well as a string of tokens $s$ of length $n_{fix}$ and an integer $n_{free}$, can generate a mathematical proof that $\mathcal{M}$ is ``overwhelmed'' by $s$, in time and space $\widetilde{O}(n_{fix}^2 + n_{free}^3)$. We say that $\mathcal{M}$ is ``overwhelmed'' by $s$ when the output of the model evaluated on this string plus any additional string $t$, $\mathcal{M}(s + t)$, is completely insensitive to the value of the string $t$ whenever length($t$) $\leq n_{free}$. Along the way, we prove a particularly strong worst-case form of ``over-squashing'', which we use to bound the model's behavior. Our technique uses computer-aided proofs to establish this type of operationally relevant guarantee about transformer models. We empirically test our algorithm on a single layer transformer complete with an attention head, layer-norm, MLP/ReLU layers, and RoPE positional encoding. We believe that this work is a stepping stone towards the difficult task of obtaining useful guarantees for trained transformer models.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。