An abstract domain for certifying neural networks

By Gagandeep Singh, Timon Gehr, Markus Püschel, Martin T. Vechev. Proc. ACM Program. Lang., 2019

847 citations recorded by the source corpus.

We present a novel method for scalable and precise certification of deep neural networks. The key technical insight behind our approach is a new abstract domain which combines floating point polyhedra with intervals and is equipped with abstract transformers specifically tailored to the setting of neural networks. Concretely, we introduce new transformers for affine transforms, the rectified linear unit (ReLU), sigmoid, tanh, and maxpool functions. We implemented our method in a system called DeepPoly and evaluated it extensively on a range of datasets, neural architectures (including defended networks), and specifications. Our experimental results indicate that DeepPoly is more precise than prior work while scaling to large networks. We also show how to combine DeepPoly with a form of abstraction refinement based on trace partitioning. This enables us to prove, for the first time, the robustness of the network when the input image is subjected to complex perturbations such as rotations that employ linear interpolation.

Subfields: Artificial Intelligence, Computer Vision and Pattern Recognition, Statistical and Nonlinear Physics

View Paper: https://www.semanticscholar.org/paper/f20de741e2d4ece239261de010d6d9beca3b26b9

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Vision and Pattern Recognition

In Statistical and Nonlinear Physics

Citations in the corpus

Teaching Temporal Logics to Neural Networks (2020, methodology): “Another area in the intersection of formal methods and machine learning is the verification of neural networks (Seshia & Sadigh, 2016; Seshia et al., 2018; Singh et al., 2019; Gehr et al., 2018; Huang et al., 2017; Dreossi et al., 2019).”
A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks (2019, methodology): “Other activation functions can be linearly bounded as discussed in CROWN (Zhang et al., 2018), DeepZ and DeepPoly (Singh et al., 2019b); CROWN and DeepPoly are also more general and do not require a i to allow a more ﬂexible selection of bounds.”
Algorithms for Verifying Deep Neural Networks (2019, background): “15 The choice of abstract domain needs to balance 15 A detailed discussion of an abstract domain for certifying neural networks can be found in [34].”
Property-driven Training: All You (N)Ever Wanted to Know About (2021, methodology): “The main line of our future work is to extend our meth-ods and conclusions to veriﬁcation (or constraint satisfaction ) frameworks such as Marabou (Katz et al. 2019) or DeepPoly (Singh et al. 2019); and obtain more ﬂexible and general programming interaces for continuous veriﬁcation (Komendantskaya,”
Fast and Stable Interval Bounds Propagation for Training Verifiably Robust Models (2019, methodology): “As an alternative, [4] adapted the framework of ‘abstract transformers’ to compute an approximation to the adversarial polytope using the stochastic gradient descent training.”
Adversarial examples for models of code (2019, background): “Even in continuous domains, guarantees have only been provided for small networks with just 88K learnable parameters [Singh et al. 2019] and 45K parameters [Balunovic et al.”
Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification (2021, methodology): “Many cheap incomplete veriﬁers are based on bound propagation methods [46, 42, 41, 13, 17, 36, 44], i.e., maintaining and propagating tractable and sound bounds through networks, and CROWN [46] is a representative which propagates a linear or quadratic bound.”
Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond (2020, methodology): “Recent research studies have developed perturbation analysis bounds that are sound, computationally feasible, and relatively tight [48, 54, 40, 47, 38, 46].”
Exactly Computing the Local Lipschitz Constant of ReLU Networks (2020, methodology): “In brief, this is done by extending the abstract interpretation work used in certiﬁable robustness domains (Singh et al., 2019).”
Robust Deep Reinforcement Learning against Adversarial Perturbations on State Observations (2020, background): “Convex relaxation of non-linear units in neural networks enables an efficient analysis of the outer bounds for a neural network [79, 86, 66, 13, 78, 76, 57, 67].”