基于健壮半径求解的循环神经网络形式化验证方法

赵 亮, 戚润川, 段鑫民, 李春奕, 王小兵*

1西安电子科技大学计算机科学与技术学院 西安 中国 710071

1 引言

近年来, 人工智能引领科学技术的发展变革,也给人们的生活带来了天翻地覆的变化。其中受到广泛关注的神经网络领域涌现出很多表现出色的模型, 比如卷积神经网络[1]、循环神经网络[2-3]等。借助于这些神经网络模型以及各种优化学习技术, 可以对现实物理世界中高度抽象的关系进行近似。因此,它们在在图像识别、自然语言处理等一些输入输出关系过于复杂而难以精确建模的任务中取得了广泛的应用[4-6]。

虽然神经网络在诸多领域展示了其优异的性能,但其始终无法绝对精确地对无穷输入空间到输出空间的映射关系进行建模, 且模型自身仍然存在着健壮性差、行为不透明、可解释性差[7]等不可忽视的问题, 因此在实际应用中因神经网络系统的误判造成的事故屡见不鲜。例如, 2016年5月, 美国的一名司机在驾驶特斯拉Model-S的过程中, 开启了自动驾驶功能, 因识别系统的误判撞上了道路中央的半挂卡车, 当场死亡。同时学术界先后提出了基于梯度、基于迭代和基于生成对抗网络的攻击方法[8-10]。这些方法成功地对各种优秀的神经网络模型进行攻击,证明了即使在输入上施加极为微小的扰动, 也可能会导致神经网络误判, 在理论研究层面暴露了神经网络的脆弱性。

基于上述背景, 人们开展了对神经网络安全可信性的相关研究, 旨在判定或保障这一类系统的安全性, 并为此探索了多种技术。其中, 相比于传统的测试技术, 形式化验证技术可以为系统安全提供可靠与正确的保证。因此, 神经网络的形式化验证取得了广泛关注。目前的神经网络验证技术大致可分为两类: 精确求解方法[11-16]和近似求解方法[17-21]。精确求解方法主要是基于离散优化理论来形式化验证神经网络中某些属性对于任何可能的输入的可信性,即利用可满足性模理论(Satisfiability Modulo Theories, SMT)或混合整数线性规划(Mixed Integer Linear Programming, MILP)来解决此类形式验证问题。这类方法通常是通过利用ReLU的分段线性特性并在搜索可行解时尝试逐渐满足它们施加的约束来实现的。基于可满足性模理论的研究工作主要以Reluplex[11]为代表, 该工作通过扩展单纯形算法以支持ReLU约束, 并验证了激活函数为ReLU的前馈神经网络的健壮性。Lomuscio等人[13]提出的方法将神经网络编码成混合整数线性规划问题, 对线性规划中的浮点运算处理方式进行优化, 并采用了一种较为高效的线性规划求解方法, 相比于Reluplex中作为对比的线性规划方法效率大大提升。精确求解方法具有完备性, 能够返回一个确定性结果, 但这类方法具有很高的计算复杂度, 只适用于使用ReLU这样的分段线性激活函数的浅层小规模网络。

一些学者认为, 精确求解的方法将神经网络验证问题考虑得过于全面, 导致问题复杂度过高, 时间开销过大, 可以适当地将验证问题简化, 采用近似的方法进行求解[17-21]。这类方法对神经网络进行健壮性验证通常有一个一般性框架, 即在给定扰动类型与扰动范围的情况下, 通过将激活函数抽象为包含其凸包的线性约束区域, 可以逐层回溯迭代计算神经网络的近似区间, 并通过对输出层的近似区间进行分析来判断神经网络是否具有健壮性。同时为了量化健壮性, 在计算出输出层可达区间的基础上, 可以通过二分法得到一个扰动范围的健壮半径,确保在此半径范围内所有样本分类正确。这一类型的代表工作有Fast-Lin[19]、CROWN[20]和DeepPoly[21]。Fast-Lin[19]给出了一套通过线性近似来计算神经元近似区间的流程, 针对非线性激活函数ReLU采用平行近似方法。CROWN[20]在Fast-Lin的基础上对ReLU提出了效果更好的自适应近似, 同时增加了对ReLU以外的激活函数的支持。DeepPoly[21]是一种基于抽象解释的方法, 这种方法面向神经网络验证设计了一种专门的子多面体抽象域, 主要思想是为神经元维护一个具体值的区间、一个符号化约束上界与一个符号化约束下界, 并且针对仿射变换与最大池化操作分别设计了对应的抽象转换操作。近似求解不能保证在任何情况下都给出确定的验证结论,往往只能给出单边性的保障。然而, 相较于精确求解方法, 近似求解方法具有较低的时间复杂度, 适用于验证规模相对较大的网络。

现有的神经网络形式化验证的研究, 大多面向使用ReLU激活函数的全连接或卷积神经网络[22],关于循环神经网络验证的工作非常少[23-24]。而循环神经网络已被广泛应用于语音识别、自然语言处理、序列生成等多种现实场景, 其安全性的检验和保障具有重要的意义[25-27]。在此背景下, 本文旨在对循环神经网络的健壮性进行验证, 以改进目前该领域研究工作不足这一现状。然而, 循环神经网络的健壮性验证是一个复杂的问题。这类网络通常用来处理序列的建模, 网络层次较深, 且使用tanh等非分段线性激活函数。针对这一问题, 采用近似求解的方法更为适合。

本文提出了VR-RRS (Verification of RNN basedon Robustness Radius Solving), 一种基于健壮半径求解的循环神经网络形式化验证方法。首先, 该方法在经典近似求解框架上进行了改进, 引入细粒度的激活函数近似方式, 并将其应用于循环神经网络近似上下界的求解。其次, 分析细粒度激活函数近似方式的优势以及存在的问题, 并在此基础上设计了基于多路径回溯的近似区间求解方法, 使得循环神经网络各层的近似区间进一步精确。同时, 改进了传统近似求解框架的二分法求解过程。不同于传统方法中将输出层标签神经元的近似区间下界与其他神经元近似区间上界进行直接比较, 该方法直接计算标签神经元与其他神经元之差的近似区间。这种方式减小了因不等式放缩带来的对健壮性判定结果影响,从而提高求得的健壮半径, 即失真认证下界。本文在基于MNIST数据集的不同结构的循环神经网络上与同类方法POPQORN[23]进行了对比实验。实验结果表明, VR-RRS可以大幅度提升求得的健壮半径, 并且在验证成功率上具有明显优势。

本文的内容安排如下。第2节介绍相关背景和概念。第3节介绍本文提出的基于健壮半径求解的循环神经网络验证方法VR-RRS。第4节通过对比实验对所提出的方法进行评估。第5节总结全文。

2 背景知识

2.1 循环神经网络

循环神经网络是一种具有递归结构的神经网络。这种特殊的结构可以记忆上一个输入序列的特性, 因此这种网络善于从具有一定顺序意义的样本与样本间学习规律, 适用于解决连续序列相关的问题, 如自然语言处理。循环神经网络的主要计算过程用数学公式展示如下:

式(1)表示循环神经网络隐藏层的状态传递, 其中a(k)代表第k层的隐藏层状态,Waa代表隐藏层与隐藏层之间的权值矩阵,x(k)代表第k层的输入,Wax代表连接隐藏层与输入层的权重,ba代表隐藏层的偏置。从式(1)中可以看出, 循环神经网络的隐藏层状态是由当前层的输入和上一层的隐藏层状态所决定的, 这体现了循环神经网络的递归结构与记忆性质。

式(2)是循环神经网络的输出层计算公式。因为一般神经网络健壮性验证问题针对的是分类网络,所以本文选取多对一结构的用于分类的循环神经网络, 即只有最后一层拥有输出的循环神经网络。式(2)中,m代表循环神经网络的层数,F是一个代表循环神经网络的函数,WFa代表输出层权重,bF代表输出层偏置,X是整个网络的总体输入。一个简单的循环神经网络的结构示例如图1所示。

图1 一个层数为2的多对一结构循环神经网络Figure 1 A many-to-one recurrent neural network with 2 layers

2.2 健壮性验证问题定义

在给出循环神经网络的健壮性验证相关问题定义之前, 首先给出一些符号约定。令为循环神经网络的一个原始输入序列,为原始序列一个确定的扰动序列, label(X)表示输入序列的标签,f(X)代表输入序列经循环神经网络处理后得到的分类结果。

定义 1(健壮性验证问题)给定一个距离度量p和扰动距离值∊, 健壮性验证问题的目标是确定是否对于任意一个输入序列有

定义 2(健壮半径)给定一个距离度量p, 若扰动距离值∊满足则称∊是网络的一个健壮半径。

理论上存在健壮半径的上确界。然而, 文献[11]证明了即使是计算一个简单的仅使用ReLU激活函数神经网络的健壮半径上确界也是NP完全问题。基于近似求解方法实际求解出的健壮半径往往小于其上确界, 求解得到的健壮半径大小也是衡量近似求解方法优劣的重要标准。通常求解出的神经网络近似区间越精确, 能够求得的健壮半径越大。

2.3 激活函数线性近似

近似求解方式需要计算出近似区间关于输入的线性表达式, 然而神经网络常常采用非线性的激活函数。为此, 需要对激活函数进行线性松弛。线性松弛过程中上边界线与下边界线可分别用如下公式表示:

图2 经典近似求解框架中的tanh激活函数线性近似方法Figure 2 Linear approximation method of tanh activation function in the classical approximation framework

Wu等人[28]针对经典近似求解框架中存在的线性边界线对激活函数近似不够紧密的问题, 提出了一种细粒度的tanh激活函数线性近似方法。这种方法同样将激活函数的上界线与下界线的确定分为三种情况, 如图3所示。其中K为通用的记号此时, 上边界线为左右两个端点的连线, 下边界线为区间上某一点(d,tanh (d))的切线, 同时这条切线的斜率与上边界线相同。下边界线为左右两个端点的连线, 上边界线为区间上某一点的切线, 同时这条切线的斜率与下边界线相同。, 此时上边界线经过左端点并且是点的切线。下边界线经过右端点与并且是点(d,tanh (d))的切线。

图3 细粒度的tanh激活函数线性近似方法Figure 3 Fine-grained linear approximation method of tanh activation function

与经典近似求解框架中的激活函数线性近似方法相比, 细粒度近似方法避免了个别情况下近似不够紧密的问题, 如图4所示。文献[27]通过在卷积神经网络进行健壮性验证的实验, 证明了基于细粒度近似方法可以求解出更紧密的近似区间, 同时可以获得较大的健壮半径。本工作受到该方法的启发, 并在此基础上进行了改进。

图4 两种激活函数近似方法对比Figure 4 Comparison of two approximation methods for the activation function

3 基于健壮半径求解的循环神经网络健壮性验证方法VR-RRS

本节介绍所提出方法VR-RRS的具体流程。首先, 3.1节对循环神经网络各层神经元的近似上下界进行推导。随后, 3.2节基于多路径回溯策略求解更为精确的近似区间。在此基础上, 3.3节采用一种改进的二分法对网络的健壮半径进行求解。

3.1 近似上下界公式推导

近似求解方式验证神经网络健壮性的一个关键点是在给出扰动范围后能够计算出神经元取值的上下界。本节给出循环神经网络各神经元近似上下界的具体推导过程与结果。为了方便阐述, 首先对一些相关概念进行说明。

参考经典近似求解框架, 通常只计算神经元激活前值(pre-activation)的近似上下界。对于循环神经网络而言, 需计算向量y(k)=Waaa(k-1)+Waxx(k)+ba中各元素值的近似上下界。注意到隐藏层与输出层的不同, 本文使用记号与分别代表第k层第r个神经元激活前值的下界与上界, 而使用记号与分别代表输出层第j个神经元取值的下界与上界。对这些近似上下界进行求解是一个逐层回溯迭代的过程。从数学推导层面来看, 需要各神经元的近似上下界回溯迭代至输入层, 从而得到关于输入的线性表达式, 再根据线性表达式得到关于扰动范围∊的解析表达式。为了能够得到神经元激活前值的上下界关于输入的线性表达式, 需要对非线性的激活函数进行线性松弛, 线性松弛过程如2.3节所示。

给定一个输出类别数为t, 层数为m, 隐藏层神经元数目为s的循环神经网络, 输出层第j个神经元的取值计算如下:

注意到激活函数tanh(y)被两个线性函数约束, 则有再根据式(5)结合的正负情况可以得到:

其中,(X)是Fj(X)的上界表达式, 上标m代表已经回溯到循环神经网络第m个时刻的输入层, 得到了关于第m层输入X(m)的线性表达式。为了将为非负与负数的情况统一起来, 可以采用和来统一表示前的斜率与截距,和的具体定义为:

这样, 就可以将式(6)中的两种情况合并。为了进一步简化公式表示, 定义一个矩阵此外, 将代入, 即考虑向输入层的回溯, 则有:

其中,代表矩阵Λ(m)的第j行,代表矩阵Δ(m)的第j列, 类似的记号同理。将式(7)中的系数进行整理, 分别用和来表示合并后的系数,则式(7)可进一步简化为:

至此, 推导出了输出层神经元关于第m层输入的上界表达式。

接下来向前回溯, 推导输出层神经元关于第m-1层输入的上界表达式。注意到式(8)中这一部分可回溯得到关于x(m-1)与a(m-2)的线性表达式。首先, 将a(m-1)替换为tanh(),进而对其进行线性松弛, 可得:

其中,和的含义与上述和的含义类似, 即根据的正负情况来判断, 分别取或以及或, 之后的推导同理。接下来, 采用类似的方式定义矩阵注意到并将其代入式(9)。进而使用对系数进行合并整理, 可得输出层关于第m-1层输入x(m-1)的上界表达式:

观察到式(10)与式(8)具有相同的形式。接下来可将a(m-2)进行替换, 继续回溯得到包含关于x(m-2)的与a(m-3)线性表达式, 然后重复上述迭代过程按照Fj(X)≤(X)≤…≤(X)的顺序进行推导, 得到输出层神经元上界关于输入的线性表达式:

其中, 当k=m+1时,时,本文用[m]表示集合{1,2,...,m}。

目前已得到神经元上界关于输入的表达式, 但还不是具体值。为了得到具体值需要进一步将其转化为关于扰动距离∊的解析解。考虑到k∊[m]。令距离度量q满足。根据赫尔德不等式, 可得。结合式(11),输出层神经元上界关于∊的解析解为:

同理, 第v个隐藏层神经元上界关于∊的解析解为:在式(13)中, 边界处和分别取值为至此, 已推导出循环神经网络各层神经元的近似上界。

循环神经网络输出层与第v个隐藏层神经元的近似下界的推导与上述过程类似, 结果如下:

3.2 基于多路径回溯的近似区间求解

如何得到更加精确的近似区间是基于近似求解的神经网络验证方法的关键。假设对于原始样本在扰动领域范围内的所有样本经过前向传播后神经元激活前值的精确区间为, 某种近似方法求解出的上下界构成的上近似区间为, 则有。此时,越接近,越接近则越好。注意到不同的求解方法往往能求解出不同的上下界(上近似区间), 假设有两种求解方法求解出的区间分别为与, 两者的交集依然是精确区间的上近似区间, 并且精确程度不低于与。一个更紧密的区间有利于构造一个更精确的线性近似抽象, 有助于提高后续神经元近似区间求解的精确程度。由此可看出, 构造不同的近似区间回溯迭代过程, 并利用它们的求解得到的近似区间求交集, 可以得到更优的近似区间。

观察3.1节的回溯迭代过程和最终求得的关于输入的线性表达式可以发现, 关于输入的系数是由循环神经网络的权重以及激活函数线性近似步骤得到的斜率与截距组成的。由于权重是固定的, 因此对于同一个神经元的近似区间的计算而言, 构造不同的回溯迭代过程需要构造不同的激活函数的线性近似方法。2.3节以tanh激活函数为例介绍了经典近似求解框架使用的线性近似方式与细粒度的线性近似方式。可以观察出, 细粒度近似方式较经典近似求解框架的近似方式有着不同的分类模式, 可以避免经典近似求解框架中部分情况下出现的近似不紧密的现象, 如图3所示。同时, 文献[28]表明, 随着待验证的神经网络模型深度越高, 细粒度线性近似方式往往能够更好地改善验证的效果。循环神经网络通常具有较高的深度, 因此这种方式非常适合用于求解循环神经网络验证问题中的近似区间。然而, 这种细粒度的线性近似方式仍有可以改进的空间, 比如2.3节中提及的细粒度近似方法的前两种情况, 分别作切线的下边界线与上边界线与两个端点的连线平行。为了达到这种效果, 需要通过二分法去找到对应的激活函数点, 增大了时间开销。然而, 并没有理论与实验依据表明取平行线的方式一定能取得最佳的近似效果, 可构造激活函数的不同的近似方式。例如,可以选择在细粒度近似方式的前两种情况选择点的切线分别作为下边界线与上边界线, 如图5所示。

图5 改进的细粒度近似方式Figure 5 Improved fine-grained approximation

基于上述分析, 本文提出多路径回溯策略, 即通过调整细粒度近似的情况(a)中的下边界线与情况(b)中的上边界线来构造不同的回溯路径, 并计算各路径求得的近似区间的交集作为结果。具体而言, 定义一个参数θ来控制构造不同的细粒度近似方式。即根据参数θ, 对于情况(a)将下边界线选取为点的切线,对于情况(b)将上边界线选取为点的切线。每种参数θ的取值得到一条回溯路径, 图5可看作是θ=0.5的特例。同时, 用n代表回溯路径数,选取以及细粒度近似对应的路径共计n条路径。由于包含了细粒度近似对应的路径, 这样可以确保比单纯使用细粒度近似方式取得的结果更精确。以n=7为例, 选取θ=0,0.1,0.2,0.3,0.4,0.5与细粒度近似共计7条路径。将θ=0,0.1,0.2,0.3,0.4,0.5代表的回溯路径分别称为第1到第6条路径, 细粒度近似代表的路径称为第7条路径。前6条路径相对应于上述两种情况的激活函数线性近似方式如图6所示, 注意第7条路径的情况已在图3中给出。接下来, 定义不同路径下的近似区间上下界记号。令和分别表示第k条路径求解出的输出层第j个神经元的上下界,和分别表示第k条路径求解出的第z层隐藏层第j个神经元的上下界。以为例, 根据式(12)可得:

图6 n=7时前6条路径使用的激活函数近似方式Figure 6 Approximation of the activation function used by the first 6 paths with n=7

式(16)中部分符号具体定义如下:

对于∀r∊s,z∊[m-1]则有:

而、和可分别根据类似的过程求得, 其中和根据和结合对应路径的激活函数近似方式得到, 这里不再赘述。

基于上述多路径回溯策略的循环神经网络近似区间求解如算法1所示。其中,和分别对应第k条路径得到的区间上下界,代表n条路径求出的近似区间的交集, 也是该方法最终实际求得的第i层第j个神经元的近似区间。

算法 1.基于多路径回溯的近似区间求解输入: 循环神经网络的权重与偏置参数, 扰动范围∊, 距离度量p, 回溯路径数n, 原始样本X 0;输出: 循环层各神经元激活前值近似区间的上下界, 输出层神经元近似区间的上下界。1.F O R i←1 T O m D O 2.F O R j←1 T O s D O 3.F O R k←1 T O n D O=∩ //将各个路径近似区间取交集得到更精确的近似区间6.F O R k←1 T O n D O 7.()()()()l u←根据回溯迭代公式计算上下界5.()()[,]4.()(),,,i i j k j k l u←()()i i j j n j k k,,1[,]l u i i j k α α β β←交集区间()()[,]L,,U,,L,,U,,i i i i j k j k j k j k ,,,l u在不同的激活函数线性近似方式计算得到8.F O R j←1 T O s D O 9.F O R k←1 T O n D O i i j j γ γ←根据回溯迭代公式计算上下界1 1.UL[,]1 0.UL,,,j k j k=∩γ γ←UL n j j j k k,,1[,]γ γ j k

算法1保持了经典近似求解框架的高效性。设m表示网络层数,s表示隐藏层神经元数目。根据文献[20]可知, 采用单路径回溯的经典近似求解方法的时间复杂度为O(m2s3)。因此, 算法1的时间复杂度为O(nm2s3), 其中n为多路径回溯策略中的路径数。当n选取一个较小的整数, 例如n=7时, 算法1的耗时与经典近似求解方法规模相同, 相较于有着指数时间复杂度的基于优化的精确求解方法依然有着明显的优势。4.2节将通过实验对路径数n的选取进行分析。

3.3 健壮半径求解

在循环神经网络近似区间求解的基础上, 进一步对健壮半径进行求解。一种可行的二分法思想是:预设一个扰动距离的初始值∊, 由此求得输出层神经元近似区间上下界的具体值; 通过比较输出层目标神经元近似区间的下界与其他各神经元近似区间的上界来判断循环神经网络是否具有健壮性; 并根据判断结果调整∊的取值, 进入下一轮的计算, 直至∊值达到规定的精度。设label(X)为j, 则每一轮计算会检查∀i≠＞是否满足。若满足则可判定循环神经网络健壮, 进而对∊进行放大; 反之, 则无法判定网络是否健壮, 进而对∊进行缩小。然而, 这种经典的二分处理方式存在一个问题。在每一轮计算中, 上下界和各自都经过了一次赫尔德不等式的放缩, 造成了一定程度的精度缺失, 可能导致一些本可被判定为健壮的情况被判断为不确定。

针对这一问题, VR-RRS采用一种改进的二分法来求解健壮半径。不直接计算上下界和, 而是定义一个函数Di(X)=Fj(X)-Fi(X)。根据3.1节的

推导可得:

将Di(X)的近似区间下界关于∊的解析记作δiL,则有:

其中部分符号定义如下:

通过判断是否大于0即可得出神经网络是否具有健壮性的结论。这样减小了因不等式放缩带来的对于近似区间精确度的影响。式(17)仅展示了单一路径下的求解, 在实际求解过程中使用的是3.2节提出的多路径回溯策略。

综上所述, 基于改进的二分法的健壮半径求解如算法2所示。

算法 2.基于改进的二分法的健壮半径求解输入: 真实标签j, 循环神经网络的权重与偏置参数, 二分区间的初始上界∊ini, 二分法终止精度acc;输出: 健壮半径∊cert。1.ubini,lb0∊=∊∊=2.WHILE L,0 i∀≠＞ DO 3.lbubublb ijδ∊∊∊∊4.FOR i←1 TO t DO 5.IF i != j←←×,2 6.L iδ←代入∊ub计算得到7.WHILE ublbacc∊∊ DO 8.-＞←∊∊∊()2 lb+ub 9.L jδ←代入∊计算得到L jδ 10.FOR i←1 TO t DO 11.IF i != j 12.L iδ←代入∊计算得到13.IF ,L0∀≠＞ then ijδi

在算法2中, 第2-6行为确定二分法下界与上界的过程, 即确定一个满足健壮性判定条件的扰动下界∊lb, 以及一个不满足健壮性判定条件的扰动上界∊ub。第7-16行为采用改进的二分法确定健壮半径的过程, 当上下界之差小于预设精度后即返回二分下界作为最终求得的健壮半径∊cert。

4 实验与分析

本节从求解出的健壮半径与健壮性验证成功率这两个角度通过实验对VR-RRS进行评估, 并与已有的循环神经网络验证方法POPQORN[23]进行对比分析。同时, 为了证明本方法中多路径回溯策略的有效性, 对使用多路径回溯与仅使用单路径回溯策略的实验结果进行对比分析。实验选择在64位Ubuntu18.04平台上进行, CPU为16核的Intel Core i9-9900K, 频率为3.60GHZ, 内存为32GB。各循环神经网络均使用Python 3.8来实现。

关于训练循环神经网络数据集, 实验选择手写数字数据集MNIST。它是神经网络验证大赛VNN-COMP采用的三种数据集之一。另两种分别为彩色图像分类数据集CIFAR和无人机防撞系统数据集ACAS Xu。然而, 由于循环神经网络识别彩色图像准确率较低, 且ACAS Xu的样本维度过低, 这两种数据集不太适用于循环神经网络的建模处理。

MNIST数据集由手写数字0-9的图片样本组成。每张图片为28×28像素的灰度图像, 其中每个像素点取值范围为[0, 255], 样本示例如图7所示。为了适应循环神经网络的特点, 实验对样本进行一定的调整。例如, 对于一个4层的循环神经网络, 样本格式被调整为4×196, 即每个时刻输入层大小为196。所有训练样本都被标准化为均值为0, 标准差为1的数据。

图7 MNIST数据集样本示例Figure 7 Example samples of the MNIST dataset

4.1 方法性能比较

(1) 健壮半径

为了能够全面准确地分析对比VR-RRS与POPQORN, 本文在多个循环神经网络模型上进行健壮半径求解的实验。这些RNN模型具有不同的层数与隐藏层尺寸。为了叙述的方便, 使用RNN-4-32代表一个层数为4, 隐藏层尺寸为32的循环神经网络模型, 其余模型也用相同的方式表示。同时, 在每个模型上的实验均使用在测试集中能够被该模型正确分类的100个样本。VR-RRS中的回溯路径数设置为7, 即回溯路径为θ=0,0.1,0.2,0.3,0.4,0.5以及细粒度近似代表的路径。表1给出了两种方法在不同循环神经网络模型和距离度量下求得的健壮半径详细结果, 包括均值、最大值、最小值。

表1 VR-RRS与POPQORN求解出的健壮半径对比Table 1 Comparison of robust radius calculated by VR-RRS and POPQORN

从实验结果可以看出, 在所有神经网络模型以及距离度量下, VR-RRS求解出的健壮半径均值相较于POPQORN提高了19.3%~37.7%不等, 并且健壮半径的最大值和最小值也有着显著的提升。较大的健壮半径意味着更高的健壮性保障, 这充分说明了VR-RRS具备良好的性能。此外, 从表1可以看出,对于层数较高的循环神经网络模型, VR-RRS相较于POPQORN求解出的健壮半径的改善率也相对较高。对于4层的网络改善率为19.3%~21.4%, 对于7层的网络改善率为21.9%~25.6%, 而对于14层的网络改善率为29.1%~37.7%。这一结果说明本方法能够有效地验证具有较大深度的循环神经网络。

(2) 验证成功率

基于近似求解的神经网络验证方法是单边性的保障手段。当方法给出模型健壮的结论, 如扰动不超过健壮半径时, 那么该结论一定是可靠的, 此时验证成功。反之, 方法会给出不确定的结论, 但无法断定模型一定不健壮, 此时可以看做验证不成功。这也是制约近似求解验证方法应用的主要因素。因此, 提高这类方法的成功率显得尤为重要。表2给出了VR-RRS与POPQORN在RNN-7-32与RNN-7-64模型上对于不同大小的扰动(基于l1距离度量)下的验证成功率。

表2 VR-RRS与POPQORN验证成功率对比(验证样本数为100)Table 2 Comparison of verification success rate of VR-RRS and POPQORN (the number of verification samples is 100)

从实验结果可以看出, 在不同大小的扰动情况下, VR-RRS的验证成功率较POPQORN均有较大提升。其中, 对于RNN-7-32模型而言, 当扰动大于0.6时, POPQORN已不能够进行成功的验证, 而VR-RRS依然能够验证少部分样本; 对于RNN-7-64,在扰动值等于0.6时, POPQORN仅能验证出100张实验样本中的4张, 而VR-RRS能验证26张, 成功率是POPQORN的6.5倍, 显示了VR-RRS较为良好的可用性。

以上用两种方法在不同扰动类型以及不同网络模型进行对比的实验结果表明, VR-RRS的验证精度较POPQORN有显著提升。

本文的工作与同类工作POPQORN[23]均受到经典近似求解框架的启发。与POPQORN直接沿用了经典近似求解框架中激活函数的近似方法不同的是,本文提出了一种针对非线性激活函数的多路径回溯求解策略以提升求解的精度。此外, 在健壮半径求解阶段, 本文改进了POPQORN所使用的二分法求解方式。本文提出的多路径回溯策略在单个路径的构造上借鉴了文献[28]提出的细粒度的近似方式, 并在此基础上做了细节上的改进。同时, 与文献[28]旨在验证卷积神经网络不同的是, 本文验证的对象为循环神经网络。

值得指出的是, 另一项研究循环神经网络健壮性验证的工作CERT-RNN[24]亦取得了较优的性能。该工作基于使用zonotope抽象域的验证框架DeepZ[29], 并在此基础上改进了tanh激活函数的抽象变换方法。这一框架专门支持l∞范数度量下健壮半径的高效求解。与该工作不同的是, 本文的工作VR-RRS基于经典近似求解框架, 并在此基础上提出了一种多路径回溯的近似区间求解策略, 支持在各种距离度量下有效地求解健壮半径, 如l1、l2、l∞范数等。

4.2 多回溯路径对性能的影响分析

使用多路径回溯策略进行近似区间求解是本文提出的方法VR-RRS较经典近似求解框架的一个显著的改进, 也是得以提升近似区间求解精度与健壮性验证性能的关键。因此, 对使用多路径回溯策略与只使用单路径回溯的朴素方法的性能进行对比分析是有意义的。首先, 本文在RNN-14-32网络模型上使用多路径回溯策略(回溯路径数n=7)以及构成该多路径的各个单路径回溯策略进行了健壮半径求解实验, 数据结果如表3所示。

表3 使用7种单路径回溯策略与多路径回溯策略求解出的健壮半径对比Table 3 Comparison of robust radius calculated by 7 single-path backtracking strategies and the multi-path backtracking strategy

从表3可以观察到, 在7种单路径回溯策略中,θ=0.4的策略求解出的健壮半径最大,θ=0的策略求解出的健壮半径最小。原始细粒度近似方法并未求解出最大的健壮半径, 这也证实了本工作在2.2节的分析猜想。同时, 即使相较于θ=0.4的策略求解出的健壮半径结果, 使用多路径回溯策略仍提升了约15%, 这进一步证明了多路径回溯策略的有效性。

从以上实验可以看出多路径回溯策略对于求解效果的改善, 然而并非路径越多越好。如果路径选择不当, 求解出的近似区间的精确性很低, 对于多路径回溯策略不仅没有帮助而且增大了求解的时间开销。另一方面, 基于近似求解的方法也存在着精度上的理论上限[30]。因此, 有必要探究路径数量对求解效果的影响。本文在RNN-14-32网络模型上选取不同的路径数开展了健壮半径求解实验, 数据结果如表4所示。

表4 选取不同路径数n的多路径回溯策略求解出的健壮半径对比Table 4 Comparison of robust radius calculated by the multi-path backtracking strategy with different path number n

从表4可以观察到, 在路径数n由5增长至7的过程中, 多路径回溯策略求得的健壮半径有着一定的增幅。另一方面, 当路径数n大于7时得到的结果与n=7几乎相同。平衡考虑时间与性能, 本文认为n=7是相对最为合理的选择。在前一实验中观察到θ=0.4或θ=0.5的单路径回溯策略求解出的结果最佳, 这在一定程度上也可以作为选择路径的依据。

根据3.2节的分析, 采用多路径回溯策略的时间复杂度原则上是单路径回溯的n倍, 其中n为路径数。然而, 值得注意的是, 对于循环神经网络同一层的同一个神经元而言, 不同路径的近似区间计算过程互不影响, 因此可以采用多线程技术进行并行计算, 这将大大减少计算时间。本文在RNN-14-32网络模型上选取不同路径数, 并分别采用单线程、多线程方法开展了时间对比实验, 实验结果如表5所示。

从表5可以观察到, 在使用单线程进行计算的情况下, 求解时间与路径数呈线性相关。使用了多线程进行计算后, 选取最优路径数n=7的计算时间为121.9秒, 是使用单路径求解所需时间的2.6倍。同类方法POPQORN采用的是单路径求解方式, 求解时间与n=1的情形相当。可以看出, 本文提出的方法较大幅地提升了验证精度, 而引入的额外时间代价在可接受的范围内, 且相较于使用优化技术的精确求解方法仍有较大优势。

5 总结

本文提出了基于健壮半径求解的循环神经网络验证方法VR-RRS。该方法采用近似求解的方式, 针对经典近似求解框架精度较低的问题, 面向循环神经网络使用的非线性激活函数设计了一种多路径回溯的近似区间求解策略, 并在此基础上采用改进的二分法对健壮半径进行求解。实验结果表明VR-RRS较已有性能最佳的同类方法POPQORN能够求解出更优的健壮半径, 并拥有更高的验证成功率, 而仅需要较小的额外时间开销。本方法目前仅面向基础类型的循环神经网络。后续的工作计划对LSTM、GRU等扩展类型的循环神经网络进行验证。这两类循环神经网络的结构较之于基础类型的网络更为复杂, 例如包含非线性门的耦合。如何针对这样的结构开发出可行且精确的近似区间和健壮半径求解方法是研究的一大挑战。