Veriphi：攻击引导的神经网络验证与数据集依赖的训练方法

# Veriphi：基于攻击引导的神经网络验证与数据集相关训练方法
来源：https://arxiv.org/html/2606.18454
Vasili Savin¹, Kartik Arya¹ ¹维也纳工业大学，奥地利维也纳 [email protected]

###### 摘要

我们提出 **Veriphi**，一个 GPU 加速的神经网络验证系统，它结合了快速对抗攻击与使用 α,β-CROWN 方法的正式边界认证。通过在 MNIST 和 CIFAR-10 上使用三种训练方法（标准、对抗、认证）的系统性实验，我们证明 **训练方法的有效性从根本上依赖于数据集**。区间边界传播（Interval Bound Propagation, IBP）在简单的 MNIST（784 维）上达到了 78% 的认证准确率，但在更复杂的 CIFAR-10 数据集上，IBP 提供的认证性能几乎可以忽略不计，而 PGD 对抗训练在小扰动下以 94% 的认证率占据主导地位。我们通过攻击引导的证伪实现了 5 倍的验证加速，并将我们的方法扩展到生产规模的模型（1.058 亿参数），用于实际世界的航空物流优化。我们的结果挑战了“认证训练普遍优于对抗训练”的假设，表明上下文对于验证策略的选择至关重要。

## 1 引言

神经网络鲁棒性验证已成为在安全关键领域部署深度学习的关键挑战 [5 (https://arxiv.org/html/2606.18454#bib.bib5), 11 (https://arxiv.org/html/2606.18454#bib.bib11)]。虽然对抗训练 [6 (https://arxiv.org/html/2606.18454#bib.bib6)] 提供了经验鲁棒性，但它不提供正式保证。相反，认证训练方法 [4 (https://arxiv.org/html/2606.18454#bib.bib4), 13 (https://arxiv.org/html/2606.18454#bib.bib13)] 提供了数学证明，但通常牺牲了准确性或可扩展性。

最近关于大型语言模型确定性验证的工作 [1 (https://arxiv.org/html/2606.18454#bib.bib1)] 展示了对于约束满足的可靠概率边界值，这推动了类似方法在视觉和优化模型中的应用。然而，现有的验证工具面临一个根本性挑战：**从业者应针对其具体问题选择哪种训练方法？**

### 1.1 动机与问题陈述

当前的验证研究通常在一个单一数据集或架构上评估方法，导致从业者在方法选择上缺乏指导。我们确定了三个关键未解决问题：

1. **数据集复杂性**：认证训练（IBP）在验证方面是否总是优于对抗训练（PGD），还是其有效性取决于数据集复杂性？
2. **验证效率**：与纯形式方法相比，攻击引导的证伪是否能显著减少验证时间？
3. **生产规模可扩展性**：验证技术是否能从学术基准（19.1 万参数）扩展到生产模型（1 亿+参数）？

### 1.2 贡献

本文做出以下贡献：

- **数据集相关训练分析**：我们证明 IBP 训练在简单数据集上占主导地位（MNIST：78% vs PGD 的 65%），但在复杂数据集上失败（CIFAR-10：1% vs PGD 的 67%），确立了数据集复杂性（可能由输入维度和视觉复杂性驱动）作为方法选择的关键因素。
- **攻击引导验证框架**：我们提出一个两阶段系统，结合 FGSM/I-FGSM 攻击与 α,β-CROWN 形式验证，通过早期证伪实现了 85% 的时间缩减（5.4 倍 GPU 加速）。
- **生产规模验证**：我们将验证从 19.1 万参数模型扩展到 1.058 亿参数（550 倍增长），应用于真实世界的空客 Beluga 航空物流问题，展示了超出学术基准的实际适用性。
- **边界方法比较**：通过对 CROWN、α-CROWN 和 β-CROWN 的系统评估，我们显示更紧的边界相比标准 CROWN 提供不到 5% 的改进，表明边界复杂性的收益递减。

## 2 相关工作

### 2.1 形式验证方法

基于混合整数线性规划（MILP）[9 (https://arxiv.org/html/2606.18454#bib.bib9)] 和可满足性模理论（SMT）[5 (https://arxiv.org/html/2606.18454#bib.bib5)] 的完全验证方法提供了精确解但扩展性差。使用抽象解释 [2 (https://arxiv.org/html/2606.18454#bib.bib2), 8 (https://arxiv.org/html/2606.18454#bib.bib8)] 和线性松弛 [16 (https://arxiv.org/html/2606.18454#bib.bib16), 11 (https://arxiv.org/html/2606.18454#bib.bib11)] 的不完全方法提供了更好的可扩展性。

α,β-CROWN 框架 [12 (https://arxiv.org/html/2606.18454#bib.bib12), 15 (https://arxiv.org/html/2606.18454#bib.bib15)] 通过结合高效的边界传播与分支定界细化，在 VNN-COMP 竞赛中取得了最先进的性能。我们的工作建立在 auto-LiRPA [14 (https://arxiv.org/html/2606.18454#bib.bib14)] 上，这是这些方法的参考实现。

### 2.2 认证训练

认证训练方法在训练期间提供可证明的鲁棒性保证。Wong 等人 [13 (https://arxiv.org/html/2606.18454#bib.bib13)] 引入了凸外部边界最小化。Gowal 等人 [4 (https://arxiv.org/html/2606.18454#bib.bib4)] 提出了区间边界传播（Interval Bound Propagation, IBP）训练，在 MNIST 上取得了强结果。然而，扩展到复杂数据集仍然具有挑战性 [17 (https://arxiv.org/html/2606.18454#bib.bib17)]。

### 2.3 对抗训练

Madry 等人 [6 (https://arxiv.org/html/2606.18454#bib.bib6)] 将 PGD 对抗训练确立为标准防御。虽然缺乏形式保证，但它能很好地扩展到复杂数据集 [7 (https://arxiv.org/html/2606.18454#bib.bib7)]。我们的工作提供了首次系统性比较，显示何时认证训练优于对抗训练。

### 2.4 大型语言模型验证

最近关于 BEAVER [1 (https://arxiv.org/html/2606.18454#bib.bib1)] 的工作通过系统性生成空间探索解决了大型语言模型的确定性验证。虽然 BEAVER 侧重于带有前缀闭约束的顺序文本生成，我们的工作通过嵌入空间扰动解决了分类鲁棒性。两种方法都旨在提供可靠的数学保证，但针对根本不同的模型架构和验证目标。

## 3 方法

### 3.1 验证架构

Veriphi 实现了一个两阶段攻击引导验证策略：

#### 阶段 1：快速证伪

我们采用 FGSM [3 (https://arxiv.org/html/2606.18454#bib.bib3)] 和 I-FGSM（迭代 FGSM）攻击，并配置超时（默认：10 秒）。如果攻击成功，我们立即返回 **FALSIFIED**（已证伪）。

#### 阶段 2：形式验证

如果攻击失败，我们通过 auto-LiRPA 调用 α,β-CROWN 来计算认证边界。对于输入 \(x\) 和扰动预算 \(\epsilon\)（使用 \(L_{\infty}\) 范数）：

\[
\text{lower}_c, \text{upper}_c = \text{bound}(f_{\theta}(x+\delta), \delta \in [-\epsilon, \epsilon]^d) \quad (1)
\]
\[
\text{verified} \iff \text{lower}_{y_{\text{true}}} > \max_{c \neq y_{\text{true}}} \text{upper}_c \quad (2)
\]

其中 \(f_{\theta}\) 是网络，\(y_{\text{true}}\) 是真类，\(\text{bound}(\cdot)\) 计算区间边界。

### 3.2 训练方法

我们比较三种训练方法：

#### 基线

标准交叉熵最小化：

\[
\mathcal{L}_{std} = \mathbb{E}_{(x,y)\sim \mathcal{D}}[-\log p_{\theta}(y|x)] \quad (3)
\]

#### PGD 对抗训练

遵循 Madry 等人 [6 (https://arxiv.org/html/2606.18454#bib.bib6)]：

\[
\mathcal{L}_{PGD} = \mathbb{E}_{(x,y)} \max_{\|\delta\|_{\infty} \leq \epsilon} [-\log p_{\theta}(y|x+\delta)] \quad (4)
\]

其中内部最大化使用投影梯度下降，步长 \(\alpha = \epsilon/4\)，通常 20 步。

#### IBP 认证训练

遵循 Wong 等人 [13 (https://arxiv.org/html/2606.18454#bib.bib13)]：

\[
\mathcal{L}_{IBP} = (1-\kappa) \mathcal{L}_{std} + \kappa \cdot \mathcal{L}_{robust} \quad (5)
\]

其中 \(\mathcal{L}_{robust}\) 使用区间边界传播，且 \(\kappa\) 在训练过程中从 0 线性增加到 0.5。

### 3.3 模型架构：Tiny Recursive 模型

我们采用 Tiny Recursive 模型（TRM）[10 (https://arxiv.org/html/2606.18454#bib.bib10)]，这是一种为递归计算推理任务设计的新颖架构。TRM-MLP 变体使用：

- **状态向量**：\(y \in \mathbb{R}^{256}\)（解状态），\(z \in \mathbb{R}^{256}\)（推理状态）
- **递归更新**：对于 \(L\) 个改进步骤，每个步骤有 \(H\) 个推理循环：
  \[
  z^{(h)} \leftarrow f_z([x, y, z^{(h-1)}]) \quad \text{对于 } h = 1...H \quad (6)
  \]
  \[
  y^{(\ell)} \leftarrow f_y([y^{(\ell-1)}, z^{(H)}]) \quad \text{对于 } \ell = 1...L \quad (7)
  \]
- **输出**：\(\text{logits} = W_{\text{head}} y^{(L)} + b\)

该架构对验证友好（ReLU 激活、线性操作），同时通过递归保持表达能力。MNIST 模型有 19.1 万参数；CIFAR-10 模型类似。

我们选择 TRM-MLP 基于三个原因：(1) 验证友好的架构（ReLU、线性操作、无批归一化），(2) 最近工作在推理任务上表现出色 [10 (https://arxiv.org/html/2606.18454#bib.bib10)]，(3) 递归结构测试了超出 CNN 的非标准架构上的验证。

我们从头训练而非微调，以隔离训练方法的影响。使用 IBP/PGD 微调预训练模型可能会产生不同的认证率。

### 3.4 实验设置

#### 数据集

- **MNIST**：6 万训练，1 万测试，28×28 灰度（784 维）
- **CIFAR-10**：5 万训练，1 万测试，32×32 RGB（3072 维）
- **Airbus Beluga**：2336 个物流问题，可变维度（生产部署）

#### 训练配置

- **MNIST**：基线（60 轮），PGD（\(\epsilon = 2/255\)，60 轮），IBP（\(\epsilon = 1/255\)，60 轮）
- **CIFAR-10**：基线（100 轮），PGD（\(\epsilon = 8/255\)，100 轮），IBP（\(\epsilon = 2/255\)，100 轮）
- **优化器**：AdamW，学习率 0.001，余弦衰减
- **批大小**：128（MNIST），256（CIFAR-10）

#### 验证配置

- **样本量**：每个 epsilon 值 512 个样本（从测试集随机采样）
- **Epsilon 值**：MNIST（0.01, 0.04, 0.06, 0.08, 0.1），CIFAR-10（0.001, 0.002, 0.004, 0.006, 0.008）
- **边界方法**：CROWN，α-CROWN，β-CROWN
- **硬件**：VSC-5 双 A100 GPU（各 80GB），AMD EPYC 7713 CPU
- **超时**：每个样本 60 秒

## 4 结果

### 4.1 数据集复杂性决定方法有效性

表 1 (https://arxiv.org/html/2606.18454#S4.T1) 展示了我们的主要发现：训练方法的有效性是数据集相关的。

表 1：不同训练方法和数据集下的验证准确率（%）。每个配置 512 个样本，β-CROWN 边界。

#### MNIST（简单数据集）

IBP 训练在 \(\epsilon = 0.06-0.1\) 时达到 75-78% 的验证准确率，超过 PGD 12-15 个百分点。认证训练目标直接优化可验证边界，在 784 维输入空间上表现优异。

#### CIFAR-10（复杂数据集）

IBP 相对于基线没有提供改进（两者在 \(\epsilon \geq 0.006\) 时都达到 1%），而 PGD 在所有 epsilon 值下达到 58-94%。输入维度增加 4 倍（784 → 3072）导致 IBP 边界计算失败，产生过于保守的边界，从而无法进行认证。

#### 解释

这种显著差异表明 IBP 的边界传播在处理数据集复杂性时遇到困难——可能是由于输入维度增加（784→3072）和视觉复杂性（灰度数字 vs. 彩色物体）——区间算术累积了过多的过近似误差。PGD 对抗训练是经验性的而非基于边界，因此在不同数据复杂性下保持有效性。

### 4.2 攻击引导的验证加速

表 2 (https://arxiv.org/html/2606.18454#S4.T2) 显示了攻击引导证伪带来的验证性能提升。

表 2：验证时间比较：纯形式 vs. 攻击引导方法。MNIST，512 个样本，\(\epsilon = 0.1\)。

| 方法 | 平均时间 (s) | 加速比 | GPU 内存 (MB) |
|------|--------------|--------|----------------|
| 纯 α-CROWN | 1.21 | 1.0× | 28 |
| 攻击引导 | 0.22 | 5.5× | 24 |
| **时间分解** |
| 攻击阶段 | 0.08 | – | 18 |
| 形式阶段 | 0.14 | – | 24 |

攻击引导方法通过在调用昂贵的正式验证之前，在 <0.1s 内证伪易受攻击的样本，实现了 85% 的时间缩减。在 MNIST 上 \(\epsilon = 0.1\) 时，攻击成功证伪了 40% 的样本，完全避免了正式验证。

### 4.3 边界方法比较

我们系统地评估了三种边界传播方法（表 3 (https://arxiv.org/html/2606.18454#S4.T3)）。

表 3：MNIST PGD 模型上的边界方法比较，512 个样本，\(\epsilon = 0.08\)。

更紧的边界（α, β-CROWN）仅带来微小的改进（<5%），但时间成本增加 20-30%。对于实际验证，标准 CROWN 边界提供了最佳的准确-效率权衡。这些结果表明，在实际设置中，更紧的边界可能并不总是证明其计算成本的合理性。

### 4.4 生产规模应用：Airbus Beluga 物流

我们选择 Airbus Beluga 来展示在学术视觉基准之外的实际适用性。航空物流是一个安全关键领域，其中形式验证通过认证的约束满足提供了具体价值。

我们将 Veriphi 扩展到验证一个 1.058 亿参数的 TRM 模型，该模型训练于 Airbus Beluga 航空物流约束满足问题。该模型优化了将工装分配给航班、货架和生产计划，需满足以下约束：

- **航班容量约束**（重量、体积）
- **货架容量约束**（物理空间）
- **生产计划时间约束**
- **类型匹配约束**（工装-货架兼容性）

#### 架构扩展

Beluga TRM 使用：

- **输入维度**：23,840（问题状态：821 个工装 × 29 个特征）
- **隐藏维度**：\(y=512, z=512\)，MLP 隐藏层 = 1024
- **输出**：821 个工装 × 10 个动作 = 8,210 维 logits
- **参数**：105,847,690（比 MNIST 模型大 550 倍）

#### 验证结果

在 10 个采样问题上，\(\epsilon = 0.05\)（5% 参数扰动）：

- **验证稳健**：4/10 问题（40%）
- **证伪**：6/10 问题（找到反例）
- **平均验证时间**：每个问题 2.6 秒
- **GPU 内存**：峰值 380MB（完全在 A100 容量内）

这证明了 Veriphi 成功扩展到生产规模模型（1 亿+参数），且验证时间实用（<5 秒）。该模型在 40% 的测试问题上，在问题参数（航班延误、需求变化）±5% 扰动下保持约束满足，为实际航空物流提供了形式鲁棒性保证。

### 4.5 GPU 分析与优化

使用 NVIDIA Nsight Systems，我们对验证流水线进行了分析以识别瓶颈：

- **CUDA 内核时间**：25.75%（边界传播）
- **PyTorch 操作**：18.78%（张量操作）
- **auto-LiRPA 库**：12