通过ReLU催化的抽象精化实现Transformer的精确验证

# 通过 ReLU 催化的抽象精炼实现 Transformer 的精确验证

来源: https://arxiv.org/html/2605.14294

11institutetext:九州大学，福冈，日本
11email:[email protected],11email:\{zhang, zhao\}@ait.kyushu-u.ac.jp
22institutetext:国立信息学研究所，东京，日本

###### 摘要

Transformers 的形式化验证因其在安全关键型应用中的广泛部署而变得越来越重要。与经典神经网络相比，Transformer 的推理涉及高度复杂的计算，例如自注意力层中的点积，这使得其验证极其困难。现有方法通过构建凸约束来逼近 Transformer 的输出范围，从而采用过近似方法，这些方法可以实现高效率。然而，它们可能会牺牲验证精度，从而引入显着的近似误差，导致频繁出现误报。在本文中，我们提出了一种能够实现更高精度的 Transformer 验证方法。我们方法的核心是对 ReLU 的一种创新用法，通过它我们可以表示点积的精确但非线性的边界，从而可以进一步利用大量关于 ReLU 凸松弛的现有文献来推导出精确的边界。我们将两种经典方法扩展到 Transformer 的背景下，一种是基于规则的方法，另一种是基于优化的方法，从而产生了两个用于高效和精确验证的新框架。我们在从两个情感分析数据集导出的不同模型架构和鲁棒性属性上评估了我们的方法，并与最先进的基线方法进行了比较。与基线相比，我们的方法在大多数验证任务中可以实现显着的精度提升，同时效率的妥协是可以接受的，这证明了我们方法的有效性。

## 1 引言

在过去的十年中，深度学习的快速发展推动了不同应用领域前所未有的突破。作为一个里程碑式的进展，由 *自注意力* 机制驱动的 Transformers [27 (https://arxiv.org/html/2605.14294#bib.bib3)] 为多个领域（例如计算机视觉和自然语言处理）带来了革命性的性能提升。然而，与其他类型的神经网络类似，Transformers 也因对对抗性扰动存在众所周知的脆弱性而引发对其可信度的重大质疑。例如，*同义词替换* [21 (https://arxiv.org/html/2605.14294#bib.bib29)，1 (https://arxiv.org/html/2605.14294#bib.bib28)] 已被证明是 NLP 中一种有效的攻击方法，可以通过将输入句子中的某些词替换为同义词来欺骗模型。鉴于 Transformers 在安全关键型应用（例如自动驾驶、医疗保健）中的部署日益增多，确保其在噪声和复杂环境中的鲁棒性已成为一项紧迫需求。

验证是一种首选方法，可以正式证明系统的安全性和鲁棒性，从而减轻对其错误行为的担忧。在神经网络背景下，验证已被广泛研究（参见综述 [19 (https://arxiv.org/html/2605.14294#bib.bib21)] 和竞赛报告 [6 (https://arxiv.org/html/2605.14294#bib.bib18)]），并建立了完善的方法论基础。主要挑战在于如何处理网络的 *非线性组件*，例如经典前馈神经网络中的激活函数。由于这个原因，精确计算神经网络输出的边界通常需要指数级的时间复杂度，因此无法扩展到现实世界的模型上。相比之下，*抽象解释* 是一种构建其输出的凸 *过近似* 并评估近似输出是否满足所需属性的方法——只要过近似输出满足该属性，原始输出也必然满足该属性，从而验证神经网络。由于近似输出边界的凸性，这些方法效率更高，因此在实践中更受欢迎。

**相关工作概览**

尽管经典神经网络验证的研究蓬勃发展，但 Transformer 的验证仍处于非常早期的阶段。然而，站在经典验证的肩膀上，研究界直接采用了抽象解释 [23 (https://arxiv.org/html/2605.14294#bib.bib10)，3 (https://arxiv.org/html/2605.14294#bib.bib11)，35 (https://arxiv.org/html/2605.14294#bib.bib12)]，这种方法对于大规模 Transformer 更具可扩展性。例如，作为最先进的方法，Shi 等人 [23 (https://arxiv.org/html/2605.14294#bib.bib10)] 将线性松弛的思想从经典神经网络验证扩展到 Transformer，并为 Transformer 的不同非线性组件（例如自注意力层中的点积运算）设计了不同的线性边界。与精确限定 Transformer 输出的验证方法（例如 [18 (https://arxiv.org/html/2605.14294#bib.bib17)]）相比，计算凸过近似通常需要多项式时间复杂度，因此它们更快、更具可扩展性，因此可用于处理现实世界中复杂 Transformer。

**抽象解释的完备性问题**

作为抽象解释的一个内在问题，如果过近似输出违反了给定属性，这并不意味着原始输出也违反了该属性，在这种情况下，报告的违反（即过近似输出的违反）可能是一个 *误报*。这被称为 *完备性问题* [19 (https://arxiv.org/html/2605.14294#bib.bib21)]，本质上，它源于对 Transformer 非线性组件进行近似时引入的误差。特别地，我们表明现有的过近似方法通常是 *次优的*，因此可能会引入显着的近似误差并导致许多误报。鉴于验证通常代价高昂，误报的频繁发生可能导致时间和资源的大量浪费，这凸显了对更精确近似方法的需求。

**抽象精炼的核心思想**

虽然 Transformer 中存在各种非线性运算，但点积在自注意力层的矩阵乘法中发生得最频繁，并带来了经典神经网络验证中不存在的独特挑战。在 [23 (https://arxiv.org/html/2605.14294#bib.bib10)] 中，主要贡献涉及为点积设计一个可证明正确的平面边界，该边界以刚性策略给出，总是覆盖从点积导出的双曲抛物面的一侧（参见图 2(b) (https://arxiv.org/html/2605.14294#S3.F2.sf2) 进行说明）。虽然这是一个合理的选择，但这不是唯一的选择，例如，可能存在一个对偶边界，覆盖双曲抛物面的另一侧（参见图 2(c) (https://arxiv.org/html/2605.14294#S3.F2.sf3) 进行说明）。然而，这两个平面边界，包括 [23 (https://arxiv.org/html/2605.14294#bib.bib10)] 中的边界和对偶边界，在所有的不同情况下都不是最优的。为了精炼近似，我们需要设计新方法来融合两个平面边界，同时保持边界的线性以维持验证效率。

**贡献**

在本文中，我们探索了 ReLU 函数的一种新颖用法，据此我们提出了 `BuFFeT`，代表 **B**o**u**nd **F**using-based re**F**in**e**ment for **T**ransformers，它融合了点积运算的平面边界，并在 ReLU 函数的辅助下表示它们。这样做的好处是，我们可以利用现有的经典神经网络验证文献中大量关于 ReLU 线性松弛的丰富成果，以及为收紧边界而开发的各种技术，从而利用 ReLU 基于表示的松弛线性边界。因此，我们可以为点积——自注意力层中的基本运算——推导出更紧密的边界，进而导致 Transformer 输出的边界更紧密。此外，基于我们的表示，我们还表明 [23 (https://arxiv.org/html/2605.14294#bib.bib10)] 中提出的边界及其对偶情况，是可以通过我们的表示推导出的两个特定实例，并解释了它们为何是次优的。

此外，我们利用经典神经网络验证中两种现有策略的见解来推导改进的近似。第一种策略改编自 [24 (https://arxiv.org/html/2605.14294#bib.bib23)]，简单但有效，它基于 ReLU 的输入范围选择最优的平面边界来精炼近似。第二种策略受 [32 (https://arxiv.org/html/2605.14294#bib.bib22)] 启发，更为复杂——它将近似的精炼形式化为一个优化问题，并在 ReLU 的边界空间中搜索以找到最优解。得益于此形式化，我们可以调用现代优化求解器（如 Adam）来迭代地尝试 ReLU 的不同边界并精炼验证结果。然后，一旦找到足以证明 Transformer 鲁棒性的边界，验证就可以终止。

我们在使用情感分析数据集训练的 Transformer 分类器和 TinyBERT [13 (https://arxiv.org/html/2605.14294#bib.bib25)] 上评估了我们的方法。总共，我们对 10 个具有不同复杂度的基于 Transformer 的模型进行了实验。我们用 140 个验证任务评估每个模型的鲁棒性，总计在我们的评估中产生 1400 个验证任务。我们选择最先进的方法 [23 (https://arxiv.org/html/2605.14294#bib.bib10)] 作为基线，并在验证精度和效率方面将我们的方法与它进行比较。通过我们的结果，我们观察到，对于大多数验证任务，我们的方法，特别是 `o-BuFFeT`，表现出明显的精度提升，这显着增强了验证结果的可靠性。

**影响**

值得注意的是，这项工作不仅提供了两种有效的验证方法，更重要的是，通过使用 ReLU，它在 Transformers 和经典神经网络之间架起了验证方法论的桥梁，可能允许更多已建立的 ReLU 分析方法应用于 Transformer 验证。在这方面，它为 Transformer 验证的未来研究铺平了道路。

## 2 预备知识

### 2.1 符号说明

在本文中，我们采用如下符号。给定 $X \in \mathbb{R}^{n \times m}$ 作为一个矩阵，我们用 $X_{ij} \in \mathbb{R}$（其中 $i \in \{1, \dots, n\}$, $j \in \{1, \dots, m\}$）表示 $X$ 中索引为 $(i,j)$ 的元素。我们用 $X_{i,:} \in \mathbb{R}^m$ 表示 $X$ 的第 $i$ 行，它是一个 $m$ 维向量。此外，如果 $Y \in \mathbb{R}^m$ 是一个 $m$ 维向量，我们用 $Y_i \in \mathbb{R}$ 表示 $Y$ 在其第 $i$ 维上的元素。

### 2.2 Transformer 验证问题

**Transformer 架构**

图 1：Transformer 架构

**自注意力 Transformer**

Transformers [27 (https://arxiv.org/html/2605.14294#bib.bib3)] 的特点是采用了 *自注意力* 机制，并已被应用于计算机视觉和自然语言处理等多个领域。虽然 Transformers 通常由编码器和解码器组成，但在本文中，我们遵循 [23 (https://arxiv.org/html/2605.14294#bib.bib10)] 仅考虑编码器，这种架构被 BERT [11 (https://arxiv.org/html/2605.14294#bib.bib27)] 等采用，可用于情感分析等应用中的分类任务。由于篇幅限制，我们将 Transformer 架构的更详细介绍留在 §0.A 中，这里重点介绍 Transformer 推理的形式化表示。如图 1 所示，一个 $N$ 层 Transformer 是一个函数 $f: \mathbb{R}^{n \times m} \mapsto \mathbb{R}^{c}$，它将输入 $X \in \mathbb{R}^{n \times m}$ 映射到输出 $f(X) \in \mathbb{R}^{c}$，具体如下：

\[
\begin{aligned}
f_{\text{Sub1}}(X) &:= f_{\mathrm{AN1}}(f_{\text{Attn}}(XW_Q, XW_K, XW_V), X), \tag{1}\\
f_{\text{Sub2}}(Y) &:= f_{\mathrm{AN2}}(f_{\text{FNN}}(Y), Y), \\
f(X) &:= f_{\text{Pool}}(\underbrace{f_{\text{Sub2}} \circ f_{\text{Sub1}}(\cdots(f_{\text{Sub2}} \circ f_{\text{Sub1}}(X)))}_{\text{调用 $f_{\text{Sub2}} \circ f_{\text{Sub1}}(X)$ $N$ 次}})
\end{aligned}
\]

Transformer 首先经历 $f_{\text{Sub1}}$，其中包括函数 $f_{\text{Attn}}: \mathbb{R}^{n \times m} \times \mathbb{R}^{n \times m} \times \mathbb{R}^{n \times m} \mapsto \mathbb{R}^{n \times m}$，它表示自注意力层中的计算。它接受三个矩阵 $Q$, $K$ 和 $V$ 作为输入，每个矩阵通过将输入 $X$ 与一个参数矩阵（即 $W_Q$, $W_K$, 或 $W_V$）相乘得到，并按照下式计算输出矩阵 $f_{\text{Attn}}(Q, K, V) \in \mathbb{R}^{n \times m}$：

\[
f_{\text{Attn}}(Q, K, V) := \mathrm{softmax}\left(\frac{QK^{\mathrm{T}}}{\sqrt{d_k}}\right) V \tag{2}
\]

其中 $\mathrm{softmax}$ 是一个归一化函数，$\sqrt{d_k}$ 是一个预定义的重新缩放因子。输出 $f_{\text{Attn}}(Q, K, V)$ 然后经过 $f_{\mathrm{AN1}}: \mathbb{R}^{n \times m} \times \mathbb{R}^{n \times m} \mapsto \mathbb{R}^{n \times m}$ 进行残差加法和归一化操作，得到 $f_{\text{Sub1}}(X)$ 的结果。然后，$f_{\text{Sub1}}(X)$ 作为 $f_{\text{Sub2}}$ 的输入，经历 $f_{\text{FNN}}$，它包含两个全连接层，作为一个前馈神经网络，每层由一个仿射变换和一个 $\mathrm{ReLU}$ 激活函数组成。之后，$f_{\text{FNN}}$ 的输出再经过另一个加&归一化层 $f_{\mathrm{AN2}}$ 以推导出 $f_{\text{Sub2}}$ 的输出。在整个包含 $N$ 个编码器层的 Transformer 中，$f_{\text{Sub2}} \circ f_{\text{Sub1}}(X)$ 被迭代调用 $N$ 次，然后其输出经过一个池化层 $f_{\text{Pool}}$，将结果矩阵中的信息聚合成一个向量 $f(X) \in \mathbb{R}^{c}$，作为 Transformer 的最终输出。

**鲁棒性验证问题**

鲁棒性指的是 Transformers 在对抗性扰动下行为的一致性，并已被广泛认为是其可靠性的一个基本属性。考虑一个自然语言处理任务，其中 $X$ 表示一个给定的句子，$X$ 的每一行 $X_{i,:}$ 表示一个词。我们定义一个谓词 $\Phi: \mathbb{R}^{n \times m} \mapsto \{\mathsf{true}, \mathsf{false}\}$ 来识别 ...