迈向可验证的变换器：求解器可检查的电路解释

背景与问题

机械可解释性的核心目标之一是识别模型内部执行特定任务的电路（即一组相关的组件与连接）。当前验证这些电路解释的标准方法高度依赖于：

• 示例测试：通过观察电路在特定输入上的激活来佐证其功能。
• 消融研究：移除或扰动电路组件，观察行为变化。
• 人工推理：基于对电路结构的分析进行逻辑推断。
  这些方法虽然有价值，但存在根本局限：它们无法提供严格的数学证明。这导致研究者只能声称一个解释是“合理的”或“可能的”，而无法断言它是“正确的”。解释与验证之间存在鸿沟，阻碍了将可解释性发现转化为可靠的知识。

核心内容

本文提出的Verifiable Transformers框架旨在跨越这一鸿沟。其核心思想是：给定一个已定位的行为、一个有限的任务域和一个候选的标记投影，将提取出的电路本身编码为一个形式化对象，从而能够用SMT求解器进行自动验证。

该框架提供两条路径：

1. 直接验证：当电路的操作（如特定的注意力机制、激活函数）可以精确且高效地转换为SMT公式时，直接将整个提取出的电路编码进求解器。研究者可以定义并验证电路需要满足的具体属性，例如：

   • 投影功能等价性：电路的计算结果是否等价于某个目标函数？
   • 边必要性：移除电路中的某条边是否会导致功能失败？
   • 任务相关不变性：改变输入中与任务无关的部分，电路行为是否保持不变？
   • 最终残差稳健性：电路对模型最终输出的影响是否稳定？

2. 代理验证：对于包含难以直接编码（如标准softmax注意力）的复杂操作的电路，此路径绕开了直接编码的障碍。它训练一个SMT可编码的代理模型来模拟原始电路的行为，并在有限的任务域上严格验证代理模型与原始电路的一致性。随后，即可对代理模型进行形式化验证。如果发现不一致，求解器还能自动生成反例。

为了验证该框架的可行性，作者在可控的实验环境中进行了实例化：

• 他们设计了一个GPT风格的架构，但替换为SMT友好的组件（Signed L1 BandNorm、稀疏注意力、LeakyReLU）。
• 在小规模符号任务（如引号闭合、括号类型跟踪）上，他们成功训练了模型，提取了稀疏电路，并穷举验证了电路的功能等价性、内容不变性、边必要性和稳健性。
• 他们在GPT-2规模上证明了使用相同操作栈的模型可以在真实数据（OpenWebText）上稳定训练，尽管对大型模型进行完整的直接验证在计算上仍不可行。
• 他们展示了在包含难编码注意力的任务局部电路上使用代理验证，既得到了经过验证的符号解释，也获得了求解器生成的、能揭示电路局限性的反例。

意义与影响

本工作的意义不在于对整个大模型进行全面的形式化验证（这被明确认为是不现实的），而在于为机械可解释性领域开辟了一条具体的、可操作的路径，将定性的、基于示例的电路解释转化为可证伪的形式化命题。

• 方法论跃迁：它将电路验证从“手工艺”（人工设计测试案例、进行消融）提升到了“工程化”（基于形式化方法的自动化验证）的层面。研究者不再只能说“这个解释看起来对”，而是可以问“这个解释在数学上是否成立？”
• 解释的严格化：框架迫使研究者将模糊的、概念性的解释（例如“电路A负责任务B”）精确地定义为可以在有限域上检查的数学属性。这极大地提高了解释的精确度和可交流性。
• 发现局限性：SMT求解器生成的反例是极具价值的副产品。它们能自动、精确地揭示一个电路解释在何处、何种条件下失败，从而为迭代和改进解释提供了明确指引。
• 推动标准化：该框架为比较不同可解释性方法提取出的电路提供了一个潜在的、更严格的标准：一个解释的强度可以由其能够通过验证的形式化属性来衡量。

总而言之，本文的核心贡献是提出了一个将形式化验证思想注入机械可解释性研究的系统框架，为将“可解释的模型”推向“可验证的解释”奠定了基础。