走向可验证的 Transformer：求解器可检查的电路解释

机械可解释性通常会发现电路，然后通过示例和消融来论证它们的作用。我们引入了可验证的 Transformer，这是一个框架，用于将任务局部电路转变为有界的、求解器可检查的声明：预测功能等价性、任务相关不变性、边缘必要性以及对连续最终残差扰动的鲁棒性。在小规模上，我们直接验证引用结束和括号型电路的所有四个属性，包括程序介导的电路，其注意力选择完全是象征性的。在 GPT-2 规模上，我们在使用 +0.0087 OpenWebText 损失增加进行训练后从稀疏最大/LeakyReLU 模型中删除 LayerNorm，用合成的受限 DSL 程序替换保留的注意力头，并仅校准程序本地读数，同时冻结和散列所有其他参数。由此产生的三边引用电路（嵌入 $\to$ MLP 0 $\to$ 程序头 $\to$ logits）在线性实数算术中验证散列固定的 1,280 提示域上的所有四个属性：1,280/1,280 等价性和不变性，每条边 640 个边必要性见证，以及 $ε= 0.01$ 的鲁棒性（最小认证）半径 0.01515。对于同一开启检测/复制类型任务的两个字母变体，未触及的门暴露了本地化前沿：括号类型提取仅对所有 144 个头都是精确的，而构造的引用工件则使用三个边缘进行验证。基于自然发现的验证由于可衡量的原因而失败；在规模上，我们发现我们必须构建我们可以验证的对象。已验证的对象是经过校准的工件，而不是未修改的模型，并且所有声明都仅限于声明的域。