神经网络已广泛应用于各种现实场景. 过去难以处理的高维复杂问题, 如图像分类, 神经网络在一定程度上已经可以达到人类的水平. 随着硬件性能提升和算法的进步, 神经网络模型甚至在一些问题上已经十分成熟, 但同时, 其可解释性^[1]却十分有限. 另一方面, 由于自身不可避免的过拟合以及攻击技术的发展, 使得无论来自于自然或人为影响, 神经网络都是极其不稳定的. 因此, 在一些安全攸关的应用场景下, 神经网络的部署应用存在较强的局限性. 比如对于自动驾驶系统, 路标的识别错误可能会导致灾难性的后果. 若将神经网络应用于这样的场景, 其鲁棒性必须有严格的保证.

神经网络鲁棒性保障最直接的方法是使用足够多的测试用例来进行测试, 但有限的测试用例并不能保证其绝对安全性. 如一张28×28像素的灰阶图片, 若仅允许对任意像素值最大加1, 产生的图片已多达2^28×28种, 全部测试显然不现实. 面对这样的问题, 神经网络的形式化验证受到了广泛关注, 它能够为神经网络的安全性提供数学保证.

神经网络验证要处理的典型问题是网络的可达性质, 即给定一个神经网络及输入范围, 计算输入范围经过这个网络能够到达的输出范围. 在实际问题中, 比如图像分类问题, 这一性质通常和局部鲁棒性^[2]联系在一起. 局部鲁棒性是给定一张具体的输入图片和一个最大扰动范围, 若扰动后的图片分类标签不发生改变, 我们称这个分类网络关于输入图片和扰动范围是鲁棒的; 反之, 若存在分类标签的改变, 则称这个分类网络关于输入图片和扰动范围是不鲁棒的. 这一问题的困难之处在于神经网络中非线性激活函数的叠加, 导致难以准确地求解网络对输入输出的映射关系. 已经有一些综述^[3−6]介绍了目前神经网络验证的主流方法和工具, 同时, 能够验证的网络规模也在逐年增加. 然而遗憾的是, 目前依然没有足够有效的方法能够直接应用于工业场景的问题规模. 因此, 发展更加快速和准确的神经网络验证方法备受关注, 也是本文的关注点.

本文着重研究只包含ReLU激活函数的神经网络. 目前, 对于ReLU神经网络的验证方法大致可分为2类.

● 一类方法提供可靠(sound)且完备(complete)的结果, 即我们不仅能够相信它给出的安全答案, 也能相信它给出的不安全答案. 显然, 这要求计算网络在给定输入范围下的准确可达集. 文献[7]证明了这类方法具有NP时间复杂度.

● 另一类方法提供可靠却不完备的结果, 即能够相信它给出的安全答案, 然而当这类方法无法给出答案或给出不安全答案时, 我们无法根据这一结果得到网络不安全的结论. 这类方法通常对ReLU网络的可达集做上近似处理, 即真正的可达集包含于这类方法计算得到的可达集. 因此, 当这类方法得到的可达集与不安全区域有交集时, 并不能说明真正的可达集与不安全区域有交集. 按照近似方法不同, 这类方法又可大致分为两组: (1) 基于线性抽象, 使用线性抽象将ReLU激活函数抽象为包含其凸包的线性约束区域^{[8, 9]}; (2) 基于半正定规划(SDP), 将ReLU激活函数表示为二次约束, 再将得到的验证问题松弛为SDP问题^{[10, 11]}. 上近似方法相较于计算准确可达集有较低的时间复杂度. 尤其是线性抽象方法, 它使用容易求解的线性形式近似网络的真正可达集, 能够用于验证较大规模的网络.

与线性抽象紧密相关的另一个概念是符号传播^[12]. 符号传播技术在神经网络上传播节点取值的符号约束. 如在图 1中, 节点x_2,1的取值依赖x_1,1和x_1,2, 它们的关系是x_2,1=x₁₁+x_1,2; 而x_3,1的取值依赖x_2,1, 它们的关系是x_3,1=ReLU(x_2,1). 则代入x_2,1的符号约束, 可得x_3,1=ReLU(−x_1,1+x_1,2). 符号传播可以用来显式地描述节点之间的取值关系, 是一种有效分析神经网络的方法. 线性抽象则是将上述非线性的关系式x_3,1=ReLU(−x_1,1+x_1,2)抽象为线性约束, 以降低求解难度.

针对基于线性抽象的符号传播方法, 本文提出了多路径回溯的概念. 例如在图 1中, 如果节点值x_3,1= ReLU(x_2,1)被抽象为区间[0, ax_2,1+b], 其中, a, b为确定常数, 那么x_3,1的上界可由x_3,1≤ax_2,1+b确定. 利用x_2,1的符号约束向输入层替换, 可得到此上界关于输入层的表示x_3,1≤a(−x_1,1+x_1,2)+b. 利用符号约束替换到输入层的符号传播过程实际上确定了x_3,1上界的一条传播路径, 我们称其为回溯路径(back-propagation path), 这类方法的代表是DeepPoly^[13]. 若x_3,1有另一上界x_3,1≤cx_2,1+d, 则上述替换过程可确定x_3,1上界的另一条回溯路径, 进而得到x_3,1的另一个上界表示. 在多路径回溯的概念下, 已有的方法仅使用单条回溯路径, 因此只能得到x_3,1的一个上界. 使用多条回溯路径可以得到x_3,1的多个上界, 从而可能得到比使用单条回溯路径更为精确的上界. 更精确的上下界是这类方法的关键, 它有助于得到更精确的验证结果.

本文对基于线性抽象的符号传播方法作出改进, 旨在提高这类方法的精度. 我们的主要贡献有以下3点.

● 我们提出了多路径回溯的概念, 并指出现有的基于线性抽象的符号传播方法仅使用单条回溯路径计算神经网络节点上下界, 是多路径回溯的一种特例.

● 我们实现了多路径回溯方法, 并在数据集ACAS Xu, MNIST及CIFAR10上与使用单条回溯路径的DeepPoly对比. 结果表明, 使用多条回溯路径能明显提升验证精度, 而仅引入较低的额外时间代价.

● 我们在MNIST数据集上将多路径回溯方法与使用全局优化方法的Optimized LiRPA对比, 结果表明, 多路径回溯方法依然具有精度优势.

本文第1节具体介绍一些相关概念和已有方法. 第2节提出多路径回溯的概念并证明其可靠性. 第3节通过实验评估我们的方法. 第4节讨论更多相关工作. 第5节给出结论.

1 背景知识

本文关注激活函数为ReLU的前馈神经网络的验证问题. 前馈神经网络是节点分层表示的有向无环图, 第1层称为输入层, 最后一层称为输出层. 我们用x_i,j表示第i层的第j个节点. 为避免引入过多符号, 在不产生歧义的上下文中, 也用x_i,j表示对应节点的值. 除了i=1即输入层外, 每个节点x_i,j被它的所有上层节点用单向边连接, 这些单向边的权重构成节点x_i,j的权重向量w_i,j. 除权重向量之外, 每个x_i,j有一个常量偏移b_i,j. 我们用x₁表示第i层节点取值组成的向量. 为了描述方便, 本文将ReLU层作为一种层类型加到每个仿射变换层之后, 形成仿射变换层和ReLU层交替的神经网络结构, 如图 2所示. 我们约定: 除输入层和输出层外, 奇数层为ReLU层, 偶数层为仿射变换层. 在这种表示下, 一个ReLU层节点x_i+1,j与连接它的仿射变换层节点x_i,j的关系是x_i+1,j=ReLU(x_i,j)$ \buildrel \Delta \over = $max(0, x_i,j); 一个仿射变换层节点x_i,j与上层节点的关系是x_i,j=w_i,jx_i-1+b_i,j. 例如在图 2中, x_3,1=ReLU(x_2,1), 其中, x_2,1由仿射变换x_2,1=w_2,1x₁+b_2,1得到.

给定一个有界范围的输入, 每个节点x_i,j的取值不再是一个数值而是一个数值区间[l_i,j, u_i,j], 其中, l_i,j和u_i,j分别称为节点x_i,j的数值下界和数值上界. 仿射变换层节点x_i,j作为ReLU函数的输入, 若有l_i,j < 0 < u_i,j, 则称这个节点激活状态不确定.

一个神经网络确定了一个从输入到输出的函数f, 从经验上来看, f通常具有十分复杂的映射关系, 因此, 验证问题最关注的是f的可达集性质.

定义1(验证问题). 给定L层神经网络$f:{\mathbb{R}^{{d_1}}} \to {\mathbb{R}^{{d_L}}}$, 其中, d_i表示第i层维数; 给定输入范围$\mathcal{X}_1 $, 不安全输出范围$ \bar S $. 验证问题的目标是, 确定是否有$ f({\mathcal{X}_1}) \cap \bar S = \emptyset . $

如果可达集f($\mathcal{X}_1 $)与不安全区域$ \bar S $交集为空, 称神经网络f关于性质$({\mathcal{X}_1}, \bar S)$是安全的; 反之, 若交集非空, 则称关于性质$({\mathcal{X}_1}, \bar S)$是不安全的. 例如图像分类问题中, 输入域$\mathcal{X}_1 $是对一张原始图片经过一定大小扰动的全体图片, 不安全区域$ \bar S $可以是除正确分类标签之外的其他标签, 这样, 上述验证问题即图像分类网络的局部鲁棒性问题^[2]. 验证f($\mathcal{X}_1 $)与$ \bar S $交集为空, 等价于验证在输入范围$\mathcal{X}_1 $下, 正确标签对应的节点值恒大于其他标签对应的节点值. 因此, 求解验证问题的关键实际上是求解输出层节点的可达集. 对于使用线性抽象等可靠但不完备的方法, 关键则是如何更准确地近似输出层节点的真正可达集.

1.1 线性抽象

线性抽象方法将非线性激活函数ReLU抽象为包含其凸包的线性约束区域, 因为处理线性函数的叠加比处理非线性函数的叠加简单. 图 3表示常见的4种ReLU抽象方式, 图中的横轴表示一个仿射变换层节点x_i,j的取值, 它的数值上下界[l_i,j, u_i,j]跨过原点, 因此激活状态不确定; 纵轴表示它经过ReLU激活函数的取值x_i+1,j.蓝色阴影区域表示对ReLU函数抽象后的输入输出关系. 如在图 3(a)中, x_i,j=0时, x_i+1,j=ReLU(x_i,j)=0被抽象为蓝色区域与纵轴的交集, 即图 3(a)中黑色方括号区间.

图 3(a)通常称为LP抽象^[14], 其中, LP是线性规划(linear programming)的简称. 其抽象区域重合于ReLU激活函数在[l_i,j, u_i,j]上的二维凸包, 可以表述为以下3个线性约束:

$ \begin{gathered} {x_{i + 1, j}} \leqslant \frac{{{u_{i, j}}}}{{{u_{i, j}} - {l_{i, j}}}}({x_{i, j}} - {l_{i, j}}), \\ {x_{i + 1, j}} \leqslant {x_{i, j}}, \\ {x_{i + 1, j}} \leqslant 0. \\ \end{gathered} $

对单个ReLU激活函数的线性抽象中, 这种抽象方法是最精确的. LP抽象的一个重要问题是: 每个节点具有两个下界约束, 使得确定这个节点的数值上下界实际上成为一个最优化问题, 这也是其名称LP抽象的来源. 使用LP抽象计算每个节点的数值上下界能够得到较为精确的结果, 但随着网络深度和宽度增加, 求解接近输出层的节点数值上下界对应的LP问题会变得十分复杂.

图 3(b)−图 3(d)均为简单线性抽象, 它们分别称为直角三角形抽象、钝角三角形抽象和平行四边形抽象^[15]. 在这3种抽象方法中, 每个ReLU节点的上界和下界约束分别只有一个, 这使得可以利用符号传播逐层地传递上下界约束, 而不涉及复杂的优化方法. 它们是神经网络验证中速度很快的方法, 但另一方面, 较少的约束意味着较大的精度损失. 而且随着网络深度的增加, 精度损失的叠加会愈加明显. 如何利用这种简单的约束得到尽可能高的验证精度, 是目前备受关注的问题.

下面的定理1说明这4种抽象的可靠性, 即x_i,j经过ReLU的值属于经过上述ReLU抽象的区间.

定理1. 给定l_i,j < 0, u_i,j > 0, 对于任意λ∈[0, 1]及任意x_i,j∈[l_i,j, u_i,j], 下式成立:

$ \lambda {x_{i, j}} \leqslant ReLU({x_{i, j}}) \leqslant \frac{{{u_{i, j}}}}{{{u_{i, j}} - {l_{i, j}}}}({x_{i, j}} - {l_{i, j}}). $

证明: 注意到u_i,j/(u_i,j−l_i,j)∈(0, 1)且x_i,j−l_i,j≥0. 当x_i,j < 0时, 由ReLU函数定义, ReLU(x_i,j)=0, 而不等式左边λx_i,j≤0恒成立且不等式右边u_i,j(x_i,j−l_i,j)/(u_i,j−l_i,j)≥0, 故上式成立; 当x_i,j≥0时, ReLU(x_i,j)=x_i,j, 而不等式左边λx_i,j≤x_i,j恒成立且u_i,j(x_i,j−l_i,j)/(u_i,j−l_i,j)−ReLU(x_i,j)=l_i,j(x_i,j−u_i,j)/(u_i,j−l_i,j)≥0, 故上式成立.

取λ=0及λ=1时, 定理1蕴含LP抽象的可靠性; 取λ=u_i,j/(u_i,j−l_i,j)时, 蕴含平行四边形抽象的可靠性. 同理可得直角三角形和钝角三角形抽象的可靠性. 此外, 定理1还表明, 任意λx_i,j都可以作为ReLU(x_i,j)的下界, 从而与上界u_i,j(x_i,j−l_i,j)/(u_i,j−l_i,j)构成仅有一个线性下界约束和一个线性上界约束的ReLU可靠抽象.

1.2 符号传播和DeepPoly

文献[12]引入了符号传播方法在神经网络验证问题中的应用. 目前, 主流的验证方法都会使用符号传播方法维护每个节点与输入层节点的约束关系. 这可以通过前向传递符号约束得到, 也可以反向替换符号约束至输入层得到. 我们将反向替换符号约束至输入层的方法称为回溯(back-propagation). DeepPoly^[13]是使用回溯方法的代表, 它使用简单线性抽象处理ReLU函数. 对于每个节点x_i,j, 它维护x_i,j关于上层节点值x_i−1的符号约束, 然后通过代入x_i−1关于x_i−2的符号约束, 依次向输入层回溯, 得到x_i,j关于输入层x₁表示的上下界符号约束. 最后, 通过代入x₁的数值上下界, 计算x_i,j的数值上下界. 回溯到输入层可以得到比前向传递符号约束更精确的上下界.

图 4展示了DeepPoly计算每个节点数值上下界的过程. 网络输入范围$\mathcal{X}_1 $={(x_1,1+x_1,2): −1≤x_1,1≤1∧−1≤x_1,2≤1}且各节点偏移都为0, 节点权重在前向边上标出. 注意, 节点x_4,1由x_3,1和x_3,2经过仿射变换得到, 它们之间的关系是x_4,1≥x_3,1−x_3,2及x_4,1≤x_3,1−x_3,2, 这是x_4,1取值的符号约束. 为了得到x_4,1尽可能精确的数值上下界, 需要得到它关于输入层的符号表示, 因此利用x_3,1和x_3,2向输入层回溯. x_3,1由x_2,1经过ReLU函数得到, 假设这里使用直角三角形抽象, 则有x_3,1≥0以及x_3,1≤0.5x_2,1+1; 同理, 对于x_3,2有x_3,2≥0以及x_3,2≤0.5x_2,2+1.那么x_4,1的上界是x_4,1≤0.5x_2,1+1−0, 下界是x_4,1≥0−(0.5x_2,2+1). 按照同样的方法继续向输入层回溯, 可以得到x_4,1关于输入层表示的符号约束为x_4,1≥−0.5x_1,1+0.5x_1,2−1及x_4,1≤−0.5x_1,1+0.5x_1,2+1, 最后代入x_1,1和x_1,2的数值上下界得到x_4,1≥−2及x_4,1≤2. 因此, [−2, 2]作为x_4,1的数值上下界.

对于所有非输入层节点, DeepPoly都使用这种回溯到输入层的方式计算其数值上下界. 除了回溯到输入层, DeepPoly还使用一个有效的启发式策略来减少对每个ReLU激活函数的抽象误差: 对于激活状态不确定的节点, 例如x_2,1, 如果求得其数值上下界为[l_2,1, u_2,1], 若|l_2,1|≥u_2,1, 则选择直角三角形抽象, 因为此时直角三角形的面积为0.5×u_2,1(u_2,1−l_2,1), 小于等于钝角三角形的面积0.5×|l_2,1|(u_2,1−l_2,1); 否则, 若|l_2,1| < u_2,1, 则选择钝角三角形抽象, 因为此时钝角三角形的面积小于直角三角形. 更小的面积意味着更小的抽象误差.

DeepPoly得到每个节点的数值上下界是可靠的, 即对于每个节点, 它真正的数值上下界包含于DeepPoly计算得到的上下界. 因此, 通过这种方法可以快速得到真正可达集的一个上近似. 如果一个输入范围被DeepPoly验证是安全的, 那么蕴含它确实是安全的; 但反之不一定成立. 上近似的精度决定了这种方法的验证能力.

下一节将介绍我们的方法, 它使用多条回溯路径, 能够改善对真正可达集上近似的精度, 而仅引入较低的额外时间开销.

2 多路径回溯

从第1.2节可以看出, DeepPoly对每个节点x_i,j维护一组符号上下界约束. 一组符号约束最多构成一条回溯路径, 因此它仅能得到x_i,j的一个数值上下界. 如果对每个节点x_i,j维护多组符号上下界约束, 分别在多组符号约束构成的多条回溯路径上回溯, 则可得到x_i,j的多个数值上下界. 不同回溯路径上可以使用不同特点的线性抽象产生不同的数值上下界, 定理1保证这多个数值上下界的交集也是x_i,j的数值上下界, 因此我们可以得到更精确的上下界, 从而进一步构造更精确的上近似. 这是本文的主要想法.

给定正整数n, 定义[n]={1, 2, …, n}表示前n个正整数构成的集合. 用$ {\mathbb{R}_1}$[x]表示实系数线性多项式集合. 给定m∈[M], 我们用抽象元素$ {a_{i, j, m}} = (a_{i, j, m}^ \geqslant , a_{i, j, m}^ \leqslant ) \in \mathcal{A} = {\mathbb{R}_1}[x] \times {\mathbb{R}_1}[x] $表示节点x_i,j的符号上下界约束, 且限定$ a_{i, j, m}^ \geqslant $和$ a_{i, j, m}^ \leqslant $具有以下特定形式:

$ a_{i + 1, j, m}^ \geqslant , a_{i + 1, j, m}^ \leqslant = \sum\limits_{k = 1}^{{d_i}} {{q_{i + 1, k, m}}} {x_{i, k}} + {r_{i + 1, j, m}}, $

$ a_{1, j, m}^ \geqslant = a_{1, j, m}^ \leqslant = {x_{1, j}}. $

上式中, q_i+1,k,m和x_i+1,j,m为常数, $ a_{i + 1, j, m}^ \geqslant $和$ a_{i + 1, j, m}^ \leqslant $分别是x_i+1,j关于第i层节点表示的线性下界约束和线性上界约束. 通过x_i+1,j所依赖的所有节点的符号约束, 可以回溯到输入层得到x_i+1,j关于输入层的线性表示. 定义变换函数γ^≥, γ^≤: $ {\mathbb{R}_1}$[x]→ $ {\mathbb{R}_1}$[x]如下:

$ \begin{array}{l}{\gamma }^{\ge }\left({\displaystyle \sum _{k=1}^{{d}_{i}}{q}_{i+1, k, m}}{x}_{i, k}+{r}_{i+1, j, m}\right)={\displaystyle \sum _{k=1}^{{d}_{i}}{\gamma }^{\ge }}({q}_{i+1, k, m}{x}_{i, k})+{r}_{i+1, j, m}\\ ={\displaystyle \sum _{k=1}^{{d}_{i}}\frac{|\delta ({q}_{i+1, k, m})+1|}{2}{q}_{i+1, k, m}}{\gamma }^{\ge }({a}_{i, k, m}^{\ge })+{\displaystyle \sum _{k=1}^{{d}_{i}}\frac{|\delta ({q}_{i+1, k, m})-1|}{2}{q}_{i+1, k, m}}{\gamma }^{\le }({a}_{i, k, m}^{\le })+{r}_{i+1, j, m}, \\ {\gamma }^{\le }\left({\displaystyle \sum _{k=1}^{{d}_{i}}{q}_{i+1, k, m}}{x}_{i, k}+{r}_{i+1, j, m}\right)={\displaystyle \sum _{k=1}^{{d}_{i}}{\gamma }^{\le }}({q}_{i+1, k, m}{x}_{i, k})+{r}_{i+1, j, m}\\ ={\displaystyle \sum _{k=1}^{{d}_{i}}\frac{|\delta ({q}_{i+1, k, m})+1|}{2}{q}_{i+1, k, m}}{\gamma }^{\le }({a}_{i, k, m}^{\le })+{\displaystyle \sum _{k=1}^{{d}_{i}}\frac{|\delta ({q}_{i+1, k, m})-1|}{2}{q}_{i+1, k, m}}{\gamma }^{\ge }({a}_{i, k, m}^{\ge })+{r}_{i+1, j, m}, \\ {\gamma }^{\ge }({x}_{1, k})={\gamma }^{\le }({x}_{1, k})={x}_{1, k}, \text{ }对任意k.\end{array} $

上式中, δ为符号函数, 当q≥0时, δ(q)=+1; 当q < 0时, δ(q)=−1. γ^≥和γ^≤是一组互递归函数, 它们用于描述x_i+1,j回溯到输入层的过程, 最终得到关于输入层表示的符号下界和符号上界. 在求x_i+1,j的下界时, 如果x_i,k对应的系数q_i+1,k,m为正, 需要使用x_i,k的符号下界; 如果x_i,k对应的系数q_i+1,k,m为负, 则需要使用x_i,k的符号上界.求x_i+1,j的上界时同理.

整个递归过程实际上确定了一条回溯路径. 定义函数$ \gamma ({a_{i, j, m}}) = ({\gamma ^ \geqslant }(a_{i, j, m}^ \geqslant ), {\gamma ^ \leqslant }(a_{i, j, m}^ \leqslant )):\mathcal{A} \to \mathcal{A} $, 对任意m∈[M], γ(a_i,j,m)确定了使用x_i,j的第m组符号约束计算数值上下界的回溯路径:

$ a_{1, *, m}←a_{2, *, m}←…←a_{i−1, *, m}←a_{i, j, m}. $

由M组抽象元素a_i,j,m可以确定M条回溯路径, 通过这M条回溯路径, 可得到x_i,j的M个关于输入层表示的符号上下界γ(a_i,j,m). 定义从γ(a_i,j,m)得到数值上下界的具象函数$ {\gamma ^ \star }:\mathcal{A} \to \mathbb{R} \times \mathbb{R} $如下:

$ {\gamma ^ \star }(\gamma ({a_{i, j, m}})) = {\gamma ^ \star }({\gamma ^ \geqslant }(a_{i, j, m}^ \geqslant ), {\gamma ^ \leqslant }(a_{i, j, m}^ \leqslant )) = (\gamma _ \geqslant ^ \star ({\gamma ^ \geqslant }(a_{i, j, m}^ \geqslant )), \gamma _ \leqslant ^ \star ({\gamma ^ \leqslant }(a_{i, j, m}^ \leqslant ))), $

其中,

$ \begin{array}{l} \gamma _ \geqslant ^ \star ({\gamma ^ \geqslant }(a_{i, j, m}^ \geqslant )) = \gamma _ \geqslant ^ \star \left( {\sum\limits_{k = 1}^{{d_1}} {{q_{1, k, m}}{x_{1, k}} + {r_{1, m}}} } \right) = \sum\limits_{k = 1}^{{d_1}} {\frac{{|\delta ({q_{1, k, m}}) + 1|}}{2}{q_{1, k, m}}} {l_{1, k}} + \sum\limits_{k = 1}^{{d_1}} {\frac{{|\delta ({q_{1, k, m}}) - 1|}}{2}{q_{1, k, m}}} {u_{1, k}} + {r_{1, m}}, \\ \gamma _ \leqslant ^ \star ({\gamma ^ \leqslant }(a_{i, j, m}^ \leqslant )) = \gamma _ \leqslant ^ \star \left( {\sum\limits_{k = 1}^{{d_1}} {{q_{1, k, m}}{x_{1, k}} + {r_{1, m}}} } \right) = \sum\limits_{k = 1}^{{d_1}} {\frac{{|\delta ({q_{1, k, m}}) + 1|}}{2}{q_{1, k, m}}} {u_{1, k}} + \sum\limits_{k = 1}^{{d_1}} {\frac{{|\delta ({q_{1, k, m}}) - 1|}}{2}{q_{1, k, m}}} {l_{1, k}} + {r_{1, m}}. \\ \end{array} $

对于x_i,j的数值下界, 若q_1,k,m > 0, 使用x_1,k的下界; 若q_1,k,m < 0, 则使用x_1,k的上界. x_i,j数值上界的计算类似.为了简便, 我们记${\gamma ^ \star }(\gamma ({a_{i, j, m}}))$为$ {\gamma ^ \star }({a_{i, j, m}}) $. 则x_i,j可计算出M个数值上下界$ ({l_{i, j, m}}, {u_{i, j, m}}) = {\gamma ^ \star }({a_{i, j, m}}) $. 它们的交集也是x_i,j的数值上下界, 我们取:

$ [{l_{i, j}}, {u_{i, j}}] = \bigcap\limits_{m = 1}^M {[{l_{i, j, m}}, {u_{i, j, m}}]} $

作为节点x_i,j最终的数值上下界.

抽象元素a_i,j,m的计算取决于神经网络中x_i,j的节点类型. 对于第m∈[M]种抽象方式, 若x_i,j是激活状态不确定的节点, 我们定义其抽象元素a_i,j,m的抽象变换为

$ ReLU_m^\# ({a_{i, j, m}}) = ReLU_m^\# ((a_{i, j, m}^ \geqslant , a_{i, j, m}^ \leqslant )) = (a_{i + 1, j, m}^ \geqslant , a_{i + 1, j, m}^ \leqslant ), $

其中, $ (a_{i + 1, j, m}^ \geqslant , a_{i + 1, j, m}^ \leqslant ) $表示节点x_i+1,j对应的抽象元素, 具体形式为

$ a_{i + 1, j, m}^ \geqslant = {\lambda _m}{x_{i, j}}, {\text{ }}a_{i + 1, j, m}^ \leqslant = \frac{{{u_{i, j}}}}{{{u_{i, j}} - {l_{i, j}}}}({x_{i, j}} - {l_{i, j}}). $

上式中, λ_m∈[0, 1]为常数. 即在每条回溯路径上, 我们对激活状态不确定的节点使用相同的λ_m. 对于激活状态确定的ReLU以及仿射变换函数, 容易定义其准确的抽象变换, 本文省略其具体形式.

DeepPoly对每个节点x_i,j仅维护一组抽象元素a_i,j,1, 是M=1的特例, 其λ₁对应第1.2节所述的启发式策略, 我们称它确定的回溯路径为DeepPoly路径. 使用一条回溯路径仅能得到x_i,j的一个数值上下界[l_i,j,1, u_i,j,1]. 通过维护x_i,j的多组抽象元素, 利用这多组抽象元素构成的多条回溯路径, 我们可以得到x_i,j更多的数值上下界信息. 此外, 多条回溯路径蕴含至少有任何一条回溯路径的效果, 则至少达到DeepPoly的精确程度.

图 5中网络是图 4的扩展, 它展示了使用两条回溯路径计算每个节点数值上下界的过程.

其中, m=1对应DeepPoly路径, 见网络外侧第1行−第4行; m=2对应平行四边形抽象的回溯路径, 见网络外侧第5行−第8行. 网络的输入范围为$\mathcal{X}_1 $={(x_1,1+x_1,2): −1≤x_1,1≤1∧−1≤x_1,2≤1}且每个节点的偏移为0. 对于ReLU层节点x_3,1, 我们维护经过DeepPoly抽象得到的符号约束x_3,1≥0及x_3,1≤0.5x_2,1+1; 同时维护经过平行四边形抽象得到的符号约束x_3,1≥0.5x_2,1及x_3,1≤0.5x_2,1+1. 这两组符号约束作为x_3,1的两个抽象元素构成两条不同回溯路径. 对于DeepPoly路径, 其关于输入层的符号上下界为

$ \begin{array}{l} \gamma ({a_{3, 1, 1}}) = ({\gamma ^ \geqslant }(a_{3, 1, 1}^ \geqslant ), {\gamma ^ \leqslant }(a_{3, 1, 1}^ \leqslant )) \\ = ({\gamma ^ \geqslant }(0), {\gamma ^ \leqslant }(0.5{x_{2, 1}} + 1)) \\ = (0, 0.5{\gamma ^ \leqslant }(a_{2, 1, 1}^ \leqslant ) + 1) \\ = (0, 0.5{\gamma ^ \leqslant }( - {x_{1, 1}} + {x_{1, 2}}) + 1) \\ = (0, 0.5( - {\gamma ^ \geqslant }(a_{1, 1, 1}^ \geqslant ) + {\gamma ^ \leqslant }(a_{1, 2, 1}^ \leqslant )) + 1) \\ = (0, 0.5( - {x_{1, 1}} + {x_{1, 2}}) + 1). \\ \end{array} $

对应的数值下界和上界分别为

$ {l_{3, 1, 1}} = \gamma _ \geqslant ^ \star (0) = 0, $

$ {u_{3, 1, 1}} = \gamma _ \leqslant ^ \star (0.5( - {x_{1, 1}} + {x_{1, 2}}) + 1) = - 0.5{l_{1, 1}} + 0.5{u_{1, 2}} + 1 = 2. $

对于平行四边形抽象对应的回溯路径, 其关于输入层的符号上下界为

$ \begin{array}{l} \gamma ({a_{3, 1, 2}}) = ({\gamma ^ \geqslant }(a_{3, 1, 2}^ \geqslant ), {\gamma ^ \leqslant }(a_{3, 1, 2}^ \leqslant )) \\ = ({\gamma ^ \geqslant }(0.5{x_{2, 1}}), {\gamma ^ \leqslant }(0.5{x_{2, 1}} + 1)) \\ = (0.5{\gamma ^ \geqslant }( - {x_{1, 1}} + {x_{1, 2}}), 0.5( - {x_{1, 1}} + {x_{1, 2}}) + 1) \\ = (0.5( - {\gamma ^ \leqslant }(a_{1, 1, 2}^ \leqslant ) + {\gamma ^ \geqslant }(a_{1, 2, 2}^ \geqslant )), 0.5( - {x_{1, 1}} + {x_{1, 2}}) + 1) \\ = (0.5( - {x_{1, 1}} + {x_{1, 2}}), 0.5( - {x_{1, 1}} + {x_{1, 2}}) + 1). \\ \end{array} $

对应的数值下界和上界分别为

$ {l_{3, 1, 2}} = \gamma _ \geqslant ^ \star (0.5( - {x_{1, 1}} + {x_{1, 2}})) = - 0.5{u_{1, 1}} + 0.5{l_{1, 2}} = - 1, $

$ {u_{3, 1, 2}} = \gamma _ \leqslant ^ \star (0.5( - {x_{1, 1}} + {x_{1, 2}}) + 1) = - 0.5{l_{1, 1}} + 0.5{u_{1, 2}} + 1 = 2. $

我们取x_3,1最终的数值上下界为

$ [l_{3, 1}, u_{3, 1}]=[l_{3, 1, 1}, u_{3, 1, 1}]∩[l_{3, 1, 2}, u_{3, 1, 2}]=[0, 2]. $

按照同样的做法, 可得到x_4,1的数值上下界为[l_4,1, u_4,1]=[−2, 2]. 因此, x_4,1是激活状态不确定的节点, 其对应的抽象变换为

$ ReLU_1^\# ({a_{4, 1, 1}}) = {a_{5, 1, 1}} = (0, 0.5{x_{4, 1}} + 1), $

$ ReLU_2^\# ({a_{4, 1, 2}}) = {a_{5, 1, 2}} = (0.5{x_{4, 1}}, 0.5{x_{4, 1}} + 1). $

由a_5,1,1和a_5,1,2可按照上述方式得到x_5,1的数值上下界为[0, 2]. 在节点x_6,1处, 使用两条回溯路径已经能够得到比DeepPoly更为精确的结果, 因为有:

$ {l_{6, 1, 1}} = \gamma _ \geqslant ^ \star (0.25{x_{1, 1}} - 0.25{x_{1, 2}} - 1.5) = - 2, $

$ {u_{6, 1, 1}} = \gamma _ \leqslant ^ \star ( - 0.25{x_{1, 1}} + 0.25{x_{1, 2}} + 1.5) = 2, $

$ {l_{6, 1, 2}} = \gamma _ \geqslant ^ \star ( - 1) = - 1, $

$ {l_{6, 1, 2}} = \gamma _ \geqslant ^ \star ( - 1) = - 1. $

我们取[l_6,1, u_6,1]=[−2, 2]∩[−1, 1]=[−1, 1], 它包含于DeepPoly得到的数值上下界. 更精确的数值上下界是我们的首要目标, 因为它还可以用来构造更精确的抽象, 从而更精确地近似真正的可达集.

下面证明上述方法的可靠性, 即任意节点x_i,j的任意回溯路径所对应的数值上下界$ {\gamma ^ \star }({a_{i, j, m}}) $, 都是此节点

在ReLU网络中数值上下界的上近似, 这保证我们得到的可达集是ReLU网络的上近似.

注意到a_i,j,m来自对ReLU以及仿射变换函数的抽象变换, 对于激活状态确定的ReLU以及仿射变换函数, 其抽象变换是准确的. 这里只对抽象变换$ ReLU_m^\# $证明可靠性, 其他抽象变换同理. 假设激活状态确定的ReLU以及仿射变换抽象已经具有可靠性.

定理2. 设i为小于网络层数L的任意偶数, 对于任意j∈[d_i]和任意m∈[M], 上述方法得到的数值上下界:

$ [{l_{i + 1, j, m}}, {u_{i + 1, j, m}}] = [\gamma _ \geqslant ^ \star ({\gamma ^ \geqslant }(ReLU_m^\# (a_{i, j, m}^ \geqslant ))), \gamma _ \leqslant ^ \star ({\gamma ^ \leqslant }(ReLU_m^\# (a_{i, j, m}^ \leqslant )))]. $

关于ReLU网络中节点x_i+1,j的数值上下界可靠.

证明: 归纳法. 初始情况i=2时, 显然成立, 因为仿射变换的抽象是可靠的. 假设i=k−2时上式成立, 其中, k为大于等于4的偶数. 即x_k−1,j的数值上下界$[{l_{k - 1, j}}, {u_{k - 1, j}}] = \cap _{m = 1}^M[{l_{k - 1, j, m}}, {u_{k - 1, j, m}}]$是可靠的. 则由仿射变换抽象的可靠性可知, $ [{l_{k, j}}, {u_{k, j}}] = \cap _{m = 1}^M[{l_{k, j, m}}, {u_{, j, m}}] $关于ReLU网络中节点x_k,j的数值上下界可靠. 因为

$ \begin{array}{l} \gamma (ReLU_m^\# ({a_{k, j, m}})) = ({\gamma ^ \geqslant }(a_{k + 1, j, m}^ \geqslant ), {\gamma ^ \leqslant }(a_{k + 1, j, m}^ \leqslant )) \\ \;\;\;\;\; = \left( {{\gamma ^ \geqslant }({\lambda _m}{x_{k, j}}), {\gamma ^ \leqslant }\left( {\frac{{{u_{k, j}}}}{{{u_{k, j}} - {l_{k, j}}}}({x_{k, j}} - {l_{k, j}})} \right)} \right) \\ \;\;\;\;\; = \left( {{\lambda _m}{\gamma ^ \geqslant }(a_{k, j, m}^ \geqslant ), \frac{{{u_{k, j}}}}{{{u_{k, j}} - {l_{k, j}}}}{\gamma ^ \leqslant }(a_{k, j, m}^ \leqslant ) - \frac{{{u_{k, j}}}}{{{u_{k, j}} - {l_{k, j}}}}{l_{k, j}}} \right), \\ \end{array} $

所以有:

$ \begin{array}{l} [{l_{i + 1, j, m}}, {u_{i + 1, j, m}}] = \left[ {\gamma _ \geqslant ^ \star ({\lambda _m}{\gamma ^ \geqslant }(a_{k, j, m}^ \geqslant )), \gamma _ \leqslant ^ \star \left( {\frac{{{u_{k, j}}}}{{{u_{k, j}} - {l_{k, j}}}}{\gamma ^ \leqslant }(a_{k, j, m}^ \leqslant ) - \frac{{{u_{k, j}}}}{{{u_{k, j}} - {l_{k, j}}}}{l_{k, j}}} \right)} \right] \\ \;\;\;\;\; = \left[ {{\lambda _m}\gamma _ \geqslant ^ \star ({\gamma ^ \geqslant }(a_{k, j, m}^ \geqslant )), \frac{{{u_{k, j}}}}{{{u_{k, j}} - {l_{k, j}}}}\gamma _ \leqslant ^ \star ({\gamma ^ \leqslant }(a_{k, j, m}^ \leqslant )) - \frac{{{u_{k, j}}}}{{{u_{k, j}} - {l_{k, j}}}}{l_{k, j}}} \right] \\ \;\;\;\;\; = \left[ {{\lambda _m}{l_{k, j, m}}, \frac{{{u_{k, j}}}}{{{u_{k, j}} - {l_{k, j}}}}{u_{k, j, m}} - \frac{{{u_{k, j}}}}{{{u_{k, j}} - {l_{k, j}}}}{l_{k, j}}} \right] \\ \;\;\;\;\; \supseteq \left[ {{\lambda _m}{l_{k, j}}, \frac{{{u_{k, j}}}}{{{u_{k, j}} - {l_{k, j}}}}{u_{k, j}} - \frac{{{u_{k, j}}}}{{{u_{k, j}} - {l_{k, j}}}}{l_{k, j}}} \right]. \\ \end{array} $

由定理1可知, 若[l_k,j, u_k,j]关于ReLU网络中x_k,j可靠, 则最后一行关于ReLU网络中x_i+1,j可靠, 即定理2成立.

直观而言, 定理2说明: 对于任意激活状态不确定的节点x_i,j, 通过其M组符号约束回溯到输入层得到的数值上下界关于ReLU网络都是可靠的. 于是, 我们的方法得到每个节点真正可达集的上近似.

算法1给出了上述方法的伪代码, 算法输入为网络f、输入范围$\mathcal{X}_1 $以及对应的不安全区域$\bar S$, 算法判断网络f关于$({\mathcal{X}_1}, \bar S)$是否安全. 因为我们把仿射变换和ReLU变换作为分离的两层, 所以需要根据不同的层类型来表示x_i,j. 在第3行, 如果第i层为仿射变换层, 那么需要用i−1层节点仿射变换表示x_i,j. 这里, w_i,j和b_i,j分别表示节点x_i,j的权重向量和偏移, x_i−1表示i−1层所有节点构成的向量. 仿射变换的抽象表示是准确的, 我们把这个准确的约束作为其抽象a_i,j,m. 利用每个a_i,j,m回溯可得到M个数值上下界[l_i,j,m, u_i,j,m], 取它们的交集作为x_i,j最终的数值上下界, 如第4行−第7行所示. 当第i层节点的数值上下界计算完成, 就可以得到本层节点的可达集$\mathcal{X} $_i, 如第13行所示. 对于仿射变换层节点, 其更精确的可达集在第10行被用来构造更精确的M种ReLU抽象. 按照相同的方法, 在第12行得到ReLU层节点的数值上下界. 第14行得到输出层节点可达集后, 就可以判断网络f可达集与不安全区域$\bar S$是否有交集: 如果没有交集, 返回SAFE, 说明f关于$({\mathcal{X}_1}, \bar S)$安全, ; 否则, 返回UNKNOWN, 因为此时不能保证f真正的可达集与$\bar S$有交集.

算法1. 验证一个网络关于一个输入范围是否安全.

输入: 网络f, 输入范围$\mathcal{X}_1 $和不安全区域$\bar S{\text{.}}$

输出: 如果安全, 返回SAFE; 否则, 返回UNKNOWN.

1.  for i←1 to L do        //L为网络f的层数

2.    for j←1 to d_i do        //d_i为第i层节点数

3.     if layer_type[i]=AFFINE then       //如果第i层为仿射变换层

4.      for m←1 to M do       //构造仿射变换函数抽象

5.       a_i,j,m←(w_i,jx_i−1+b_i,j, w_i,jx_i−1+b_i,j)

6.       $ [{l_{i, j, m}}, {u_{i, j, m}}] \leftarrow [\gamma _ \geqslant ^ \star ({\gamma ^ \geqslant }(a_{i, j, m}^ \geqslant )), \gamma _ \leqslant ^ \star ({\gamma ^ \leqslant }(a_{i, j, m}^ \leqslant ))] $

7.       $[{l_{i, j}}, {u_{i, j}}] \leftarrow \cap _{m = 1}^M[{l_{i, j, m}}, {u_{i, j, m}}]$       //取M个数值上下界的交集

8.      if layer_type[i]=RELU then       //如果第i层为ReLU层

9.       for m←1 to M do       //对于x_i,j, 用x_{i-1, j}构造M种ReLU抽象

10.        $ {a_{i, j, m}} \leftarrow ReLU_m^\# ({a_{i - 1, j, m}}) $

11.        $ [{l_{i, j, m}}, {u_{i, j, m}}] = [\gamma _ \geqslant ^ \star ({\gamma ^ \geqslant }(a_{i, j, m}^ \geqslant )), \gamma _ \leqslant ^ \star ({\gamma ^ \leqslant }(a_{i, j, m}^ \leqslant ))] $

12.       $[{l_{i, j}}, {u_{i, j}}] \leftarrow \cap _{m = 1}^M[{l_{i, j, m}}, {u_{i, j, m}}]$

13.     $\mathcal{X} $_i←[L_i, u_i]       //得到$\mathcal{X} $_i为第i层节点的可达集

14. if $ {\mathcal{X}_L} \cap \bar S = \emptyset $ then       //如果输出层可达集与不安全区域交集为空

15.    return SAFE

16. else

17.    return UNKNOWN

上近似方法(如算法1)返回UNKNOWN时, 说明它得到的可达集$\mathcal{X} $_L与$\bar S$有交集, 但$\mathcal{X} $_L是放大的可达集.虽然无法确定真正的可达集是否与$\bar S$存在交集, 然而可以利用求解过程中得到的信息进一步求得更为精确的可达集, 这一过程称为精化. 文献[16, 17]均采用这种想法, 以得到更为准确的验证结果.

算法1继承了基于简单线性抽象的符号传播方法的高效性, 其时间复杂度为Ο(MN²), 其中, N为网络f的节点数量. 对于每个节点, 回溯计算其数值上下界的时间代价是Ο(N). 回溯路径的数量M一般取低值常数, 我们将在第3.2节讨论关于M的取值. 算法1的空间复杂度是Ο(N), 对每个节点保存常数项个约束.

理论上, 回溯路径的数量可以任意多, 即M值可以任意大. 那么一个值得关心的问题是, 任意多的回溯路径能够达到多好的精度? 在第3.2节, 我们研究了随M值增加, 精度的改善效果.

3 实验与评估

和绝大部分工作一样, 我们关注对具体输入的无穷范数扰动, 并关注给定网络在无穷范数扰动下的鲁棒性. 首先, 无穷范数扰动由无穷范数距离定义.

定义2(无穷范数距离). 给定两个n维向量x=(a_i), z=(b_i), 其中, 1≤i≤n, 它们的无穷范数距离d_∞(x, z)被定义为${d_\infty }(x, z) = \mathop {\max }\limits_{1 \leqslant i \leqslant n} |{a_i} - {b_i}|.$

通常, 输入范围$\mathcal{X}_1 $由上述度量给出, 即给定具体输入x和扰动大小θ, $\mathcal{X}_1 $=$ \mathcal{B}$_∞(x, θ)$ \buildrel \Delta \over = ${z|d_∞(x, z)≤θ}. 直观而言, $\mathcal{X}_1 $是x每个维度最大允许加或减θ所构成的向量集.

对于分类网络的验证问题, 若给定输入, 鲁棒半径能够很好地量化比较不同上近似方法的精度. 下面是无穷范数距离下鲁棒半径的定义, 在后文中简称为鲁棒半径.

定义3(d_∞鲁棒半径). 对于分类网络f, 给定输入x及对应标签label(x), f关于x的d_∞鲁棒半径被定义为

$ R_{f}(\boldsymbol{x})=\max \left\{\left\{\theta \geqslant 0: f(\boldsymbol{z})={label}(\boldsymbol{x}), \forall \boldsymbol{z} \in \mathcal{B}_{\infty}(\boldsymbol{x}, \theta)\right\} \cup\{0\}\right\}. $

对于分类网络, 上述定义中, f(z)=label(x)蕴含我们对不安全区域$\bar S$的选择是x正确标签以外的所有标签, 即针对无目标攻击^[18]的鲁棒性. 直观而言, 网络f关于输入x的鲁棒半径, 就是在不产生对抗样本的前提下, 能对x施加的最大扰动θ.

若f是归一化输入的网络, 则鲁棒半径R_f(x)∈[0, 1]. 通常使用二分法计算R_f(x)的值: 取θ₁=1/2作为初始值, 在第i次迭代中, 确定网络f关于扰动θ_i后的输入范围是否鲁棒.

● 如果不鲁棒, 将θ_i+1=θ_i−(1/2)ⁱ⁺¹作为下一个取值;

● 如果鲁棒, 则将θ_i+1=θ_i+(1/2)ⁱ⁺¹作为下一个取值.

重复上述迭代过程, 直至找到满足精度要求的θ_i, 将其作为鲁棒半径R_f(x)的值.

给定神经网络和输入, 上近似方法计算得到的鲁棒半径一般小于真正的鲁棒半径, 因为上近似产生的误差通常会放大求得的可达集. 因此, 可以用不同方法计算得到的鲁棒半径来定量比较这些方法的精确度. 如果某种上近似方法得到的鲁棒半径更大, 即更接近真正的鲁棒半径, 则说明该上近似方法更精确.

我们将提出的多路径回溯方法实现为AbstraCMP工具, 其命名来源于该方法在神经网络各节点处对几种抽象(abstraction)的回溯结果进行比较(CMP). AbstraCMP使用Python 3.9实现, 其源代码以及实验结果可以在文献[19]获取. 本节我们在数据集ACAS Xu, MNIST和CIFAR10上将多路径回溯方法与使用单条回溯路径的DeepPoly进行定量比较, 在数据集MNIST上将多路径回溯方法与使用全局优化的Optimized LiRPA进行定量比较. 下面介绍实验使用的数据集和环境.

● ACAS Xu^[20]网络用于小型无人机设备的防撞规避系统, 由45个全连接前馈ReLU网络组成. 这45个网络规模相同, 均为6×50, 其中, 6表示隐藏层层数, 50表示每个隐藏层节点个数. 每个ACAS Xu网络输出层是5维, 分别表示网络给出的5种碰撞规避决策. 输入层是5维, 分别表示与其他飞行设备的距离及角度等5个参数, 是低维输入网络的代表.

● MNIST^[21]是包含0−9这10个手写数字图像的数据集, 包含6万个训练样本以及1万个测试样本. 每个样本都是灰阶图像且大小均为28×28像素. 我们使用MNIST训练数据集训练了规模分别为16×50, 10×80及20×50的3个全连接前馈ReLU网络, 每个网络的输出层是10维, 分别表示网络给出的10个分类结果. 输入层为28×28=784维, 表示一张图片的784个灰度值, 是较高维输入网络的代表.

● CIFAR10^[22]是包含10种物体图像的数据集, 包含5万个训练样本以及1万个测试样本. 每个样本都是3通道RGB图像, 且大小均为32×32像素. 我们使用CIFAR10训练数据集训练了规模分别为10×100, 15×200及16×250的3个全连接前馈ReLU网络, 每个网络的输出层是10维, 分别表示网络给出的10种分类结果. 输入层为3×32×32=3072维, 表示一张图片的3 072个灰度值, 是高维输入网络的代表.

上述ACAS Xu网络和MNIST网络均使用归一化输入训练, 因此, 关于某个给定输入的扰动是归一化后的扰动, 关于给定输入的鲁棒半径也是归一化后的鲁棒半径.

我们使用的实验平台参数为: 处理器Intel Core i7-6700@3.40 GHz; 内存大小16 GB; 操作系统版本Windows 10专业版64位; Python版本3.9. 与DeepPoly的对比实验均在相同环境下进行.

3.1 低维输入网络上的精度改善

对于ACAS Xu, 为了方便对比, 我们选择了4个随机合法输入, 分别通过AbstraCMP和DeepPoly计算这4个输入在45个网络上的鲁棒半径. 本实验中, 设定鲁棒半径精确到千分位; AbstraCMP使用M=3, 3条回溯路径分别为DeepPoly路径、直角三角形抽象对应的回溯路径和钝角三角形抽象对应的回溯路径. 结果如图 6所示.

图 6(a)展示了对于输入1, AbstraCMP和DeepPoly在45个网络中能够验证的鲁棒半径. 其中, 深蓝色区域的上边界为AbstraCMP能够验证的鲁棒半径, 浅橙色为DeepPoly能够验证的鲁棒半径. 从图中红色虚线可以看出, 在第11个网络上, 两种方法得到的鲁棒半径分别为0.053和0.04. 第2节中提到: 对于任意输入和任意网络, AbstraCMP在理论上保证至少达到DeepPoly的效果. 因此, AbstraCMP可验证的鲁棒半径(深蓝色区域)总是大于DeepPoly可验证的鲁棒半径(浅橙色区域). 通过图 6(b)−图 6(d)均能观察到同样的结论. 对于上近似方法, 同一输入下能验证更大的鲁棒半径, 意味着对真正可达集更精确的近似. 本实验中, AbstraCMP能够验证的单个鲁棒半径最大比DeepPoly提高370%; 对于每个输入, 在45个网络上能够验证的鲁棒半径平均值比DeepPoly提高25−30%. 实验结果表明, AbstraCMP在低维输入网络中的计算精度相比DeepPoly有所提升.

3.2 回溯路径数量对精度和时间的影响

在第2节提到: 理论上, 回溯路径可以任意多. 通过下面的实验, 我们将研究回溯路径数量的增加对鲁棒半径计算的改进以及带来的时间代价. 我们选定一个ACAS Xu网络, 并选定一个输入, 然后计算使用不同数量的回溯路径时, AbstraCMP所能验证的鲁棒半径大小以及对应的时间开销.

关于回溯路径的选择, 首先, 我们选取DeepPoly路径作为M=1的配置; 此外, 由于定理1中任意λ∈[0, 1]都构成对ReLU激活函数的可靠抽象, 所以我们选取[0, 1]区间的等分值构成若干条回溯路径. 具体而言, M=2时包含DeepPoly和λ=0两条回溯路径; M=3时包含DeepPoly和λ=0及λ=1共3条回溯路径; M=4时包含DeepPoly及λ=0, 0.5, 1共4条回溯路径; 以此类推. 本实验中设定鲁棒半径精确到千分位, 得到AbstraCMP能够验证的鲁棒半径随M值的变化如图 7所示.

图 7中, 带有三角形标签的蓝色实折线表示在给定网络和输入下, 随回溯路径数量M增加, AbstraCMP能够验证的鲁棒半径变化. 橙色虚线表示DeepPoly在该网络和输入下能够验证的鲁棒半径, 虽然DeepPoly没有回溯路径的概念, 但为了方便对比, 我们将其能够验证的鲁棒半径0.026作为基准线. 从图 7可以看出, 在DeepPoly的基础上, 增加较少的回溯路径就能取得相对于DeepPoly较好的效果. 在本实验的网络和输入下, 仅使用M=2, 即可使计算得到的鲁棒半径相对于DeepPoly提高57%.

M值的增加可以获得更为精确的结果, 但这种改善并不能持续. 在该实验中, 我们发现: 随M值增加, AbstraCMP能够验证的鲁棒半径会迅速收敛. 如图 7所示, 当M=7时, 就已经达到收敛值0.049. 其他实验表明, 对于大部分输入, 通常M=3或M=4已经接近收敛值. 因此, 为了平衡精度与时间, 我们认为M=3是一个较为合理的选择.

表 1给出了在上述网络和输入下, AbstraCMP计算其鲁棒半径所需时间随回溯路径数量M的变化关系. 表中第2列是DeepPoly的用时, 第3列M=2及之后各列是取不同M值时AbstraCMP的用时. 对于每一列的配置, 实验记录其运行10次的平均时间. 正如第2节的讨论, AbstraCMP的时间代价与回溯路径数量M线性相关, 从表 1中也可以看出这一关系. DeepPoly解决神经网络验证问题的时间代价是极低的, 当M取低值常数时, AbstraCMP相较于现有验证方法而言时间代价也是极低的. 我们的方法所引入的额外时间代价很小.

值得注意的是, 我们的方法在效率上存在较大的提升空间. AbstraCMP目前虽然使用简单的单线程实现, 但多路径回溯方法在理论上可以高度并行化. 对于单条回溯路径, 同层各节点的数值上下界计算可以并行进行. 在文献[23]中, 作者介绍了DeepPoly的GPU实现. 而对于AbstraCMP, 除同层各节点的并行以外, 同一节点不同回溯路径对应的数值上下界也可以并行计算, 以充分利用CPU甚至GPU的计算能力, 这将作为我们未来的一个工作方向.

3.3 高维输入网络上的精度改善

最后, 我们在数据集MNIST和CIFAR10上测试了AbstraCMP在高维输入网络上的表现. 对于MNIST数据集, 我们使用其训练集训练了3个全连接前馈神经网络, 它们的隐藏层规模分别为16×50, 10×80和20×50.我们选择测试集的前100张图片作为输入. 对比AbstraCMP和DeepPoly在不同扰动大小θ下能够成功验证鲁棒性的图片数量. 对于上近似方法, 给定一组输入和具体的θ值, 能够验证的鲁棒性越多, 自然说明这种方法越精确. 本实验中, AbstraCMP取M=3, 结果见表 2.

从表 2中可以看到, 对于同一网络和相同的扰动大小, AbstraCMP能够验证的图片数量总是大于DeepPoly. 例如, 在网络MNIST 20×50上, 选定扰动大小θ为0.010时, DeepPoly能够验证鲁棒的图片数量是73, 而AbstraCMP能够验证80张图片的鲁棒性. 实验结果表明, AbstraCMP在较高维输入网络上的计算精度相比DeepPoly同样有所提升.

在本实验中, 对相同的扰动大小, AbstraCMP能够成功验证的图片数量最多比DeepPoly多42.9% (=(10−7)/7), 此情况出现在MNIST 20×50网络且扰动大小θ=0.030时. 而且从实验结果可以观察到: 当网络隐藏层数量较多时, AbstraCMP相比DeepPoly提升更加明显. 产生这一结果的原因是: 随着网络深度的增加, 多路径回溯方法在每个节点相较于单路径回溯提升的精度得到积累和放大.

对于CIFAR10数据集, 我们使用其训练集训练了隐藏层规模分别为10×100, 15×200及16×250的3个全连接前馈神经网络. 只有ReLU层的全连接CIFAR10网络相对于MNIST网络有较低的准确率和较小的鲁棒半径, 因此对于每个网络, 我们选择测试集分类正确的前100张图片作为输入, 对比AbstraCMP和DeepPoly在不同的扰动大小θ下, 能够成功验证鲁棒性的图片数量. 本实验中, AbstraCMP取M=3, 结果见表 3.

在本实验中, 对相同的扰动大小, AbstraCMP最多能够比DeepPoly多验证12张图片的鲁棒性, 此情况出现在扰动大小为0.003 5及网络规模为15×200时. 且在扰动大小为0.003 5时, AbstraCMP在3个网络上平均比DeepPoly多验证8张图片的鲁棒性.

上述3组实验说明, 在不同规模的输入和网络下, AbstraCMP的验证精度相较于DeepPoly均有所提升.

3.4 与Optimized LiRPA的精度比较

文献[24]提出了Optimized LiRPA工具, 与本文类似, 它对ReLU函数使用简单线性抽象; 不同的是, 它取ReLU抽象下界斜率λ为变量非具体值, 鲁棒性验证问题被转化为关于一组λ的非凸全局优化问题. 通过投影梯度下降等方法可以高效地求解.

虽然与本文使用不同的方法, 但Optimized LiRPA也是基于简单线性抽象的符号传播方法, 而且也是利用不同的λ以得到尽可能精确的验证结果. 因此我们认为, 有必要将本文方法与Optimized LiRPA在验证精度上相比较.

在本实验中, 我们取MNIST测试集的前10张图片作为输入, 分别使用AbstraCMP和Optimized LiRPA计算10个输入在两个MNIST网络上的鲁棒半径, 以比较两种方法的精度差异. 本实验中, 取AbstraCMP的M=3; 使用Optimized LiRPA的原生实现且其梯度下降的迭代次数为50次; 设定鲁棒半径精确到千分位. 得到的结果如图 8所示.

图 8的柱形图中, 左边深蓝色柱形表示AbstraCMP在给定输入下得到的鲁棒半径, 相邻的浅橙色柱形表示Optimized LiRPA在给定输入下得到的鲁棒半径. 如图 8(a)中MNIST 6×50网络上, AbstraCMP和Optimized LiRPA得到输入1的鲁棒半径分别为0.014和0.008. 从图 8可看出, 两种网络规模下, AbstraCMP得到前10张图片的鲁棒半径均大于Optimized LiRPA, 说明我们的方法相对于使用参数化λ的梯度下降方法仍然具有精度优势.

3.5 与LP-ALL的精度比较

文献[25]中, 作者Salman等人将单个神经网络节点的线性凸松弛方法统一为框架, 并说明这类方法存在精度上限. 对于ReLU网络, 文中将其精度上限对应的方法称为LP-ALL. LP-ALL逐层、逐节点构造LP问题以得到每个节点的数值上下界, 并使用得到的数值上下界构造ReLU抽象. 这是目前ReLU网络单个节点的线性凸松弛方法能够得到的最精确上下界. 另一方面, LP-ALL需要解Ο(N)个LP问题, 其中, N为给定网络的节点数目, 且平均每个LP问题的变量数目为Ο(N)个, 这使得目前LP-ALL对于较大规模网络是不太现实的方法.文献[25]中使用1 000 CPU节点的集群计算了MNIST全体测试集图片对于给定扰动大小的鲁棒比例, 实验使用1×500和2×100两种规模的MNIST网络, 总计算量已经超过22 CPU年.

本节中, 我们将定量比较LP-ALL, AbstraCMP和DeepPoly的验证精度. 具体来说, 我们选择第3.3节中的两个网络: MNIST 10×80和MNIST 16×50, 每个网络分别选择10张图片作为输入, 比较3种方法得到这10个输入的鲁棒半径. 其中, AbstraCMP使用M=3, LP-ALL求解器使用与文献[25]相同的ECOS. 实验中设定鲁棒半径的精度阈值为千分位, 得到的结果如图 9所示.

从图 9中可看出, 正如Salman等人在文献[25]中提到的, LP-ALL作为一种复杂度很高的方法, 却不能显著提升已有线性近似方法的验证精度. 对于本实验使用的全体输入集, LP-ALL得到一个千分位鲁棒半径平均耗时148×10³ s (约41 h), 但其精度相较DeepPoly仅平均绝对提升0.005 0; 而AbstraCMP得到一个千分位鲁棒半径平均耗时435 s, 其精度相较DeepPoly已具有0.002 3的平均绝对提升.

同时, 由图 9也可知, AbstraCMP在精度上弥补了DeepPoly和LP-ALL的间隙, 使得时间复杂度较低的回溯方法能够更加接近LP-ALL的验证效果.

4 相关工作

根据验证结果的保证程度划分, 本文提出的方法可靠但不完备. 对于ReLU网络, 可靠且完备的方法通常需要对激活状态不确定的ReLU节点分情况讨论. 按照实现技术不同, 这类方法可大致分为4组.

(1) 基于SMT. 在实现上, 将验证问题编码为可满足性问题来求解^{[7, 14, 26]}, ReLU函数可用SMT的if-then- else语句编码.

(2) 基于混合整数线性规划(MILP). 在实现上, 将验证问题编码为MILP问题, ReLU函数的激活与不激活状态分别对应整数决策变量的1和0, 从而可以使用Gurobi等支持MILP的求解器求解^[27−29].

(3) 基于分支定界(BaB). 在实现上, 直接根据各种启发式策略来确定对哪个激活状态不确定的节点进行分支^{[24, 30]}. 另外, 目前也有工作使用图学习来指导节点的分支^[31].

(4) 基于输入域精化. 通过反复分割输入域构成验证子问题, 在足够小的输入域下, 神经网络接近线性函数, 这使得可以分别验证这些子问题, 直到得到准确的验证结果或者超时^[12].

前3组基于SMT, MILP以及BaB的方法本质上都是对激活状态不确定的节点进行分情况讨论, 所以最坏情况下, 需要描述能够确定该神经网络的2^N个线性函数, 其中, N为网络节点数量. 文献[7]也证明了其NP时间复杂度. 虽然已有很多高效的启发式策略来缓解这一复杂度, 但目前, 使用这类方法验证大规模网络仍然是不现实的.

对于使用线性抽象的方法, 通常越精确的抽象对真正可达集的近似程度越高. 值得注意的是, LP抽象虽然是单个ReLU函数的最精确线性抽象, 但并非对ReLU神经网络的最精确线性抽象, 它没有考虑同层多个节点取值的依赖关系. 利用这些依赖信息, 通常能够得到比LP更精确的抽象, 文献[27, 32]都采用了这种想法.但另一方面, 通常越精确的抽象其时间代价也相对越高. 文献[33]中给出: 对于计算给定输入范围下神经网络的可达集这一问题, 除非P=NP, 否则不存在近似率为(1−o(1))lnN的多项式时间算法, 其中, N为网络节点数量.

文献[25]将单个神经网络节点的线性凸松弛方法统一为框架, 并从理论和实验上说明单个节点的线性凸松弛方法与未松弛的原网络验证问题之间有难以弥补的间隙, 作者称这一间隙为convex barrier. 本文基于简单线性抽象的符号传播方法在其框架中属于greedy algorithm的范畴, 在文献[34]中被称为界限传播(bound propagation)方法. 但在多路径回溯的概念下, 目前这类方法均使用单条回溯路径, 因此仅能得到每个节点的一个上下界. 使用多条回溯路径可以得到每个节点的多个上下界, 从而提升验证精度.

目前已有一些工作改进基于线性抽象的符号传播方法的精度, 如RefineZono^[16]选择性地使用LP甚至MILP来得到部分节点更精确的上下界以及DeepSRGR^[17]将LP和DeepPoly相结合迭代地进行验证. 这些方法都能有效提高验证精度, 但它们都不同程度地引入LP问题的求解, 具有较高的时间代价. 相比之下, 本文是完全基于简单线性抽象的符号传播方法, 在引入较低时间代价的同时, 可获得较高的精度提升. 另外, 本文的方法也可以结合LP等更加复杂但精度更高的方法, 从而进一步提高验证精度.

5 结论

在对神经网络上近似处理的验证方法中, 基于线性抽象的符号传播方法具有很强的代表性, 它在精度与时间之间进行了折中: 一方面, 它不像区间算术一样十分不精确, 以至于难以验证有意义的性质; 另一方面, 也不像LP一样十分耗时, 以至于难以处理较大规模的网络. 本文提出了多路径回溯的概念, 将目前基于简单线性抽象的符号传播方法从单条回溯路径扩展到多条回溯路径, 并分析了多条回溯路径的可靠性和复杂度. 实验结果也表明, 我们的方法能够明显提高验证精度, 而仅引入较小的额外时间代价.

值得注意的是, 虽然本文仅关注激活函数为ReLU的神经网络验证问题, 但我们的方法不仅适用于ReLU函数, 同样适用于其他能够被线性抽象的激活函数, 如tanh和sigmoid等, 这将作为我们接下来的一个扩展方向. 另一方面, 尽管我们的方法可以取任意多条回溯路径, 但每条路径使用单一的抽象方式. 如果能够在单条回溯路径上有效地选择不同的抽象方式, 理论上精度能够获得进一步的提升. 使用全局优化方法的Optimized LiRPA实际上提供了找到一组较好λ的思路. 类似的想法还有文献[35], 作者把验证问题对应的两阶段凸优化问题重构为非凸问题, 从而能够求解更大规模的网络. 最优化方法对于神经网络验证具有重要影响, 因为这一问题本身就对应于优化问题, 未来我们也将会探讨本文方法与优化方法的联系.