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 provably flat optimization landscape by applying LiRPA to network parameters.

Weaknesses: There are two handicaps that I can see to this work: firstly, the methodology while impressive in its ability to generalize to LSTMs, CNNs, and Transformers actually seems like it may be limited in terms of its scope of verification procedures it admits. In the abstract the authors mention that they can implement things such as CROWN into their LiRPA algorithm, however CROWN also explicitly derives quadratic over and under approximations of pre-activation bounds and I am curious as to if the authors have a scheme for directly accommodating things of this nature along with higher-order convex relaxations (e.g. even degree 3 polynomials for small networks) which are harder to propagate in general as there are more complex dependencies. Further on this point, the method can really only handle linear constraints in the input. Indeed, the authors show how they can bound discrete perturbations in the NLP scenario, but at the end, it looks to me like the authors recursively build a linear region in the input space by taking maximally perturbed embeddings from the synonym set. Is there a plan for how to incorporate non-linear specifications?

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.