揭示神经网络证明共享的极限

# 揭示神经网络证明共享的极限  
来源：https://arxiv.org/html/2608.19351  
###### 摘要  
随着神经网络在关键领域的广泛应用，其鲁棒性验证日益重要。在某些场景下，证明共享通过跨查询复用中间层抽象状态（即*模板*），已被证明能够加速不完全验证技术。然而，在不同网络架构、验证性质、数据集和训练方法下，基于模板的加速是否具有鲁棒性仍存在疑问。本工作系统研究了基于模板加速的有效性及其局限性。研究发现，模板涵盖率在不同场景下差异巨大。我们提出了一种新颖的*联合稳定神经元*指标来解释这种差异，表明在某些情况下基于模板的技术几乎无法提供加速。随后，我们提出FastCert——一种*自动*在网络各层分配模板以最大化性能影响的技术，若模板可能无法产生加速则完全弃用。在大量基于覆盖设计的L₀验证任务中，FastCert相较于现有基于模板的复用技术平均实现了1.13×的加速。  

## 1 引言  
神经网络已成为图像分类的主导范式，支撑着从自动驾驶到医疗诊断的应用。尽管取得成功，但众所周知，精心设计的扰动（即对抗样本）可导致网络对输入产生误分类，而这些扰动对人眼几乎不可察觉\[35, 12, 5\]。为缓解此类风险，学界对创建具有可证鲁棒性的神经网络（抵御对抗威胁）兴趣浓厚\[18\]。这些方法在训练过程中暴露网络于对抗扰动，常利用形式化验证技术指导并优化训练过程\[41, 20\]。随后，训练后使用形式化验证器\[42, 17\]保证网络对特定扰动的鲁棒性，例如基于抽象解释的可靠但不完全的验证器\[30, 31, 41\]。近期研究表明，此类不完全验证器计算的中间抽象可泛化为模板\[37, 10\]，实现证明复用并加速后续验证查询。通常，通过验证局部L∞性质可导出少量模板\[35, 12, 18\]，每个模板允许在输入空间的关联区域内进行扰动。这些方法在相同输入的同质或量化网络相关性质（如图像上的移位块或随机t像素扰动）上已被证明有效。然而，在L₀验证等其他性质（一种现实威胁模型\[15\]，近期在验证实用性上取得重大进展\[26, 28\]）背景下，基于模板加速的有效性尚未被仔细研究。此外，尚无工作研究过基于模板的加速在网络架构、性质、数据集和训练方法多样性方面的极限。  

我们的第一个关键贡献是建立了一个系统框架，用于描述模板复用在何时是鲁棒性验证的有效加速器，何时验证器应直接放弃该技术。为使基于模板的验证器实现加速，高比例验证查询需被少量模板涵盖，同时每个模板需足够精确以支持查询验证。我们设计了一种新颖的*联合稳定神经元*指标来解释此权衡下模板复用的潜力。通过极限研究，我们表明若联合稳定神经元百分比低，则现有基于模板的证明共享技术几乎无法提供验证加速。我们对多个网络和训练方法的测量显示，基于模板加速的潜力在不同场景下差异巨大。  

鉴于模板效果的观测差异，存在为给定验证任务自动确定最佳模板应用方式的需求。我们的第二个关键贡献是提出一种新颖技术FastCert，用于*自动*在神经网络各层分配模板以最大化性能影响，或在模板可能无法产生加速时完全弃用。FastCert在验证前执行分析和模板生成，通过采样极少量查询预测模板涵盖率。我们实现了FastCert并证明，对于最先进的L₀验证器，在模板有效的情况下，它几乎总能提供比先前证明共享技术更大的加速；同时在模板无效时显著缓解减速。  

本文贡献如下：  
- •我们对基于模板证明复用的有效性进行了极限研究，通过联合稳定神经元的新指标表征其潜在成功率，并展示成功率差异巨大。  
- •我们提供了一种方法，可自动确定对于给定网络和验证任务集，是否、何处及如何应用模板复用。  
- •我们在工具FastCert中实现了该方法，并证明其在加速基于覆盖设计的L₀验证方面的实用性，相较于应用模板的最新技术平均实现1.13×加速（相当于减少7小时运行时间）。  

## 2 背景  
神经网络  
神经网络NN是一个函数N:ℝᵈⁱⁿ→ℝᵈᵒᵘᵗ，通常由单个层NL∘NL−1∘⋯∘N1组合构建。我们考虑全连接前馈网络，其中每层Ni(x)=ReLU(Ax+b)。修正线性单元（ReLU）激活函数逐元素应用max(⋅,0)。对于c类分类任务，网络输出dout:=c个分数，将最高分对应类别作为其预测。  

模板复用加速模型  
在验证器中使用模板的核心优势是：若查询Qj的抽象状态在第k层被模板Ti涵盖（即Qj⊑Ti），则可跳过该层剩余部分（层k至L）的计算。设验证实例总数为r，模板生成数量为m，每个模板生成时间成本为tg,模板匹配时间参数为tmatch(m)=ηm。则相对于基线验证时间rLν，加速比S为：S=(1+λm/r+ηm/(Lν)−ρk(L−k)/L)⁻¹ (2)。因此S>1当且仅当*节省的尾部成本*ρk(L−k)/L超过*分摊的模板生成与查找开销*λm/r+ηm/(Lν)。实际操作中，这倾向于(i)选择*(L−k)/L较大*的早期可行层（若查询产生足够高的ρk）；(ii)*少量模板*以保持查找和生成成本较低；(iii)*大量规格*以分摊tgen。在深层使用模板（残余小）或模板集过大（开销大）会消除收益，此时基于模板的方法可能无益。  

基于此加速模型，先前工作\[37, 10\]已证明模板复用可为块验证、固定大小L₀验证和几何扰动带来显著性能提升。此类场景中，验证实例数r通常为几百，模板集长度m至多为4。但先前工作未严格研究神经网络类型、数据集、训练方法和层选择对基于模板证明共享有效性的影响。  

## 4 基于模板证明共享的极限  
此处我们首先基于*神经元稳定性*概念，提出理解现有基于模板证明共享技术加速神经网络验证极限的模型。然后，我们对基于模板证明复用进行极限研究，表明其适用性随具体设置差异巨大。  

### 4.1 高效证明共享与神经元稳定性  
为实现通过模板进行高效证明共享，第3.3节显示需要满足：(1)高模板匹配率；(2)低模板计算成本；(3)低抽象形状模板涵盖确定成本。此外，存在基本正确性条件：(4)抽象解释器能验证模板对应的性质。此处我们探讨神经元稳定性如何与这些条件交互，具体而言，多少不稳定神经元使得四个条件极不可能同时满足。  

神经网络ReLU激活层（见第2节）逐元素作用，抑制负预激活并保留正激活。因此ReLU将神经元划分为活跃（正输出）和非活跃（零输出）集合，形成激活模式。在抽象解释中，通过网络传播抽象状态时，ReLU层是不精确性的主要来源。对于盒域，若神经元j的抽象状态由区间[lj,uj]表示，抽象解释器必须确定在区间上应用ReLU的效果。这需要基于0在[lj,uj]中的包含性进行案例分析，因为0是ReLU决策边界。因此，抽象解释的精度取决于神经元预激活值的抽象状态是否足以确定其ReLU激活结果。  

若神经元的预激活区间[lj,uj]*未跨越*ReLU的决策边界0，则该神经元被视为*稳定*\[4, 25\]。这发生在两种情况下：  
- •区间完全非负（lj≥0），意味着神经元*始终活跃*，ReLU函数始终表现为恒等映射。  
- •区间完全非正（uj≤0），意味着神经元*始终非活跃*，ReLU表现为常零函数。  

两种情况下，激活行为在抽象状态表示的所有具体行为中均固定，因此称为*稳定性*。若神经元区间[lj,uj]具有负下界和正上界（lj<0<uj），则该神经元*不稳定*。此时，抽象解释器必须在抽象域内近似ReLU的非线性行为，常引入过度近似。  

**定义1（联合稳定神经元）**：给定抽象状态集合S={Q1,Q2,...,Qm}，若对于网络层L中的每个神经元j，其区间在所有抽象状态中均满足稳定性条件（即每个Q∈S的lj≥0或uj≤0），则称该神经元为*联合稳定神经元*。  

**定理1**：若第k层所有神经元关于抽象状态集S联合稳定，则对任意Q∈S，该层的抽象解释不引入过度近似。  

证明：由稳定性定义，每个神经元j在所有Q∈S中预激活区间不跨越0。因此ReLU操作对所有具体行为是线性的（恒等或常零），抽象解释可精确计算该层输出。  

**推论1**：在使用模板的验证中，若查询集在第k层的所有模板上联合稳定，则所有匹配查询的该层抽象状态计算无损失精确度。  

推论表明，联合稳定神经元数量直接关联模板涵盖率（ρk）与验证精度（每个模板可验证性）。高联合稳定比例→高ρk且高精度；低比例则相反。  

### 4.2 模板复用极限案例研究  
我们进行极限研究以量化神经元稳定性对模板复用有效性的影响。评估三个代表性神经网络架构在CIFAR-10数据集上的表现：  
- **全连接网络（FC）**：三层全连接网络（784→128→128→10），ReLU激活。  
- **卷积网络（Conv）**：经典LeNet架构（两层卷积+两层全连接）。  
- **残差网络（Res）**：ResNet-18架构，含18层残差块。  

训练方法包括：标准训练（Std）、对抗训练（Adv，PGD方法）和随机平滑训练（Smth）。  

验证任务为基于覆盖设计的L₀验证，扰动像素数t=10。我们测量不同层k的模板涵盖率ρk及联合稳定神经元比例。  

**关键发现**：  
1. 模板涵盖率（ρk）与联合稳定神经元比例高度相关（ρ²≈0.89）。  
2. 全连接网络在所有层均展现高联合稳定比例（>70%），模板复用有效。  
3. 卷积网络在早期层（k<5）稳定比例高，但深层（k>10）骤降至<20%，模板复用失效。  
4. 残差网络因跳跃连接，在所有层保持中等稳定比例（40-60%），模板复用部分有效。  
5. 对抗训练网络比标准训练网络具有更高稳定性（因决策边界更平滑）。  

这些结果表明，模板复用有效性高度依赖网络架构、深度和训练方法。先前工作仅在全连接或浅层网络上验证有效，未能推广至深层现代架构。  

### 4.3 攻击模型下的模板适用性  
在现实威胁模型（如L₀验证）中，扰动可改变图像大量像素。我们测量不同扰动大小t下的模板涵盖率：  
- 小t（≤5）：涵盖率高（>80%），模板复用有效。  
- 中t（5-20）：涵盖率中等（40-70%），需谨慎选择层。  
- 大t（>20）：涵盖率极低（<20%），模板复用无效。  

这表明模板技术更适合局部扰动验证，而非大规模像素扰动。  

## 5 FastCert：自适应模板分配  
基于极限研究洞察，我们提出FastCert技术，为给定验证任务自动确定最佳模板分配策略。  

### 5.1 层选择与模板集精炼  
实践中，并非所有层均适合模板复用。早期层可能展现低涵盖率（见第4.2节），而极晚期层因残余深度小，节省潜力有限。且模板数量必须与查找成本平衡，更大模板集会增加生成和匹配开销。识别一组层和模板集...