arXiv:2502.06038v1 类别: cross 摘要: 我们开发了一个算法，给定训练好的变换器模型 $\mathcal{M}$ 作为输入，以及长度为 $n_{fix}$ 的字符串 $s$ 和整数 $n_{free}$，该算法可以在时间复杂度和空间复杂度为 $\widetilde{O}(n_{fix}^2 + n_{free}^3)$ 的情况下生成一个数学证明，证明 $\mathcal{M}$ 被 $s$ “压垮”了。当字符串 $s$ 加上任何额外字符串 $t$ 后模型的输出 $\mathcal{M}(s + t)$ 对字符串 $t$ 的值完全不敏感，且当 $t$ 的长度 $\leq n_{free}$ 时，我们说 $\mathcal{M}$ 被 $s$ “压垮”。在证明过程中，我们还证明了一种特别强烈的形式的“过度挤压”，我们利用它来约束模型的行为。我们的技术使用计算机辅助证明来确立这种与操作相关的关于变换器模型的保证。我们实验证明了该算法在包含注意力头、层规范化、MLP/ReLU 层和 RoPE 位置编码的一层变换器上的有效性。我们相信，这项工作为获得训练好的变换器模型的有效保证奠定了基础。