摘要
改进了DeepTRE的实现,在保留DeepTRE验证能力的前提下大幅降低了DeepTRE的空间复杂度,以适应大规模数据集场景。在高铁运行环境识别场景中评估了改进后的DeepTRE,并与其他主流验证工具DLV和SafeCV对比。实验结果表明,改进后的DeepTRE工具的显存占用显著低于原DeepTRE工具,相较于其他神经网络验证工具,改进后的DeepTRE工具在具有较快验证速度的前提下拥有更优异的验证效果。
人工智能(artificial intelligence,AI
目前神经网络处理效果评估主要依靠神经网络在测试集上的精度,然而测试集的数据与训练集、验证集的数据往往属于独立同分布,即测试集中并不包含被干扰过的图像,这使得大部分在测试集上表现良好的神经网络模型在面对异常样本时表现很差。将这些异常样本加入测试集重新训练神经网络来提高其鲁棒性是一个可行的办法,但是类型多变的异常样本导致新的异常样本不断产生,将新的异常样本不断加入测试集,从而引起测试准确度的不稳定,因此研究人员更多地考虑验证而非测试的方法来评估神经网络的鲁棒
系统安全性验证通常采用基于严格的数学模型的形式化方
2019年,Ruan
以高铁运行环境识别网络为背景,采用DeepTRE验证网络的鲁棒性。在使用DeepTRE验证网络的过程中,由于内存不足而导致验证中断,因此对DeepTRE实现进行了一些改进,包括由局部鲁棒性计算改为全局鲁棒性计算、允许任意设置扰动值、设定验证范围、多轮预测以减少空间复杂度4个方面。最后,基于改进的DeepTRE对识别任务进行验证实验,并与其他神经网络验证工具DLV和SafeCV进行对比。
给定一个用于分类的神经网络,对于一个输入,输出,其中表示第个标签的置信度。不失一般性,将输入归一化为,输出使用Softmax层归一化为。用表示输入为时对应的输出的分类标签。
定义1 (全局鲁棒性) 给定神经网络一个有限的原始输入集和距离范数,对于所有原始输入集,原始输入集中的图像在添加扰动后得到对抗样本数据集。全局鲁棒性计算是一个优化问题,即计算与之间的最小距离,如下所示:
(1) |
DeepTRE中使用距离范数衡量图像之间的距离,并定义输入图像数据集之间的距离是数据集中所有相应图像之间距离的期望,计算式如下所示: | (2) |
定义2 (子空间完备集) 给定一个输入和一组维度为的正整数集合,。定义的子空间为一组输入的集合,对于任意有,对于有。输入的子空间完备集为。
中的每个元素与相比除中指定的像素外的值都相等,即子空间中的每个元素都是改变了中指定的像素、其他的像素保持不变之后得到的图像。由于在维的情况下有多种组合,因此是在所有可能的下的集合。
定义3 (子空间敏感度) 给定输入子空间,输入,输出标签,关于的子空间定义如下所示:
(3) |
引入测试集和维度后,子空间敏感度定义如下所示:
(4) |
神经网络对输入的输出分类标签记为。直观上来看,表示集合中所有修改后的图像与原图像相比分到类别置信度的最大下降值,表示所有的子空间和中所有输入的分类标签置信度的最大下降值的二维数组。
DeepTRE主要包含敏感度矩阵计算和鲁棒性上下界计算两部分。一般来说,在攻击方法中生成对抗样本时计算得到的最小扰动是鲁棒性的上界,而保证一定不会产生对抗样本的最小扰动是鲁棒性的下
假设输入数据集中图像像素大小为(为图像宽度,为图像高度)、类别数量为,对每个像素添加扰动的次数为。对扰动后得到的张量进行模展开(mode-1 unfolding),得到的矩阵由个元组组成,每个元组包含2个子元组,一个是第次只改变个像素后的图像,,即子空间完备集,另一个是原图像和扰动后图像在Softmax层输入中的个类别差值。将得到的矩阵按第2个子元组原始类别的差值从大到小排序,即按照相应像素改变对正确类别影响从大到小排序,得到敏感度矩阵。敏感度矩阵实际表示的物理意义是同时改变个像素的组合对神经网络输出正确类别概率的影响。
对于鲁棒性下界的计算,只需要检测张量第3维第1行的图像是否会发生类别变化,即检测是否有。如果没有,鲁棒性下界就是,反之说明改动个像素足以引起图像类别发生改变,那么此时鲁棒性下界就是。
对于上界的计算比较复杂,包含了累加和剔除2个部分。在累加部分,对于中的每个输入图像,根据敏感度矩阵从上到下的顺序,从原图像开始迭代,采用敏感度矩阵中的扰动,直到图像类别发生变化,此时生成的图像一定是一张对抗样本。剔除部分是在这张对抗样本基础上进行的,每次恢复敏感度矩阵中一行的个像素的值,如果剔除了这个像素后的对抗样本仍然分类错误,就说明这个像素不会对分类结果产生影响,这个像素仍然保持恢复后的原值,否则撤销这一步的剔除。如此,将敏感度矩阵中的个元组剔除一次后得到的更改像素个数就是鲁棒性的上界。
首先,Ruan
其次,DeepTRE在进行鲁棒性评估时,并没有设定验证范围,这不符合实际情况。根据对抗样本的定义,生成的对抗样本与原始图像之间的距离需要限制在一定范围内,这个距离限制保证了对抗样本与原始图像的相似性,将这个范围称为验证范围,即在验证范围内用人眼看对抗样本与原始图像应该属于同一类别,超过验证范围后人眼可轻易区分对抗样本与原始图像,不会将两者划分到同一类别。DeepTRE只强调找到一个扰动的上界,当扰动超过上界时一定能够找到对抗样本。然而,当上界超过验证范围时,该上界值也就没有了意义,因此引入验证范围的概念。
最后,分析原始算法的空间复杂度。假设测试集中共有张图像属于个类别,每个像素的扰动次数为,每张图像的像素大小为,其中为图像通道数。DeepTRE在算法实现中有3个较大的矩阵:第1个矩阵是存储测试集图像地址的矩阵,由于DeepTRE将测试集中所有图像的地址存储在一个矩阵中,并依次在每张图像上计算神经网络的局部鲁棒性,因此矩阵的空间度复杂度为;第2个矩阵是输入给神经网络的张量,由个元组组成,每个元组保存添加扰动后图像的像素值,大小为,对每个被保存的扰动后图像,有个像素的值与原图像相同,一个像素的值因添加扰动而不同,每个像素被添加次扰动,因此矩阵的空间复杂度为;第3个矩阵是神经网络输出的敏感度矩阵,由个元组组成,每个元组保存Softmax层在个类别的输出,矩阵的空间复杂度为。因此,总空间复杂度为。一般而言,测试集中图像数量和类别数量不会过大,因此算法的总空间复杂度为。以ImageNet数据集为例,每张图像的像素大小为,默认扰动次数,空间复杂度为。可以看出,当数据集规模变大时,算法的空间复杂度急剧增加,使得验证无法进行。
基于上述原因,对DeepTRE进行改进,使其支持大规模图像验证,具体的改进内容包括由局部鲁棒性计算改为全局鲁棒性计算、允许任意设置扰动值、设定验证范围、多轮预测以减少空间复杂度4个方面,接下来对改进过程进行详细介绍。
使用变量表示验证范围。由于DeepTRE是基于距离,因此直观上表示的是改变的最大像素数。当改变像素的个数小于的下界时,认为生成的对抗样本与原样本应该属于同一个类别;当改变像素的个数大于的上界时,认为添加的扰动过大,用人眼看来生成的样本与原样本类别不同。改进后的DeepTRE算法如

图1 改进后的DeepTRE算法
Fig.1 Improved DeepTRE algorithm
敏感度特征图计算算法GetFeatureMap如

图2 子空间敏感度计算方法
Fig.2 Subspace sensitivity calculation algorithm
改进后的Accumulate算法伪代码如

图3 改进后的Accumulate算法
Fig.3 Improved Accumulate algorithm
根据敏感度特征图计算算法,敏感度矩阵中的扰动次数为,即对原始图像中的每个像素都扰动一次。若累加过程中对所有扰动都进行尝试,算法的空间复杂度则高达。原累加过程增加了叠加扰动的范围以限制累加扰动的数量。用户可以自由设置的值,如果扰动像素数超过,累加就终止,所以原累加算法的空间复杂度为。当设置过小时,原算法可能忽略存在的对抗样本;当设置过大时,原算法的空间复杂度仍然很大。
在新的Accumulate算法中取消范围限制,规定每当矩阵中累加的扰动数量为图像的宽时,检测一次是否找到对抗样本,如果找到就返回及找到的对抗样本,否则清空矩阵中的值并在之前扰动后的图像基础上继续添加扰动。改进后Accumulate算法空间复杂度为。
改进后DeepTRE的空间复杂度主要取决于新的敏感度矩阵计算算法,与原敏感度矩阵计算算法相比,改进后算法包含2个较大的矩阵,第1个为神经网络输入矩阵,第2个为Softmax层的输出矩阵。
对于第1个矩阵,假设测试集中共有张图像属于个类别,用扰动代替原算法中的扰动次数,这样可以在验证开始前任意设置扰动大小,而不需要在扰动时动态计算。每张图像的像素大小为。对扰动后的图像分批处理,每批都有个图像,因此输入给神经网络的张量大小为。为方便实现,对于大型图像数据集,可以设置。时间换空间的策略能有效降低空间复杂度,达到两者的平衡,此时空间复杂度为。
对于第2个矩阵,不像原方法将个类别在Softmax层的输出全部保存,由于只关注是否生成对抗样本,而不关注生成对抗样本的具体类别,因此对于原始图像生成的扰动后图像,只需保存第类别Softmax层的输出即可,这部分的空间复杂度为。
因此,通过多轮预测优化,改进后DeepTRE的空间复杂度为。
对于DeepTRE,目前有严格的理论证明过程,但该方法只应用于少数公共数据集。在本节中,基于文献[
实验是在使用Tesla K40c的GPU 上进行的,验证范围,扰动。采用包括6 000张图片的测试集对模型进行鲁棒性评估,改进后的DeepTRE对每张图像的平均搜索时间为10 min。实验后一共生成了1 792个对抗样本,每个类别分别有199、98、0、532、411、552个,攻击成功率为 0.298 7。

图4 改进后DeepTRE生成的对抗样本示例
Fig.4 Adversarial examples generated by improved DeepTRE
实验结果表明,改进后DeepTRE的攻击效果良好。直观上看,攻击“白天有雨”类别的效果不好,没有生成一张对抗样本,在其余5个类别中攻击效果均较好,在“夜间晴天”类别生成的对抗样本数量最多,与原样本的距离也最小。对于第7组和第9组图像而言,DeepTRE添加的扰动肉眼几乎不可分辨。对于“白天晴天”而言,部分图像添加的扰动个数很少(第7组),部分图像添加扰动个数却很多(第6组),但扰动像素个数与图像类别没有确定的关系。
已知DeepTRE全局鲁棒性上界是测试集上所有对抗样本与原图像之间距离的期望,为1 037 572/1 792=579(数据集中的扰动像素总数为1 037 572,有1 792个对抗样本)。通过实验给出了训练好的模型的鲁棒性上界为579。
在空间复杂度方面,改进前的DeepTRE由于空间复杂度过高导致显存溢出而无法进行实验,因此在理论上讨论改进前后DeepTRE空间复杂度的差异。为了减少复杂度,只考虑维的情况。数据集中每张图像的像素大小为224224,一共6个类别,在添加扰动得到敏感度矩阵后分224次输入到神经网络中进行预测,那么算法的复杂度为2242242243=33 718 272。原DeepTRE空间复杂度为22422422242243=15 105 785 856,是改进后DeepTRE的448倍,改进后的DeepTRE以时间换空间的方法减少了中间矩阵的大小,使得能够支持更大图像像素和数量的数据集。
采用2种神经网络验证方法DLV(deep learning verification)和SafeCV(safe computer vision)在同一识别案例中进行实验,并将验证结果与改进后DeepTRE进行对比。DLV通过离散化处理输入层或隐藏层的向量空间,然后在离散化空间上应用穷举搜索算法寻找对抗样本,从而验证神经网络的鲁棒性。SafeCV将对抗样本的搜索过程转化为双人回合制随机博弈,并通过蒙特卡罗树搜索逐步搜索博弈状态空间来寻找对抗样本。
DLV在使用过程中有2个问题。第一,DLV确保找到对抗样本是基于离散化方式对验证范围进行了穷举搜索,但增加了算法的时间复杂度;第二,将神经网络模型集成到DLV上时,需要给定的用户参数个数多达15个,因此影响对抗样本的寻找速度及寻找结果。对于第2个问题,采取多次实验的方法,尝试采用不同的参数值以丰富对抗样本的寻找结果。最终得到的重要参数值(节选)如下:numOfFeatures=10 000(表示验证网络每一层时考虑的特征数量),featureDims=5(每个像素的维度数量),controlledSearc=("",40)(使用范数度量扰动,扰动的范数小于40)。
相比之下,改进后的DeepTRE涉及的参数只有2个,对用户十分友好,同时验证速度也快于DLV。SafeCV的验证更快,远远快于DLV,略快于改进后的DeepTRE。
针对改进后的DeepTRE,DLV和SafeCV的实验结果中挑选6组进行对比,如

图5 原始图像和改进后DeepTRE、DLV、SafeCV生成的对抗样本
Fig. 5 Original images and adversarial examples generated by improved DeepTRE, DLV and SafeCV
在维度t=1的情况下,改进后的DeepTRE得到基于的神经网络全局鲁棒性下界为1,上界为579,而DLV和SafeCV都是针对单个输入图像,如果在一定范围内能够找到对抗样本,神经网络就是不鲁棒的,如果没有对抗样本,神经网络就是鲁棒的,并没有给出全局的证明。DLV在小于40的区域内针对所有输入图像都找到了对抗样本,因此DLV得到基于的鲁棒性上界小于40,基于的鲁棒性上界小于;SafeCV的运行速度很快,采用蒙特卡罗树搜索返回最优结果,尽管得到了最优结果,但是除“夜间晴天”类别中的个别输入图像外,大部分图像改动的像素个数都是上万,从视觉上认为生成的对抗样本改动过大,甚至人眼都可以将对抗样本与原始图像区分,因此SafeCV方法在模型和数据集上的验证效果较差,得出的鲁棒性上界也过大。
在验证效果方面,改进后的DeepTRE要显著强于DLV和SafeCV,可以在更小的下生成对抗样本。从运行时间上看,改进后的DeepTRE明显快于DLV,但是略慢于SafeCV。
通过对DeepTRE进行优化降低了DeepTRE的空间复杂度以支持大规模图像数据集,改进内容包括由局部鲁棒性计算改为全局鲁棒性计算、允许自定义设置扰动值、设定验证范围、多轮预测以减少空间复杂度4个方面。最后,采用实验验证了改进后的DeepTRE的效果。结果表明,一方面改进后的DeepTRE显著降低了空间复杂度以支持更大规模的数据集,另一方面改进后的DeepTRE相较于DLV和SafeCV在较快的验证速度下拥有更优异的验证效果。
作者贡献声明
高 珍:论文审阅与修改,算法设计指导。
苏 宇:模型构建,算法设计与实现,论文撰写。
侯潇雪:模型构建,算法设计与实现,论文撰写。
方 沛:论文审阅与修订。
张苗苗:论文审阅与修订,算法改进指导。
参考文献
RUSSELL S J. Artificial intelligence: a modern approach[M]. New York: Pearson Education, Inc., 2010. [百度学术]
MITCHELL T M. Machine learning[M]. New York: McGraw-Hill Co. Ltd., 1997. [百度学术]
SESHIA S A, SADIGH D, SHANKAR SASTRY S. Towards verified artificial intelligence[J]. Communications of the ACM, 2016, 65(7): 46. [百度学术]
DIETTERICH T G, HORVITZ E J. Rise of concerns about AI: reflections and directions[J]. Communications of the ACM, 2015, 58(10): 38. [百度学术]
SZEGEDY C, ZAREMBA W, SUTSKEVER I, et al. Intriguing properties of neural networks[J/OL]. [2022-02-01]. https://arxiv.org/abs/1312.6199. [百度学术]
RUAN W, HUANG X, KWIATKOWSKA M. Reachability analysis of deep neural networks with provable guarantees[C]//IJCAI. Stockholm: IJCAI, 2018: 2651-2659. [百度学术]
CLARKE E M, WING J M. Formal methods: state of the art and future directions[J]. ACM Computing Surveys (CSUR), 1996, 28(4): 626. [百度学术]
WING J M. A specifier’s introduction to formal methods[J]. Computer, 1990, 23(9): 8. [百度学术]
KATZ G, BARRETT C, DILL D L, et al. Reluplex: an efficient SMT solver for verifying deep neural networks[C]//International Conference on Computer Aided Verification. Heidelberg: Springer, 2017: 97-117. [百度学术]
LOMUSCIO A, MAGANTI L. An approach to reachability analysis for feed-forward ReLU neural networks[J/OL]. [2022-02-01]. https://arxiv.org/abs/1706.07351. [百度学术]
DUTTA S, JHA S, SANKARANARAYANAN S, et al. Output range analysis for deep feedforward neural networks[C]//NASA Formal Methods Symposium. Heidelberg:Springer, 2018: 121-138. [百度学术]
HUANG X, KWIATKOWSKA M, WANG S, et al. Safety verification of deep neural networks[C]//International Conference on Computer Aided Verification. Heidelberg: Springer, 2017: 3-29. [百度学术]
WICKER M, HUANG X, KWIATKOWSKA M. Feature-guided black-box safety testing of deep neural networks[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer, 2018: 408-426. [百度学术]
MOOSAVI-DEZFOOLI S M, FAWZI A, FROSSARD P. DeepFool: a simple and accurate method to fool deep neural networks[C]//Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. Las Vegas: IEEE Computer Society, 2016: 2574-2582. [百度学术]
GEHR T, MIRMAN M, DRACHSLER-COHEN D, et al. AI2: safety and robustness certification of neural networks with abstract interpretation[C]//2018 IEEE Symposium on Security and Privacy (SP). San Francisco: IEEE, 2018: 3-18. [百度学术]
RUAN W, WU M, SUN Y, et al. Global robustness evaluation of deep neural networks with provable guarantees for the hamming distance[C]//IJCAI. Macao: IJCAI,2019: 5944-5952. [百度学术]
CARLINI N, WAGNER D. Towards evaluating the robustness of neural networks[C]//2017 IEEE Symposium on Security and Privacy (sp). San Jose: IEEE Computer Society, 2017: 39-57. [百度学术]
HOU X, AN J, ZHANG M, et al. High-speed rail operating environment recognition based on neural network and adversarial training[C]//2019 IEEE 31st International Conference on Tools with Artificial Intelligence (ICTAI). Portland: IEEE Computer Society, 2019: 840-847. [百度学术]