LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions
LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions
复制标题
DOI：
10.1007/978-3-030-99524-9_19
复制
发表时间：
2022-01
期刊：
影响因子：
--
通讯作者：
Brandon Paulsen;Chao Wang
中科院分区：
文献类型：
--
作者：
Brandon Paulsen;Chao Wang
验证神经网络鲁棒性的最可扩展的方法取决于计算网络激活函数的合理线性下限和上限。目前的方法是有限的，因为线性边界必须由专家手工制作，并且可能是次优的，特别是当网络的架构使用例如LSTM和最近流行的Swishactivation中的乘法来组成操作时。对专家的依赖阻止了鲁棒性认证在激活函数的最新发展中的应用，此外，缺乏紧密性保证可能会给人一种关于特定模型的不安全感。据我们所知，我们是第一个考虑自动合成任意n维激活函数的紧线性界的问题。我们提出了第一个完全自动化的方法，实现了严格的线性边界，同时只利用激活函数本身的数学定义。我们的方法利用一个有效的启发式技术来合成的界限是紧的，通常声音，然后验证的健全性（并调整界限，如果必要的话）使用高度优化的分支和边界SMT求解器，dReal。尽管我们的方法依赖于SMT求解器，但我们表明，在实践中运行时间是合理的，并且与最先进的方法相比，我们的方法通常可以实现2- 5倍更严格的最终输出边界和超过四倍的认证鲁棒性。
The most scalable approaches to certifying neural network robustness depend on computing sound linear lower and upper bounds for the network’s activation functions. Current approaches are limited in that the linear bounds must be handcrafted by an expert, and can be sub-optimal, especially when the network’s architecture composes operations using, for example, multiplication such as in LSTMs and the recently popularSwishactivation. The dependence on an expert prevents the application of robustness certification to developments in the state-of-the-art of activation functions, and furthermore the lack of tightness guarantees may give a false sense of insecurity about a particular model. To the best of our knowledge, we are the first to consider the problem ofautomaticallysynthesizingtightlinear bounds for arbitrary n-dimensional activation functions. We propose the first fully automated method that achieves tight linear bounds while only leveraging the mathematical definition of the activation function itself. Our method leverages an efficient heuristic technique to synthesize bounds that are tight andusually sound, and then verifies the soundness (and adjusts the bounds if necessary) using the highly optimized branch-and-bound SMT solver,dReal. Even though our method depends on an SMT solver, we show that the runtime is reasonable in practice, and, compared with state of the art, our method often achieves 2-5X tighter final output bounds and more than quadruple certified robustness.