Formal Security Analysis of Neural Networks using Symbolic Intervals
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana Columbia University
最近精读了这一篇论文，整理一下自己的感受。
摘要
在DNN普及的环境下，人们对DNN的安全性分析越来越重视（尤其是交通的防碰撞系统），但最近较多使用的SMT solver耗费资源巨大。因此本论文提出了一种新的，用于分析DNN安全性的框架——reluval。Reluval使用区间分析的方法寻找DNN的对抗样本，对DNN的输入区间进行两种方法的结合分析：Symbolic intervals和 Iterative refinement（split）。由此得到的分析框架可以容易地实现并行，相比于Reluplex（一种先进的DNN安全性验证方法）快200倍。 本文的重点在于引出并证明Symbolic intervals和 Iterative refinement，尤其是证明Iterative refinement的正确性，并在此基础上构建reluval的工作流程，以及加以实现。最后在ACASXu和mnist上对reluval模型进行评价。
研究的问题
区间分析（interval analysis）问题。首先文章针对任意DNN抽象出的函数f定义了一种区间扩展函数F（X），X为DNN的输入区间[X1,X2,…,Xd]，F的输出为DNN输出值的区间。（DNN输出值的区间用f（X）表示，F是我们要优化的目标，使其接近f（X））。 在此基础上，本文还给F定义了inclusion isotonic（值域包含子集的值域），Lipschitz continuous（区间宽度作为斜率）三种区间分析方法。文章举例列出了3种区间分析的方法：Naive interval propagation；Symbolic interval propagation； Iterative bisection and refinement。后两种对应了Symbolic intervals和 Iterative refinement。3种分析方法如下图： Naive interval propagation有严重的dependency problem，会极大的高估输出域。而Symbolic interval propagation可以精确地输出，但存在的问题是激活函数relu是非线性的，当某一个relu单元输入值为负时无法继续进行符号分析。解决这个问题的方法是第三个Iterative refinement。下面文章会证明Iterative refinement在分割的子区间数量n足够大时会趋近于真实值。证明。文章证明了两个问题，真实值f（X）永远为Naive interval propagation结果的子集；Iterative refinement在分割的子区间数量n足够大时会趋近于真实值。第一个证明比较显然，不再赘述。第二个证明首先利用relu的特点证明 F 是 Lipschitz continuous的。 然后利用这一点证明损失函数 随着n增大收敛于0。因此理论上使用Iterative refinement我们可以达到任何想要的精度。这就证明了reluval的正确性。Reluval的工作流程。如果估计的输出区间足够紧以满足安全需要，则它将安全属性声明为已验证。如果输出间隔显示出位置存在，则reluval随机从间隔中随机抽取几点并检查是否存在冲突。如果检测到任何冲突的情况，即违反安全属性的具体输入，它会将其作为对抗样例输出。否则，reluval使用迭代间隔定义进一步收紧输出间隔，以接近理论上最紧的界限，并重复上述相同的过程。一旦迭代次数达到预设阈值，reluval输出超时，表示它无法验证安全属性。流程如下图： 算法实现。限于篇幅，这里不再粘贴伪代码，具体可见论文7、8、9页。 对于Symbolic interval，算法实现过程中使用到了具体化（concretization）的方法部分解决了Symbolic interval非线性单元（relu节点）的问题。具体化的规则符合relu函数的规则（文章顺便还证明了这样的具体化得到的区间确实包含真实区间结果）： 对于Iterative refinement文章提出了其两种优化：Influence analysis，Monotonicity。前者的思想是使用梯度（雅可比矩阵）选择影响最大的的一个输入区间优先进行分割（后面具体算法的分析描述没大看懂，smear function什么的。。。但大概就是这个思想吧）。后者正如其名，当Fi（X）对Xj的偏导恒正或负，我们可以简单地将区间Xj替换为两个增量值 和 。Reluval的实现。前面提到Reluval可以容易地实现并行，并行的实现遇到了两个问题，一是Iterative refinement分割时树不平衡，二是由于无法预测分割深度，因此可能会有较大调度开销。为次本文开发了一个动态线程重新平衡算法，解决了这些问题。 此外，本文还在实现时解决了数据传递时round导致较小的浮点数变为0的问题。Reluval的评价。本文在ACASXu和mnist上进行评价，得到reluval可以准确缩小所有可能的对抗范围，从而提供更多的洞察对抗样例在难以察觉的位置的分布，且它可以将对抗性输入范围与非对抗性输入范围隔离开来。（总之阐明了一些可以进步的地方之后，摆出各种reluval的优点，说明reluval是当今最为优秀的dnn安全分析工具） 备注 写了两页。。。本论文还是比较适合我现在的知识水平的，而且举的例子也很易懂。本文最核心的内容大概就是在Iterative refinement收敛性的证明上，证明过程都是集合、区间计算比较容易理解。此外我认为本文对我而言最有意义的地方就是提供了区间分割方法来对DNN输出区间进行分析。 但还是有些不太理解的地方，比如smear function，这个函数应该在引用的26、27论文中，由于时间紧迫，即将赶往南京+复习本校的考试，就没看。。。不过我对Influence analysis优化的理解应该是没错的。还有后面ReluVal does not need any seed input部分也不太懂。。。
