迈向可验证Transformer：求解器可验证的电路解释

# 走向可验证的Transformer：可被求解器检验的电路解释
来源：https://arxiv.org/html/2605.24033
\(2026年5月18日\)

###### 摘要

机械可解释性通常识别Transformer模型内部的电路，但这些电路的解释通常通过示例、消融和人工推理来验证。这留下了从发现一个合理电路到证明该电路功能之间的差距。我们提出*可验证的Transformer*，这是一个将任务局部化的Transformer电路转化为有界、可被求解器检验的声明的框架。给定一个行为、一个有限的任务域和一个候选token投影，我们提取一个任务电路，并验证诸如投影功能等价性、边必要性、任务相关不变性和最终残差鲁棒性等属性。

该方法首先提取一个任务局部化电路。直接验证将提取的电路本身编码到SMT求解器中。当电路包含无法精确或易处理编码的算子时，代理中介验证拟合一个可SMT编码的代理，在有界域上针对提取电路对其进行验证，并针对代理验证符号化解释。我们使用Signed L1 BandNorm、sparsemax注意力和LeakyReLU实例化一个GPT风格架构的直接验证。该架构专为基于SMT的电路验证设计；大多数组件是分段仿射的，而标准QK sparsemax注意力仍然是SMT可表示的，但通过查询-键乘积和注意力加权值聚合引入了非线性算术。

在小型符号序列任务上，我们训练一个SMT可表示的Transformer，提取用于引号闭合和括号类型跟踪的稀疏电路，并穷举验证投影功能等价性、内容不变性、边必要性和最终残差鲁棒性。在GPT-2规模下，同一算子栈在OpenWebText上稳定训练，尽管朴素的直接SMT验证仍然难以处理。我们还展示了在具有难以编码注意力的任务局部化电路上的代理中介验证，展示了已验证的符号解释和求解器生成的反例。本文的保证是有界的、投影的、电路级别的。目标不是完整模型验证，而是为将机械电路解释转化为可被证明或反驳的形式化命题提供一条具体路径。

## 1 引言

大部分机械可解释性将训练后的Transformer视为训练后需要逆向工程的自然对象。这种经验方法已经产生了重要成果，包括局部化注意力头、稀疏特征以及针对算法行为的经过手工分析的电路[14 (https://arxiv.org/html/2605.24033#bib.bib14),13 (https://arxiv.org/html/2605.24033#bib.bib13),6 (https://arxiv.org/html/2605.24033#bib.bib6)]。但Transformer架构是工程产物。我们不仅可以为现有模型开发更好的事后分析工具，还可以问如何设计模型和电路分析流程，使得机械性声明更容易陈述、提取和验证。

本文以*可验证的Transformer*之名研究这个问题。目标不是端到端地验证任意大语言模型。相反，目标是使一类更狭窄但具体的机械性声明可被求解器检验。例子包括：

- • 这个提取的电路在有限域上的每个输入上是否选择了与符号参考程序相同的任务token？
- • 在指定的消融语义下，每个保留的边在行为上是否必要？
- • 该电路是否对任务无关的token变化保持不变？
- • 在指定内部接口上的有界扰动下，电路的任务决策是否稳定？
- • 一个紧凑的符号程序是否精确描述了电路的有界域行为，或者求解器能否找到一个反例？

这些声明在机械可解释性中精神上是常见的，但通常在采样输入上评估或从定性电路分析中论证。我们转而将它们表述为有界验证问题。

### 1.1 电路提取与验证

工作流程始于一个训练好的模型 \(M\)、一个任务行为、一个有限任务域 \(D\) 和一个候选token集 \(T\)。我们提取一个任务局部化电路 \(C_E\)，其中 \(E\) 是保留的边集，并评估关于投影任务决策的声明

\[
d_T(F, x) = \operatorname*{arg\,max}_{t \in T} F_t(x),
\]

其中 \(F_t(x)\) 是模型或电路 \(F\) 分配给 token \(t\) 的logit。投影决策是诸如引号闭合（问题是模型选择单引号还是双引号）和括号类型跟踪（问题是模型选择方括号还是花括号闭合分隔符）等任务的相关对象。

电路提取后，验证方法取决于提取的电路是否可以直接编码。图1 (https://arxiv.org/html/2605.24033#S1.F1) 总结了由此产生的验证路径。

完整模型 \(M\)
↓
任务域规范 \((D, T)\) 和电路提取
↓
提取的电路 \(C_E\)
直接验证                    代理中介验证
\(C_E\) →                     \(C_E\) → \(S\) → \(P\) →
SMT 证明或反例             SMT 证明或反例

图1: 电路验证路径。从任务局部化的提取电路开始，直接验证对 \(C_E\) 本身进行编码。代理中介验证拟合一个可SMT编码的代理 \(S\)，合成或指定一个符号程序 \(P\)，并在有界域上验证程序-代理等价性。在直接验证中，\(C_E\) 本身被编码到SMT求解器中，因此证明和反例直接应用于编码后的电路。在代理中介验证中，当 \(C_E\) 包含无法精确或易处理编码的操作时使用，我们拟合一个可SMT编码的代理 \(S\)，在有界域上针对 \(C_E\) 对其进行验证，然后验证关于 \(S\) 的符号假设。

### 1.2 为什么架构很重要

标准Transformer组件并非为精确符号推理而设计。Softmax注意力使用指数和归一化；LayerNorm除以数据相关的标准差[1 (https://arxiv.org/html/2605.24033#bib.bib1)]；GELU是一个光滑的非分段线性激活函数[8 (https://arxiv.org/html/2605.24033#bib.bib8)]；标准注意力包含双线性查询-键交互[16 (https://arxiv.org/html/2605.24033#bib.bib16)]。这些操作原则上并非无法推理，但它们使得即使是小的提取电路的直接形式化验证也变得困难。

因此，我们用一个GPT风格架构实例化直接验证，其中困难的组件被更SMT友好的替代方案取代：

- • Signed L1 BandNorm 取代 LayerNorm。
- • Sparsemax 取代注意力中的 softmax[11 (https://arxiv.org/html/2605.24033#bib.bib11)]。
- • LeakyReLU 取代 GELU[8 (https://arxiv.org/html/2605.24033#bib.bib8)]。

由此产生的模型是*SMT可表示的*，而非自动SMT易处理的。这一区别很重要。Sparsemax本身在得分向量上是分段线性的，但带有标准QK评分的完整sparsemax注意力仍然包含变量乘积：\(q_i^\top k_j\) 和 \(a_{ij} v_j\)。这些项将编码推入非线性实数算术或需要特殊抽象。在我们的实验中，该架构在GPT-2规模下是可训练的，但该规模下的直接验证仍然难以处理。

### 1.3 贡献

本文有六项贡献。

1. 1. 我们形式化了对有限有界域上提取的Transformer电路的投影验证。
2. 2. 我们定义了投影功能等价性、边必要性、任务相关不变性和最终残差鲁棒性的电路级属性。
3. 3. 我们引入了一种用于由可表示算子构成的电路的直接SMT验证方法，并用一个使用Signed L1 BandNorm、sparsemax注意力和LeakyReLU的GPT风格架构实例化它。
4. 4. 我们在两个符号序列任务上展示了端到端的直接验证。用于引号闭合和括号类型跟踪的小模型电路对所有目标属性进行了穷举验证。
5. 5. 我们在GPT-2规模下在OpenWebText和WikiText-103上评估了可验证算子栈。整个栈稳定训练，但朴素的直接SMT验证仍然难以处理。
6. 6. 我们引入了一种针对带有难以编码组件的提取电路的代理中介符号验证方法。该方法在可能时验证符号解释，并在解释失败时返回具体反例。

### 1.4 声明纪律

本文的保证是有界的、投影的、电路级别的。我们不主张完整模型验证、全词汇等价性、全局电路最小性、任意长度正确性或可扩展的GPT-2规模SMT验证。任务域、候选token投影、电路提取语义和代理验证过程是规范的一部分。这些限制并非偶然；正是它们使声明足够精确以接受检验。

## 2 验证提取电路的形式化框架

### 2.1 任务域和投影决策

令 \(D_{\mathrm{task}}\) 为一个有限有界任务域。例如，\(D_{\mathrm{task}}\) 可以是固定模板族的所有token序列，具有有界长度和小的有限词汇量。令 \(T\) 为一个任务特定的候选token集，例如用于引号闭合的两个引号token，或用于括号类型跟踪的两个闭合分隔符token。

对于模型或电路 \(F\)，令 \(F_T(x)\) 表示限制到 \(T\) 的logit向量。我们定义投影任务决策

\[
d_T(F, x) := \operatorname*{arg\,max}_{t \in T} F_t(x). \tag{1}
\]

令 \(P: D_{\mathrm{task}} \to T\) 为一个符号参考程序。对于类似语法的行为，这个投影决策是相关的目标。我们不要求所有词汇logit的相等性。

### 2.2 提取电路和零消融语义

令 \(M\) 为完整训练模型。一个电路 \(C_E\) 通过在一个粗粒度计算图中保留边集 \(E\) 并将删除的边贡献设为零来获得。在本文的实验中，粗粒度图包含残差流组件，如嵌入、注意力输出、MLP输出和logits。保留的电路沿保留路径使用原始训练权重和激活。

对于保留边 \(e \in E\)，令 \(C_{E \setminus \{e\}}\) 为移除边 \(e\) 后的相同电路。我们称之为*零消融语义*。这很重要，因为边必要性和忠实性声明取决于删除的计算如何表示。

电路提取并非声明中立的。如果 \(C_E\) 被提取以在域 \(D\) 上保留完整模型的投影决策，那么相关的忠实性条件是

\[
\forall x \in D, \quad d_T(C_E, x) = d_T(M, x). \tag{2}
\]

如果 \(C_E\) 被提取以优化针对 \(P\) 的任务准确性而非匹配 \(M\)，那么它应称为任务电路，而不一定是忠实的模型电路。

### 2.3 属性

表1 (https://arxiv.org/html/2605.24033#S2.T1) 总结了核心属性。

表1: 通过直接SMT验证的电路级属性。所有属性均基于有限有界任务域和任务特定的候选token投影。在最终残差鲁棒性属性中，\(r_E(x)\) 是电路 \(C_E\) 在最终归一化和解嵌入之前的最终残差，\(G_T(r)\) 是通过对残差 \(r\) 应用最终归一化和解嵌入并限制到 \(T\) 而获得的投影任务决策。

### 2.4 直接SMT验证

当 \(C_E\) 是直接SMT可表示且易处理时，验证器对电路进行编码并对目标属性取反。例如，对于功能等价性，求解器检查

\[
\exists x \in D_{\mathrm{task}}: \; d_T(C_E, x) \neq P(x). \tag{3}
\]

的可满足性。如果查询不可满足，则该属性在 \(D_{\mathrm{task}}\) 上得到证明。如果可满足，求解器返回一个具体反例。该证明是针对验证器使用的导出精确实数或有理数电路表示，而非PyTorch中的逐位IEEE浮点执行；穷举的PyTorch健全性检查用于捕获实现与编码电路之间的不匹配。对于诸如sparsemax和BandNorm等分支算子，实现使用分支证书。如果在整个相关域或扰动集上无法认证追踪到的分支，验证器返回未知而非证明。

### 2.5 代理中介验证

当提取的电路包含无法直接或易处理编码的操作时，我们引入一个可SMT编码的代理 \(S\)。然后在一个有界域上针对 \(S\) 验证符号解释程序 \(P\)。

保证由链接构成：

电路忠实性：\(\displaystyle \forall x \in D, \; d_T(C_E, x) = d_T(M, x),\) \tag{4}
代理保真度：\(\displaystyle \forall x \in D, \; d_T(S, x) = d_T(C_E, x),\) \tag{5}
程序等价性：\(\displaystyle \forall x \in D, \; P(x) = d_T(S, x).\) \tag{6}

这里 \(P(x) \in T\) 表示符号程序返回的token，而 \(d_T(S, x)\) 表示代理的投影token决策。如果后两个链接在同一个域上成立，则 \(P\) 捕获了提取电路在 \(D\) 上的投影行为。如果所有三个都成立，则 \(P\) 捕获了完整模型在 \(D\) 上的投影行为。在我们的代理中介实验中，符号证明是针对代理或有限教师关系的；原始的难以编码的注意力计算在有界域上通过行为验证而非直接编码。

## 3 SMT可表示的Transformer架构

### 3.1 设计目标

直接SMT验证受益于其提取电路可以精确编码的架构。因此，我们定义一个GPT风格的自回归解码器Transformer，它保留了GPT-2[15 (https://arxiv.org/html/2605.24033#bib.bib15)]的高级残差结构，同时将难以编码的组件替换为更可表示的替代方案。该架构专为基于SMT的电路验证设计，而非用于大规模完整模型的即时证明。

### 3.2 原始操作

首选的原始操作集包括仿射映射、比较、最大/最小、分段线性激活、阈值化、top-k或支持选择，以及线性区域上的有限析取。这些组件通常可以在带有分支结构的无量词线性实数算术中编码。然而，标准注意力通过变量乘积引入了有界度多项式项。因此，我们使用更广泛的短语*SMT可表示*。特别地，带有QK评分的sparsemax注意力在非线性实数算术中完全可表示，但这是一个主要的扩展瓶颈。

### 3.3 Signed L1 BandNorm

LayerNorm通过数据相关的标准差[1 (https://arxiv.org/html/2605.24033#bib.bib1)]进行归一化。这引入了除法和平方根，这对于精确SMT编码来说很棘手。Signed L1 BandNorm用投影风格的质量控制取代了方差归一化。

一个自然的替代方案是移除归一化，但