A Dual Approach to Scalable Verification of Deep Networks

By Krishnamurthy (Dj) Dvijotham, Robert Stanforth, Sven Gowal, Timothy A. Mann, Pushmeet Kohli. 2018

416 citations recorded by the source corpus.

This paper addresses the problem of formally verifying desirable properties of neural networks, i.e., obtaining provable guarantees that neural networks satisfy specifications relating their inputs and outputs (robustness to bounded norm adversarial perturbations, for example). Most previous work on this topic was limited in its applicability by the size of the network, network architecture and the complexity of properties to be verified. In contrast, our framework applies to a general class of activation functions and specifications on neural network inputs and outputs. We formulate verification as an optimization problem (seeking to find the largest violation of the specification) and solve a Lagrangian relaxation of the optimization problem to obtain an upper bound on the worst case violation of the specification being verified. Our approach is anytime i.e. it can be stopped at any time and a valid bound on the maximum violation can be obtained. We develop specialized verification algorithms with provable tightness guarantees under special assumptions and demonstrate the practical significance of our general verification approach on a variety of verification tasks.

Subfields: Artificial Intelligence, Electrical and Electronic Engineering, Hardware and Architecture, Safety, Robustness & Interpretability

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 Electrical and Electronic Engineering

In Hardware and Architecture

In Safety, Robustness & Interpretability

Citations in the corpus

Scalable agent alignment via reward modeling: a research direction (2018, methodology): “The size of veriﬁed models has been pushed beyond MNIST-size to over a million parameters (Dvijotham et al., 2018b; Wong et al., 2018), which indicates that verifying practically sized RL models might soon be within reach.”
Certified Adversarial Robustness via Randomized Smoothing (2019, methodology): “We did not compare against Dvijotham et al. (2018b) since the authors did not release code and the method is very similar to Wong et al. (2018).”
Efficient Formal Safety Analysis of Neural Networks (2018, background): “While these techniques tend to scale significantly better than solver-based approaches, they suffer from high false positive rates and struggle to find concrete counterexamples demonstrating violations of safety properties [42, 32, 13, 9].”
Formal Security Analysis of Neural Networks using Symbolic Intervals (2018, methodology): “[11] transform the verification problem into an unconstrained dual formulation using Lagrange relaxation and use gradient-descent to solve the optimization problem.”
Counterfactual Normalization: Proactively Addressing Dataset Shift and Improving Reliability Using Causal Mechanisms (2018, methodology): “To proactively address perturbations of test distributions, recent work considers formal veriﬁcation methods for bounding the performance of trained models on perturbed inputs (e.g., Raghunathan et al. (2018); Dvijotham et al. (2018)).”
Robustness May Be at Odds with Accuracy (2018, background): “…has there been progress towards models that achieve robustness that can be demonstrated empirically and, in some cases, even formally veriﬁed (Madry et al., 2017; Kolter & Wong, 2017; Sinha et al., 2017; Tjeng & Tedrake, 2017; Raghunathan et al., 2018; Dvijotham et al., 2018a; Xiao et al., 2018b).”
Scaling provable adversarial defenses (2018, methodology): “In contrast, the previous best veriﬁed robust error for this (cid:15) , from [Dvijotham et al., 2018], was 80%.”
Adversarial vulnerability for any classifier (2018, methodology): “Other works have recently studied procedures and algorithms to provably guarantee a certain level of robustness [22, 23, 24, 25, 26], and have been applied to small datasets (e.”
Adversarial examples from computational constraints (2018, background): “Perhaps the most significant developments have been related to training models with provable robustness guarantees (Dvijotham et al., 2018; Wong and Kolter, 2018; Weng et al., 2018; Xiao et al., 2018), however, currently all the methods for such training are either extremely slow or the certified bo”
On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models (2018, methodology): “As shown by Dvijotham et al. [7], many useful veriﬁcation problems ﬁt this deﬁnition.”
Provably Robust Deep Learning via Adversarially Trained Smoothed Classifiers (2019, background): “On the bright side, these methods are more scalable and efficient which makes some of them useful for building certified defenses [38, 35, 36, 27, 28, 39, 10, 9, 7, 13, 26, 30, 15, 37, 40].”
Semidefinite relaxations for certifying robustness to adversarial examples (2018, methodology): “2 which forms the basis for several existing works on scalable certification [9, 10, 28, 29].”
Adversarial Examples on Object Recognition (2020, background): “[41] propose a similar form in which the dual problem is formulated and solved using a Lagragian relaxation of the optimization problem, thus obtaining an upper bound on the robustness against adversarial examples.”
Algorithms for Verifying Deep Neural Networks (2019, methodology): “Method Name Activation Approach Input/Output Completeness ExactReach [46] ReLU Exact Reachability HP/HP(bounded)1 X AI2 [14] Piecewise Linear Split and Join HP/HP(bounded)1 × MaxSens [44] Any Interval Arithmatic HP/HP(bounded)1 × NSVerify [23] ReLU Naive MILP HR/PC2 X MIPVerify [38] ReLU and Max MIL”
Certified Adversarial Robustness with Additive Noise (2018, methodology): “Similar to [16, 17], their certified bound is agnostic to model structure and is scalable, but it is loose and is not comparable to [16, 17].”