AI 2 : Safety and Robustness Certification of Neural Networks with Abstract Interpretation

By Timon Gehr. 2018

Subfields: Safety, Robustness & Interpretability, Program Analysis & Verification

How researchers see this paper

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

In Safety, Robustness & Interpretability

In Program Analysis & Verification

Citations in the corpus

Training verified learners with learned verifiers (2018, neutral): “Algorithms based on formal veriﬁcation [7, 10, 14] and mixed integer programming [9, 27] have been proposed to solve this problem for networks with piecewise linear activation functions (like ReLUs and maxpooling).”
Formal Security Analysis of Neural Networks using Symbolic Intervals (2018, background): “[14] leverages zonotopes for approximating each ReLU outputs.”
Scaling provable adversarial defenses (2018, background): “For example, Gehr et al. [2018] develop a suite of veriﬁcation methods based upon abstract interpretations (these can be broadly construed as relaxations of combinations of activations that are maintained as they pass through the network).”
Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for L0 Norm (2018, background): “Recently, some researchers use abstract interpretation to verify the correctness of DNNs [4,14].”
CRADLE: Cross-Backend Validation to Detect and Localize Bugs in Deep Learning Libraries (2019, methodology): “Adversarial Testing of DL Models: Much recent work focuses on testing DL models [19], [21]–[25], [50]–[55].”
A Statistical Approach to Assessing Neural Network Robustness (2018, background): “In other work spanning both communities (Gehr et al., 2018; Weng et al., 2018a; Wong & Kolter, 2018), researchers have relaxed the satisﬁability problem of classical veriﬁcation, and are able to produce certiﬁcates-of-robustness for some samples (but not all that are robust) by giving a lower-bound…”
Evaluating Robustness of Neural Networks with Mixed Integer Programming (2017, background): “…employ a range of techniques, including duality [13, 32], layer-by-layer approximations of the adversarial polytope [41], discretizing the search space [23], abstract interpretation [16], bounding the local Lipschitz constant [40], or bounding the activation of the ReLU with linear functions [40].”
MixTrain: Scalable Training of Formally Robust Neural Networks (2018, methodology): “To solve such problem, sound approximations successfully simplify the verification problem with traditional analysis methods like interval [7], convex polytope [26], abstract domain [28], Lagrangian relaxation [29] and Lipschitz continuous [65], [30].”
A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks (2019, background): “This leads to interval bounds propagation (IBP) (Gowal et al., 2018) ( k = 1 ) and “Hybrid Zonotope Domain” (Mirman et al., 2018) (general k ) which gives even looser bounds, but its computation cost is also greatly reduced to O ( Lk ) .”