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

arXiv:2605.24033v1 公告类型：新 摘要：机械可解释性通常识别 Transformer 模型内的电路，但这些电路的解释通常通过示例、消融和手动推理来验证。这就在寻找合理的电路和证明电路的功能之间留下了差距。我们引入了可验证的 Transformers，这是一个用于将任务本地化 Transformer 电路转换为有界的、求解器可检查的声明的框架。给定一个行为、一个有限任务域和一个候选令牌投影，我们提取一个任务电路并验证诸如投影功能等价性、边缘必要性、任务相关不变性和最终残差鲁棒性等属性。直接验证将提取的电路本身编码到 SMT 求解器中。当电路包含不完全或不易编码的运算符时，代理介导的验证适合 SMT 可编码代理，在有界域上针对提取的电路对其进行验证，并针对代理验证符号解释。我们使用 Signed L1 BandNorm、sparsemax Attention 和 LeakyReLU 来实例化 GPT 风格的架构的直接验证。在小型符号序列任务中，我们训练一个可表示 SMT 的 Transformer，提取用于报价结束和括号类型跟踪的稀疏电路，并详尽地验证预计的功能等价性、内容不变性、边缘必要性和最终残差鲁棒性。在 GPT-2 规模上，相同的操作符堆栈可以在 OpenWebText 上稳定地训练，尽管简单的直接 SMT 验证仍然很棘手。我们还展示了对具有难以编码注意力的任务局部电路的代理介导的验证，显示了经过验证的符号解释和求解器生成的反例。目标不是全模型验证，而是将机械电路解释转变为可以证明或反驳的正式命题的具体路径。