可证明地用设计输入压垮Transformer模型
Provably Overwhelming Transformer Models with Designed Inputs
AI总结：
提出一种算法，可为训练好的Transformer生成其被特定输入压垮的数学证明，利用最坏情况过度压缩界，并在单层Transformer上验证，为模型保证奠定基础。
摘要：
我们开发了一种算法，该算法以训练好的Transformer模型$\mathcal{M}$、长度为$n_{fix}$的令牌字符串$s$以及整数$n_{free}$作为输入，能够生成一个数学证明，证明$\mathcal{M}$被$s$“压垮”，其时间和空间复杂度为$\widetilde{O}(n_{fix}^2 + n_{free}^3)$。当模型在该字符串加上任何附加字符串$t$上的输出$\mathcal{M}(s + t)$，在长度($t$) $\leq n_{free}$时完全不受$t$值的影响，我们称$\mathcal{M}$被$s$“压垮”。在此过程中，我们证明了“过度压缩”的一种特别强的最坏情况形式，并用它来界定模型的行为。我们的技术使用计算机辅助证明来建立关于Transformer模型的这种操作相关的保证。我们在一个带有注意力头、层归一化、MLP/ReLU层和RoPE位置编码的单层Transformer上实证测试了我们的算法。我们相信，这项工作是为训练好的Transformer模型获得有用保证这一艰巨任务迈出的垫脚石。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
