基于线性规划的分类深度神经网络鲁棒性验证

111418基于线性规划的分类深度神经网络的鲁棒性验证王琳1、2、3杨正峰2陈欣3赵庆业3李祥坤2刘志明4何继峰21浙江理工大学2华东师范大学上海市可信计算重点实验室3南京大学软件新技术国家重点实验室4西南大学linwang@zstu.edu.cn，zfyang@sei.ecnu.edu.cn，chenxin@nju.edu.cnqingyezhao@foxmail.com，xkli@stu.ecnu.cn，zhimingliu88@swu.edu.cn，jifeng@sei.ecnu.edu.cn摘要迫切需要验证分类深度神经网络（CDNN）的鲁棒性，因为它们嵌入在许多安全关键型应用中。现有的鲁棒性验证方法依赖于输出集的过逼近计算，由于逼近 过 程 中 伴 随 着 误 差 积 累 ， 很 难 推 广 到 实 际 的CDNN。在本文中，我们开发了一种新的方法，用于稳健性验证的CDNN与sigmoid激活函数。该方法将鲁棒性验证问题转化为一个等价的检测输入区域中最可疑点的问题，从而构成一个非线性优化问题。为了使其易于处理，通过将非线性约束放宽到线性包含- s中，将其进一步细化为线性规划问题。我们在一些最先进的基准测试中对几个训练用于图像分类的CDNN进行了比较实验，显示了我们的精度和可扩展性的优势，使实际CDNN的有效验证成为可能。1. 介绍分类深度神经网络（CDNN）是一种特殊类型的深度神经网络，它接受复杂的高维输入，通过多层神经元对其进行转换，并最终将其识别为特定的输出标签或类别。 作为分类器，它们一直在*通讯作者。这项工作得到了2017年YF基金资助的国家重点研发计划的B1001801 ， 部 分 由 中 国 国 家 自 然 科 学 基 金 资 助 61772203 ，61602348，61690204，61632015，61672435，61732019、61751210和61572441，部分由上海自然科学基金资助，资助号为17ZR 1408300，部分由软件新技术与产业化协同创新中心资助，部分由西南大学资助，资助号为SU 116007。在各种应用中采用，如自适应控制[31，34]，模式识别[28]，图像理解，ing [8，18]，网络安全[29]，语音和音频分析[14，15]和自动驾驶[26]。在安全关键系统中嵌入CDNN以像人类专家一样做出判断是一个不断增长的趋势[19]。不幸的是，许多研究人员[3，32]报告称，CDNN在扰动方面不稳健。例如，对输入图像应用人眼无法感知的最小变化，可能会使经过良好训练的CDNN对其进行错误分类。不鲁棒的问题显然会引起使用神经网络的安全关键系统的潜在安全问题，并需要有效的验证技术来检查CDNN的鲁棒性[11，17]。 我们指出，当给定指定区域内的每个可能输入值时，CDNN是鲁棒的，其输出保证具有相同的分类标签，这对应于分类的主要鲁棒要求：最小扰动（由阈值限制）不应影响分类结果。给定一个CDNN，其鲁棒性可以通过估计输出集相对于给定输入区域的范围来验证提出了一些方法来计算特定类型的CDNN的输出范围[2，6，12，22]。将局部梯度下降搜索与全局混合整数线性规划相结合的方法基于多面体操纵的方法能够计算具有ReLU激活函数的CDNN的精确输出区域，并将多面体的并集作为其输入集[35]。一般情况下，输出集的计算是非常困难的，因为处理一般激活函数的理论是不可判定的。将CDNN的验证问题转化为程序设计问题的方法受到了广泛的关注。111419近年来的。建议扩展单纯形方法以处理ReLU节点施加的约束的方法，将SAT求解与线性规划和线性逼近相结 合 的 方 法 可 以 处 理 具 有 分 段 线 性 激 活 函 数 的CDNN[10]。ReLU的分段线性特征使得配备ReLU的CDNN的验证更加容易[5，25]。对于非线性激活函数，如S型函数，研究了基于逼近的方法.抽象-细化方法引入分段线性函数来近似S形激活函数，将网络编码为一组线性约束，然后通过求解器HYSAT [24]求解它们。基于离散化的方法使用逐层分析和SMT技术来验证用于图像分类的CDNN [16]。基于模拟的方法将输出范围估计问题公式化为最大灵敏度，其可以通过求解凸优化问题链来计算[36]。由于近似引起的误差在网络中逐层传播，因此这些基于近似的方法在遇到实际的CDNN时容易失败。如何提供足够的精度和可扩展性以满足实际CDNN的验证要求是验证方法必须面对的关键挑战本文提出了一种新的方法来验证配备激活函数的CDNN的鲁棒性：乙状结肠它不是计算输出集相对于给定输入区域的过近似，而是将鲁棒性验证问题转换为在输入区域中找到比该区域中的任何其他点更容易被分配有不同标签的点的问题，并检查该点是否会被误分类。具体来说，我们建立了一个等价的优化问题，其中网络中神经元之间的关系被编码为约束，目标函数旨在找到输出值之间的最小差异，相对于所需的标签和其他标签。由于期望的标签应该具有最大值，所以优化问题的最优性是正的当且仅当鲁棒性保持。通过将约束中的非线性S形函数替换为线性包含，进一步放松了优化问题，以便线性规划（LP）求解器可以工作。更确切地说，S形函数包含在一个封闭的多面体中，该多面体由有界导数和线性包含相结合而产生。导出的优化问题构成了验证的充分条件，因为其约束的可行集是原始约束的超集。所提出的方法与现有方法相比具有两个优点：1.它通过检查输入区域中的最坏点是否将被分类为不同的类别来验证鲁棒性。从而对CDNN的鲁棒性提供了更精确的估计。2.它可以安全地扩展到现实规模的网络，这超出了现有的网络。这是支持的比较实验上产生的CDNN从许多国家的最先进的基准。本文的主要贡献概括如下：1.我们提出了一种新的方法来验证CDNN的鲁棒性，它将鲁棒性验证问题转化为一个等价的优化问题。2.我们提出了一种新的计算方法，通过近似激活函数sigmoid与一个紧密封闭的区域，然后利用LP求解器来解决它。3.我们在一组由许多最先进的CDNN组成的基准上进行了对比实验，这表明我们在精度和可扩展性方面的优势，使实用的CDNN得到验证。本文的结构如下。第2节介绍了CDNN的一些概念，然后描述了鲁棒性验证问题。第三节将鲁棒性验证问题转化为一个非线性优化问题，提出了一种基于线性规划的计算方法。我们在基准测试上进行了实验，在第5节得出结论之前，在第4节中证实了我们的算法的有效性。2. 预赛记法设N和R分别为自然数集和实数域;n表示由不大于n的正整数组成的集合，即，n={1，2，. . .，n}，其中n是正整数，I表示开区间（0，1），Is表示与正整数s的笛卡尔积Is=I ×···×I.2.1. 深度神经网络深度神经网络（DNN）由一个输入层、一个输出层和其间的多个隐藏层组成。DNN中的神经元（所谓的节点）被布置在不相交的层中，其中一层中的每个神经元连接到下一层，但是同一层中的神经元之间没有连接。此外，隐藏层中的每个神经元的输出通过前一层的神经元输出的线性组合来分配，然后应用非线性激活函数。形式上，DNN定义如下。定义1（深度神经网络）深度神经网络N是元组L，X，W，B，Φ，其中• L={L[0].. .，L[n]}是层的集合，其中层L[0]是输入层，L[n]是输出层，并且L[1]，.. .，L[n-1]是隐藏层。每一层L[k]，0≤k≤ n与一个sk维向量空间kRsk相关联，其中每一个维度对应于一个神经元。111420• X ={x[0]，. . .，x[n]}，其中x[k]是对应于层L[k]中的神经元的值的向量，其中0≤k≤ n。• W={ W[1]，. . .，W[n]}是权矩阵的集合。每个非输入层L[k]（1≤k≤ n）都有一个权重矩阵W[k]∈Rsk×sk−1，L[k]中的神经元通过权重矩阵W[k]连接到前一层L[k−1]的神经元。• B={b[1]，. . .，b[n]}是偏置向量的集合。对于每个非输入层L[k]，其中1≤k≤ n，偏置向量b[k]∈Rsk用于为L[k]中的神经元分配偏置值。• Φ={Φ[1]，. . . ，n[n]}是一组激活函数- sn[k]：nk−1→ n k，每个非输入层L[k]对应一个，其中1 ≤ k ≤ n。此外，L [ k ]中的神经元的值向量x[k]由x[k-1]的值向量与权重矩阵W[k]、偏置向量 b[k] 和 激 活 函 数 k[k] 确 定 ， 即 ， x[k]=k[k]（W[k]x[k−1]+b[k]），其中激活函数k[k]被逐元素地应用。给定一个DNNN：nL，X，W，B，Φn，可以看出第k-1层的输出是第k层的输入从映射的角度来看，每个非输入层L[k]，1≤k≤n，定义了一个函数fk：Rsk−1→Rsk，其中f k（x）=W[k]（W[k]x + b[k]）.（一）因此，N的行为由复合函数f：Rs0→Rsn定义，其定义为：f（x）=fn（fn−1（···（f1（x）.（二）根据通用近似定理[27]，它保证了原则上DNNN能够近似任何非线性实值函数。尽管逼近非线性函数的能力令人印象深刻，但由于DNN的非线性和非凸性，在预测N2.2. 深度神经网络的分类及其鲁棒性在 本 小 节 中 ， 我 们 将 介 绍 分 类 深 度 神 经 网 络（CDNN）的概念，并描述CDNN的鲁棒性验证问题。CDNN是深度神经网络的主要应用之S.在这种类型的网络中，CDNN将充当分类器，用于指定某些输入属于哪个标签。给定具有输入x[0]的CDNNN：kL，X，W，B，Φk，层k中x[k]的激活为x[k]=fk（fk−1（·· ·（f1（x[0]），x[n]的外激活，put层可以通过（2）中所示的层传播，即x [n]= f（x [0]）∈ Isn。要求分类决策产生一个函数基于输出值x[n]，通过选择x[n]中最大元素对应的索引，将x[0]赋值给标签∈sn。因此，函数f是argmax和f的合成，即，f（x[0]）= arg max（f（x[0]））= arg max（x[n]）。（四）1≤n ≤sn为了使输入x[0]被分类，输出x[n]的最大元素必须是唯一的。换句话说，=（x[0]）这意味着x[n]>x[n]，对于所有的n=n。ℓℓ˜为了本文的目的，我们假设所有的N中的权重矩阵W和偏置向量B具有固定值。有关权重和偏倚选择的概述以及对以前工作的回顾，请参见[13]。观察给定DNN的组成，证明其属性的困难是由激活函数的存在引起的。激活函数通常是将前一层的神经元值连接到下一层的神经元值的非线性函数。有一些典型的激活函数- s，例如sigmoid，整流线性单元（ReLU）和tanh函数[13]。在本文中，我们只关注具有广泛使用的sigmoid激活函数x=1。（三）1 +e−x我们扩展了x（x）的定义，以应用分量方式给定一个CDNN N，我们说两个输入x[0]和y[0]具有相同的标签，如果（x[0]）=（y[0]）。具有相同标签的这种性质也可以从离散输入推广到输入区域。更具体地，如果从Θ i中选择的两个任意输入x[0]和y[0]具有相同的标签，则我们说（x[0]）=类似于[16]中的描述，给定输入区域具有相同标签的这种性质被称为鲁棒性。在这种情况下，在指定的输入区域Θ上描述给定CDNN N的鲁棒性规范。我们从健壮性的通用定义开始。（）T将向量x表示为（x） ：（x1），· · · ，n（xn）. 由于定义2（稳健性）一分类深度sigmoid函数的一个性质：对于给定的输入x[0]∈Rs0，函数fk的输入和输出为R→I，可以限制为x[k]=f k（x[k−1]）∈Isk，1 ≤ k ≤ n.神经网络N与输入区域Θ，鲁棒性当且仅当输入区域Θ内的所有输入具有相同的标签时，x[0]，y[0]∈θ=（五）111421也就是说，如果存在一个指数n，1≤n≤ sn，使得（x[0]）=对于每个输出x[n]都满足。换句话说，N与Θ是鲁棒的，当且仅当min{min{x[n]−x[n]，=}}>0。（九）满足，我们说N关于θ是鲁棒的。x[n]ℓℓ˜给定一个CDNNN，鲁棒性验证的问题是决定N相对于输入区域Θ是否为从（9）中，可以构造以下非线性优化问题，其目标是线性分段健壮。根据定义2，鲁棒性验证的目标是确定是否存在统一作用：p=min[k][k]{x[n]−x[n]，=}label（index）n，使得由s.t. ai≤x[0]≤bii=1，···，s0，从Θ中选择的输入满足z[k]我=W[k] x[k−1] + b[k]k=1，···，n，n（十）x[n]>x[n]对于所有的=。（七）x[k]= n（z[k]）k = 1，···，n.ℓℓ˜相反，如果存在两个输入x[0，y[0]∈θ使得argmax（f（x[0]））argmax（f（y[0]））是满意的。 此后我们将始终考虑输入区域Θ是笛卡尔积，即Θ = 101×···× 100 s0，其中101i=[ai，bi]是以ai，bi∈R为界的闭区间，对所有1≤i≤ s0。3. 分类深度神经网络在这项工作中，我们提出了一种直接的方法来攻击-ING鲁棒性验证问题，而不是计算输出集的过度近似给定一个具有输入区域的CDNN，我们建立了一个等价于原始鲁棒性验证问题的非线性优化问题。也就是说，鲁棒性验证的充分必要条件是检查输入区域中的最可疑点是否鲁棒。(see第3.1节）。为了减轻实际CDNN的计算困难性，给出了一个代理来将导出的非线性优化放松为线性规划问题（见第3.2节）。此外，松弛LP问题的最优解的正性足以保证给定网络的鲁棒性（见3.3节）。3.1. 从鲁棒性验证到非线性优化给定一个具有输入区域Θ的CDNNN：L，X，W，B，Φ，回想一下，鲁棒性满足是为了验证是否存在相同的标签，使得每个输出都满足条件（7）。结果，通过检查任意输出，即，其中x[0]是从Θ中选择的随机输入。根据标签的不同，通过检查条件（7）进行的稳健性验证等同于验证min{x[n]−x[n]，=}>0（8）下面的定理说明了等价变换鲁棒性验证和非线性优化求解之间的关系。定理1设N是一个分类深度神经网络，Θ是给定的输入区域。假设y[0]是从Θ中随机选择的，并且θ是由N与y[0]分类的标签，即，=假设p是优化问题（10）的最优值，由N、Θ和θ确定。则N关于Θ是鲁棒的当且仅当pθ> 0。证明1观察优化问题（10）的约束是N的等价表达式：x[n]=f（x[0]）。因此，取（7）和（9）之间的等价性产生期望的结果。Q实际上，优化问题（10）试图找到输入区域中最有可能不鲁棒如果最差点是鲁棒的，那么所有其他点也应该是鲁棒的。3.2. 深度神经网络该小节考虑如何根据线性约束对CDNN中的行为进行编码，以便高度可扩展的LP求解器可以有助于验证实际大小的CDNN编码基于网络中每个神经元的输入-输出行为，主要挑战是处理由激活函数引起的非线性。为了促进这种线性松弛，我们首先通过逐层估计计算所有神经元的下限和上限，然后在产生的界限内线性区间分析的有界导数不失一般性，我们考虑单层L[k]。如第2节所示，已知L[k]中的神经元x[k]的值可以通过下式计算：x[k]=n（W[k]x[k−1]+b[k]），（11）其中，逐元素地应用了k。通过引入辅助变量z[k]，可以将评估（11）重写为线性映射z[k]=W[k]x[k−1]+ b[k]，（12）ℓℓ˜511422∪我RkJk=1一个非线性映射x[k]= n（z[k]）。（十三）令D[0]= Θ是表示输入神经元的边界的区间向量，并且令D[k]，1≤k≤n是表示第k层神经元的边界的区间向量所有神经元的界都可以通过每个-使用（12）和（17），我们提供了一种对层L[k]的输入-输出行为进行线性编码的方法。因此，对网络N进行编码的线性约束的集合可以被定义为：C=nCk。 在这种情况下，从上述线性编码可以得出，用于鲁棒性验证的等效优化问题（10）可以放松为以下优化问题：形成逐层分析的程序。更多信息[n][n] ˜具体地说，假设D[k-1]是由先前的pr= minx[k]，z[k]{x−x，=}层，使用间隔计算（12）产生范围S.T.X[k] ∈D[k]ℓ，k= 0，· · ·，nz[k]，记为[α，β对于每个j= l，· · ·，s. S-z[k]=W[k]x[k−1]+b[k]，k=1，···，n，（十八）jk、jk、jk[k][k][k]由于k是单调递增函数，所以第i个元素x−p（z）−rk≥0，k= 1，· · ·，nx[k]的项可由<$（αk，i）≤x[k]≤<$（βk，i）有界。x[k]−p[k]（z[k]）−rk≤ 0，k= 1，· · ·，n.因此，我们有x[k]<$D[k]，其中D[k]是以下区间向量D[k]=[k（αk，1），k（βk，1）]×···×[k（αk，s），k（βk，s）]。注1与优化问题（10）相比，（18）的可行集是（10）的超集，这导致（18）的最优解是k k线性包含让我们解释如何计算线性包含的激活函数y=x（x）内的domain[a，b]。让我们首先选择区间[a，b]的中点，并且对x（x）的泰勒展开在点处产生线性近似，n（x）=p（x）+r（x），（10）的最佳值，即，pr≤p。3.3. 线性规划的转换优化问题（18）的目标函数是分段线性的。为了使其适用于LP求解器，通过引入辅助变量t将其转换为等效的优化问题：其中p（x）=（）+′（）（x−）是（x）在点的线性近似，r（x）是误差函数。由前-p=最大t[n][n]S.T.x −x≥t，，探索区间评价[23]，我们可以得到包含，用[r，r]表示，表示计算的r（x）的范围x[i]∈ℓD[k]，k= 0，· · ·，n（十九）在域[a，b]。z[k]=W[k]x[k−1]+b[k]，k=1，···，n··总结一下 称为LI的过程，x[k] -p[k]（z[k]）−r≥0，k= 1，· · ·，n用线性近似的边界推导，是适用的x[k]−p[k]（z[k]）−rk ≤0，k=1，···，n到激活函数的线性包含，即，设p和p是最优化的最优解，R rLI：n（a）≤ n（x）≤ n（b），p（x）+r≤ n（x）≤ p（x）+r. （ 十四）问题（18）和（19）。因为p=min{x[n]-r[k]x[n]}，且x[n]−x[n]≥p，对于所有的n=n，我们有p≥p。如上所述，假设zj的范围是[αk，j，βk，j]由前一层r产生。 F或每个另一方面，pr是满足以下条件的最大值[k][k]约束集合{x[n]−x[n]≥t，则p≥p。1≤j≤s k调用LI过程到xj=（zj ），产量ℓℓ˜∗ ∗r r相关的线性不等式：n（αk，j）≤x[k]≤n（βk，j），（15）结合这两个因素，得出pr=pr。上述转换之间的一个充分的条件是鲁棒性，p[k]（z[k]）+r≤x[k]≤p[k]（z[k]）+r.（十六）CDNN的定义j jk，jj jjk、j通过对向量x[k]逐分量地调用LI过程，非线性约束（13）可以被放松为以下线性约束nx[k]∈D[k]，定理2给定一个CDNNN：N，L，X，W，B，Φn，输入区域为Θ。假设（19）是如上所述建立的线性规划问题，并且p是（19）的最优值。如果p>0，则N是鲁棒的。511423RRKKCk：x[k]−p[k]（z[k]）−r[k]≥0，x[k]−p[k]（z[k]）−r[k]≤0，（十七）证明2对于具有输入区域Θ的给定N，可以建立优化问题（10）。由于（18）和（19）之间的等价性，并结合Re-1，其中p[k]（z[k]）=[1]（z[k]-z[k]），其中p是（10）的最优值的下界。德-[k]是z[k]范围的中点向量，r[k]=英博>0，则（10）的最优解为正。（rk，1，· · ·，rk，s ）T，并且r[k]=（rk，1，· · ·，rk，s）T。最后，从定理1得出N是鲁棒的。Q611424∗∗定理2保证当p∈ 0时，N对θ是鲁棒的。bRobust为真，则具有Θ的N为鲁棒的（第14行），并且如果bUnrobust为真，则具有Θ的N是不鲁棒的，因为t-考虑pr<= 0的情况，并且对应的最坏点是x[0]，需要使用N来验证x[0]，表示为作为（x[0]）。 如果n（x<$[0]）n=n，即x<$[0]被错误分类，则x<$[0]提供了一个反例来表明N不是鲁棒的。但如果n（xn[0]）=n，则N的鲁棒性保持不确定，因为我们不能预测其他坏点是否鲁棒。为了验证给定网络N的鲁棒性，我们建立了一个松弛线性规划问题（19），可以使用传统算法（如邻域点法[4]）求解。此外，（19）的最优值的正性足以验证N.算法1中总结了详细程序。算法一：RobustVerifier（CDNN的鲁棒性验证）输入： 输入区域Θ。输出：bRobust; bUnrobust。1bRobust<$; bUnrobust <$;2 确定标签编号：3从Θ中选择随机元素x[0]，即，x[0]∈Θ;[0] int n = nums（n）;5D[0]←Θ;6 C← {};对于k= 1，78D[k]是由D[k-1]通过边界推导计算出来的;9Ck←LinearEncoding（N，D[k]）;10C←C<$Ck;11 构造如（19）中的线性规划问题;12调用LP求解器以获得最优pr及其优化器：（x<$[k]，z<$[k]）;13如果pr>0，则14bRobust← TRUE;其他1516如果（x[0]）=，则17bUnrobust← TRUE;RobustVerifier将具有输入区域Θ的CDNN N作为输入。在行1中，定义了两个布尔标志，即，bRo- bust和bUnrobust。该过程首先通过执行从Θ中选择的元素来确定N的标号，然后对线性约束的集合进行迭代（第5行和第6行）。第7行到第10行获得近似激活函数的线性约束。第11行构造了相应的线性规划，并且可以通过调用LP求解器（第12行）来找到它的解。RobustVerifier返回以下结果之一：如果输入x[0]和x[0]具有不同的标签。否则RobustVerifier无法确定N是否稳健。注2设D[n]是通过边界推导（第8行）获得的输出层Ln的范围，表示为D[n]=[l1，u1]×···[lsn，usn]。一旦l>u为each也就是说，具有输入区域Θ的N具有相同的标记θ。在在这种情况下，Robustverifier结束并且bRobust被设置为TRUE。因此，这种用于计算输出层的下限和上限的简单方法（称为RobustLU）也可以用于验证N与Θ的鲁棒性。4. 评价在评估中，我们使用从三个流行的图像数据集生成的图像分类网络设计的图像分类，作为目标CDNN的鲁棒性验证。这些图像分类网络包括训练用于分类数据库MNIST [20]中数字0-9的10类手写图像、数据库（GTSRB）[30]中43类德国交通标志的网络。和来自加州理工学院101数据集的101类图像[21] .所有图像分类网络都是从神经网络库Keras [7]构建的，其后端是深度学习包Tensorflow [1]。三个数据集的详细信息如下：• 经修改的国家标准和技术研究所。MNIST数据库是为训练各种图像处理系统而设计的手写图像的大型集合，其中每个图像的大小为28×28，并且是黑白的。它有60，000个训练输入图像，属于10个标签之一即从数字0到数字9。• 德国交通标志识别基准。GTSRB是一个大型的交通标志图像集，设计用于单图像，多类分类问题。它由超过50，000个交通标志图像组成，属于43个不同的类别。在GTSRB中，每个图像的大小为32×32，有三个通道（红色，绿色和蓝色）。• 加州理工101号数据集Caltech-101数据集由属于101个不同类别的图像组成，每个类别中的图像数量从40到800不等。大多数图像的分辨率为300×200像素，有三个通道。在[24]中，NEVER工具被提出来验证一种特殊类型的具有S形激活函数的神经网络，称为多层感知器（MLP）。MLP是CDNN的退化，因为它仅将激活函数限制为611425位于输出神经元上。我们推广了算法来处理CDNN，称为Generalized-NEVER（GNEV-ER）。我 们 已 经 实 现 了 所 提 出 的 算 法 Ro-bustVerifier ，RobustLU （ 见 注 释 2 ） 和 Generalized- NEVER 作 为MATLAB程序。由鲁棒验证产生的LP问题由LP求解器linprog求解。通过在具有3.2GHz Intel（R）Xeon Gold6146处理器和128 GB RAM的Ubuntu 18.04 LTS计算机上运行它们获得了以下实验结果。4.1. 性能在本节中，我们通过不同的扰动和网络结构来评估这三种工具的性能。从MNIST数据集训练的CDNN用于性能评估，其输入层由784个神经元组成，输出层由10个神经元组成。对于MNIST中的每个图像，指定具有这些像素的可能扰动范围的像素集合，其形成输入层的输入区域Θ给定CDNN N和输入区域Θ，鲁棒性验证需要检查鲁棒性属性是否关于Θ成立，即，将输入区域Θ内的所有输入分配给相同的标签。图1显示了输入区域的配置：一组扰动（扰动半径为0。5）到每个图像左上角的大小为5×5图1.MNIST CDNN相对于.扰动图像。表1列出了三种工具Ro-bustVerifier 、RobustLU和GNEVER在不同扰动下的比较结果这里，输入区域是图像左上角的大小为5×5的块;表示扰动半径，即，θ=0。2意味着扰动随-在[-0]范围内变化。2，0。2）被强加在原始图像上;r1、r2和r3分别记录了工具Ro-bustVerifier 、 RobustLU 和 GNEVER 的 识 别 率 。 在 这里，识别率被定义为将特定工具报告的鲁棒图像加上对抗性示例的数量除以正在验证的图像的总数。从表1可以看出，在所有情况下，在所有情况下，工具RobustVerifier的性能优于其他两个工具，而工具RobustLU的性能优于工具GNEVER。例如，考虑k = 0的情况。2、三种工具的正确识别率分别为表1.不同扰动下的性能ϵR1R2R30.1095.94%92.56%90.39%0.1592.16%84.57%82.00%0.2087.90%83.88%64.65%0.2579.43%67.74%65.78%0.3070.56%65.32%45.74%在10,000次检测中，阳性率分别为87.90%、83.88%和64.65%。当k增长到0时。3、正确识别率分别降至70.56%、65.32%和45.74%。性能结果符合我们讨论的近似精度降序。对于同一个工具，在同一列中看到的结果，当扰动变大时，验证工具的性能下降，因为扰动的增加加速了近似误差的积累。表2列出了不同网络结构的比较结果。这里，输入区域被定义为左上角的一个5×5块，扰动半径固定为0.20;n表示CDNN的层数，在每个隐层中，神经元的数量sk随40≤sk≤100而变化。表2.在不同网络结构上的性能nR1R2R3587.90%83.88%64.65%672.33%51.84%50.24%761.33%43.11%29.07%850.58%百分之二十九点零二27.79%945.90%33.28%31.63%1034.65%百分之十四点一九12.40%表2显示了工具RobustVerifier在所有情况下的性能最好，并且RobustLU的性能优于GnVER。随着隐层的增加，逐行检查验证结果，验证工具的性能下降。逼近误差逐层累积是导致性能下降的主要采用的紧密近似技术有助于我们的工具受到较少的影响。4.2. 精度与性能在本小节中，我们评估了具有较大CDNN的三种工具，并研究了精度如何影响验证实际CDNN的性能。对于GTSRB生成的CDNN，我们将输入区域指定为每个图像中心的3×3块，扰动半径为0。05在RGB（红绿蓝）通道之一。对于输入区域的这种配置，工具Ro-bustVerifier可以验证扰动图像与其原始图像属于同一类，而其他两个不能。611426图4.训练的CDNN是鲁棒的w.r.t.扰动图像。图2.GTSRB CDNN相对于.扰动图像。图3. GTSRB CDNN的对抗性示例。图2显示了4对配置的原始图像和扰动图像，这些图像已被验证为鲁棒的。然后通过增大扰动半径或扰动块的大小不幸的是，这两种工具都不能验证扰动图像在这些配置下是鲁棒的。对于输入区域，在中心放置一个3×3的块，扰动半径为0。1在RGB通道之一上，我们的工具可以返回许多与扰动图像的错误分类相对应的对抗性示例。图3给出了一些对抗性的例子，其中输入区域设置为干扰半径λ=0。在一个通道上的1个连接到3×3尺寸的中心块。与MNIST数据库相比，GTSRB的CDNN必须识别更多的类，43比10。 因此，它对与生俱来的扰动更敏感。当遇到这种CDNN时，无法提供足够精度的验证方法不起作用。我们还进行了实验的CDNN从加州理工学院101数据集。训练的CDNN不少于180，000个神经元，而输入区域被设置为图像中心的大小为40×40的块，扰动半径为0。五、图4中显示了几对原始图像和扰动图像。图5列出了性能与网络结构的对比结果这里，X轴表示CDNN的层数，而Y轴记录成功验证的速率。对于每种网络结构，选择10种不同的神经元数目配置进行实验，其中每个隐层的神经元数目为[150][150][150][150][151]][152][153][154] 十 次 实 验 的平均成功验证率如图所示。对于工具GEVER，其性能在23%和81%之间变化。随着隐层数的增加，它的近似值引入的误差会迅速逐层传播，从而使它急剧下降。对于所有的实验，我们的工具RobustVerifier可以给出准确的结果，超过82%的干扰图像。请注意，验证结果不仅取决于具体的验证方法，还取决于被验证的CDNN的质量。7层或8层的CDNN似乎不如其他的好。在这个实验中，我们的工具RobustVerifier表现最好，并显示了它的能力，处理真正的CDNN。图5.加州理工学院101的性能与网络结构5. 结论我们提出了一种新的方法，用于使用sigmoid激活函数攻击分类深度神经网络的鲁棒性验证。为了使其易于操作，我们首先将验证问题转化为一个等价的非线性优化问题，然后通过求解非线性激活函数的线性松弛产生的线性规划问题来进行。我们基于LP的方法已经在RobustVerifier工具中实现，并在几个最先进的CDNN上进行了真实图像的验证。性能结果突显了该方法在提供关于显著规模的CDNN的鲁棒性的正式保证方面的潜力611427引用[1] Mart 'ın Abadi，Paul Barham，Jianmin Chen，ZhifengChen ， Andy Davis ， Jeffrey Dean ， Matthieu Devin ，Sanjay Ghe- mawat，Geoffrey Irving，Michael Isard ，Manjunath Kudlur ， Josh Levenberg ， Rajat Monga ，Sherry Moore，Derek Gor- don Murray，Benoit Steiner，Paul A. Tucker ， Vijay Vasude-van ， Pete Warden ，Martin Wicke ， Yuan Yu ， and Xiaoqiang Zheng.Tensorflow：一个大规模机器学习系统在第12届USENIX操作系统设计与实现研讨会（OSDI）中，第265[2] OsbertBastani，YaniIoannou，LeonidasLampropoulos，Dimitrios Vytiniotis，Aditya V.诺丽，还有安东尼奥·克里明·伊斯.带约束的神经网络鲁棒性度量。在2016年第29届神经信息处理系统（NIPS）集，第2613[3] 巴蒂斯塔·比吉奥、伊基诺·科罗纳、达维德·马约卡、布莱恩·尼尔森、内迪姆·斯恩迪奇、帕维尔·拉斯科夫、乔治·贾钦托和法比奥·罗利。在测试时对机器学习的规避攻击。在2013年欧洲机器学习和数据库知识发现会议论文集，第387-402页[4] 斯蒂芬·博伊德和利文·范登伯格。凸优化。剑桥大学出版社，2004年。[5] 放大图片作者：John H. S. Torr、Pushmeet Kohli和M.帕万·库马尔分段线性神经网络验证：比较研究。CoRR，ab- s/1711.00455，2017年。[6] Nicholas Carlini和David A.瓦格纳。对神经网络鲁棒性的评价。在IEEE安全和隐私研讨会论文集，第39[7] 弗朗索瓦·肖莱。K时代 https://keras.io。，2015年。[8] 丹·C Ciresan，UeliMeie r，andJürgenSchmidhube r. 用于图像 分 类 的 多 在 IEEE 计 算 机 视 觉 和 模 式 识 别 会 议（CVPR）的会议记录中，第3642-3649页[9] SouradeepDutta，SusmitJha，SriramSanakaranarayanan，and Ashish Tiwari.深度前馈神经网络的输出范围分析。在美国宇航局形式方法（NFM）第10届国际研讨会论文集，第121-138页[10] 鲁迪格·埃勒斯。分段线性前馈神经网络的正规化在第15届自动化技术验证和分析国际研讨会（ATVA）的会议中，第269-286页[11] Alhussein Fawzi、Omar Fawzi和Pascal Frossard。分类器对 对 抗 扰 动 的 鲁 棒 性 分 析 Machine Learning ， 107（3）：481[12] 泽维尔·格洛罗特安托万·博德斯和约舒亚·本吉奥。深度解析整流神经网络。在第14届人工智能和统计学国际会议（AISTATS）的会议记录中，第315-323页[13] Ian Goodfellow Yoshua Bengio和Aaron Courville深度学习麻省理工学院出版社，2016.[14] Kun Han，Dong Yu，Ivan Tashev.使用深度神经网络和极端学习算法的语音情感中国。在国际语音通信协会（INTER-SPEECH）第15届年会的会议记录中，第223-227页[15] G.欣顿湖Deng，D. Yu，G. E. Dahl，A. R. Mohamed，N.Jaitly，A. Senior，V. Vanhoucke，P.阮氏T. N. Sainath和B.金斯伯里语音识别声学建模的深度神经网络：四个研究小组的共同观点IEEE Signal Processing Magazine，29（6）：82-97，2012。[16] Xiaowei Huang，Marta Kwiatkowska，Sen Wang，andMin Wu.深度神经网络的安全性验证。在第29届计算机辅助验证（CAV）国际会议的开幕式上，2017年3-29页[17] 作者：Guy Katz作者：David L. Dill，Kyle Julian，andMykel J. Kochenderfer Reluplex：一个用于验证深度神经网络的高效SMT求解器。在第29届计算机辅助验证国际会议（CAV）中，第97-117页[18] Alex Krizhevsky、Ilya Sutskever和Geoffrey E.辛顿使用深度卷积神经网络的图像网分类。在2012年第26届神经信息处理系统（NIPS）集，第1106[19] 泽尚·库尔德和蒂姆·凯利。建立人工神经网络的安全标准。在Proceedings of the 7th International Conference onKnowledge-BasedandIntelligentInformationandEngineering Systems（KES），第163-169页[20] Yann LeCun、Corinna Cortes和Christopher J.C.伯吉斯mnist手写数字数据库。http://yann.lecun.com/exdb/mnist