Linear relaxation based perturbation analysis (LiRPA) for neural networks,
which computes provable linear bounds of output neurons given a certain amount
of input perturbation, has become a core component in robustness verification
and certified defense. The majority of LiRPA-based methods focus on simple
feed-forward networks and need particular manual derivations and
implementations when extended to other architectures. In this paper, we develop
an automatic framework to enable perturbation analysis on any neural network
structures, by generalizing existing LiRPA algorithms such as CROWN to operate
on general computational graphs. The flexibility, differentiability and ease of
use of our framework allow us to obtain state-of-the-art results on LiRPA based
certified defense on fairly complicated networks like DenseNet, ResNeXt and
Transformer that are not supported by prior works. Our framework also enables
loss fusion, a technique that significantly reduces the computational
complexity of LiRPA for certified defense. For the first time, we demonstrate
LiRPA based certified defense on Tiny ImageNet and Downscaled ImageNet where
previous approaches cannot scale to due to the relatively large number of
classes. Our work also yields an open-source library for the community to apply
LiRPA to areas beyond certified defense without much LiRPA expertise, e.g., we
create a neural network with a probably flat optimization landscape by applying
LiRPA to network parameters. Our opensource library is available at
https://github.com/KaidiXu/auto_LiRPA.