Github link: https://github.com/zhangzhaodi233/NeWise

Zhaodi Zhang

East China Normal University

Yiting Wu

East China Normal University

Si Liu

ETH Zurich

Switzerland

Jing Liu

East China Normal University

Min Zhang

East China Normal University

China

The robustness of deep neural networks is crucial to modern AI-enabled systems. Formal verification has been demonstrated effective in providing certified robustness guarantees. 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 a theoretical foundation. 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 experimental results demonstrate the promising performance achievement of our approaches over state of the art: (i) achieving up to 436.36% improvement to certified lower robustness bounds; and (ii) exhibiting notably more precise verification results on convolutional networks.

Zhaodi Zhang

East China Normal University

Yiting Wu

East China Normal University

Si Liu

ETH Zurich

Switzerland

Jing Liu

East China Normal University

Min Zhang

East China Normal University

China