一句话:提出网络级紧致性统一定义,并设计两种可证明最紧的线性近似,显著提升 Sigmoid 类网络鲁棒性验证精度。
深度神经网络鲁棒性的形式化验证至关重要,而 Sigmoid 类激活函数的非线性使验证通常依赖过近似,带来精度损失。现有工作致力于寻找更紧的近似,但其紧致性定义多为启发式、缺乏理论基础,且仅在某些网络上占优。本文通过实证分析神经元级紧致性刻画后,提出网络级紧致性(network-wise tightness)作为统一定义,并指出其计算是复杂的非凸优化问题。作者从两个不同视角绕过该复杂度,设计了两种可证明最紧的线性近似方法。实验表明,所提方法优于现有技术:认证鲁棒下界最高提升 251.28%,在卷积网络上给出明显更精确的验证结果。
The robustness of deep neural networks is crucial to modern AI-enabled systems and should be formally verified. Sigmoid-like neural networks have been adopted in a wide range of applications. Due to their non-linearity, Sigmoid-like activation functions are usually over-approximated for efficient verification, which inevitably introduces imprecision. Considerable efforts have been devoted to finding the so-called tighter approximations to obtain more precise verification results. However, existing tightness definitions are heuristic and lack theoretical foundations. We conduct a thorough empirical analysis of existing neuron-wise characterizations of tightness and reveal that they are superior only on specific neural networks. We then introduce the notion of network-wise tightness as a unified tightness definition and show that computing network-wise tightness is a complex non-convex optimization problem. We bypass the complexity from different perspectives via two efficient, provably tightest approximations. The results demonstrate the promising performance achievement of our approaches over state of the art: (i) achieving up to 251.28% improvement to certified lower robustness bounds; and (ii) exhibiting notably more precise verification results on convolutional networks.
@inproceedings{paperbot7306,
title = {Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural Networks},
author = {Zhaodi Zhang and Yiting Wu and Si Liu and Jing Liu and Min Zhang},
booktitle = {ASE},
year = {2022},
doi = {10.1145/3551349.3556907}
}