Training verified learners with learned verifiers

By Krishnamurthy (Dj) Dvijotham, Sven Gowal, Robert Stanforth, Relja Arandjelovi'c, Brendan O'Donoghue, Jonathan Uesato, Pushmeet Kohli. 2018

176 citations recorded by the source corpus.

This paper proposes a new algorithmic framework, predictor-verifier training, to train neural networks that are verifiable, i.e., networks that provably satisfy some desired input-output properties. The key idea is to simultaneously train two networks: a predictor network that performs the task at hand,e.g., predicting labels given inputs, and a verifier network that computes a bound on how well the predictor satisfies the properties being verified. Both networks can be trained simultaneously to optimize a weighted combination of the standard data-fitting loss and a term that bounds the maximum violation of the property. Experiments show that not only is the predictor-verifier architecture able to train networks to achieve state of the art verified robustness to adversarial examples with much shorter training times (outperforming previous algorithms on small datasets like MNIST and SVHN), but it can also be scaled to produce the first known (to the best of our knowledge) verifiably robust networks for CIFAR-10.

Subfields: Artificial Intelligence, Computer Vision and Pattern Recognition, 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 Computer Vision and Pattern Recognition

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): “Another line of research has focused on strengthening network robustness either by incorporating these relaxation methods into training process [43, 8, 24] or by leveraging techniques like differential privacy [22].”
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 verified (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).”
On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models (2018, methodology): “[23] fix the activation bounds and optimize the dual solution using an additional verifier network.”
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].”
Bag of Tricks for Adversarial Training (2020, background): “Other more theoretically guaranteed routines include training provably robust networks (Dvijotham et al., 2018a;b; Hein & Andriushchenko, 2017; Wong & Kolter, 2018) and obtaining certiﬁed models via randomized smoothing (Cohen et al., 2019).”
Fast and Stable Interval Bounds Propagation for Training Verifiably Robust Models (2019, methodology): “[2018a], Kurakin et al. [2016], Tramer et al. [2017], Yuan et al. [2019]. One extremely effective way to defend against adversarial examples is to generate such examples in the training stage Madry et al.”
InfoBERT: Improving Robustness of Language Models from An Information Theoretic Perspective (2020, methodology): “Recent work (Huang et al., 2019; Jia et al., 2019) has applied IBP in the NLP domain to certify the robustness of models.”
Certifying LLM Safety against Adversarial Prompting (2023, methodology): “They use techniques such as interval-bound propagation (Gowal et al., 2018; Huang et al., 2019; Dvijotham et al., 2018; Mirman et al., 2018), curvature bounds (Wong & Kolter, 2018; Raghunathan et al.”
Towards Stable and Efficient Training of Verifiably Robust Neural Networks (2019, background): “Other similar approaches include Mirman et al. (2018); Wang et al. (2018a); Dvijotham et al. (2018b).”
Learning to Give Checkable Answers with Prover-Verifier Games (2021, unknown): “consistent models [28, 36, 23, 7] and those that formally verify adherence to specifications [17, 7, 30].”
Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond (2020, methodology): “Several further refinements for the LiRPA bounding process were also proposed recently, including using an optimizer to choose better linear bounds [7, 29], relaxing multiple neurons [39] or further tighten convex relaxations [42], but these methods typically involve much higher computational costs.”
Achieving Verified Robustness to Symbol Substitutions via Interval Bound Propagation (2019, methodology): “Incomplete methods provide loose robustness bounds, but can be more scalable and used inside the training loop for training models to be robust and verifiable (Raghunathan et al., 2018; Wong and Kolter, 2018; Dvijotham et al., 2018; Gowal et al., 2018).”
Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability (2018, methodology): “…= 2/255 45.93% 13.50 = 8/255 20.27% 22.33 Our network for = 0.1 on MNIST achieves provable adversarial accuracies comparable with the current best results of Wong et al. (2018) and Dvijotham et al. (2018), and our results for = 0.2 and = 0.3 achieve the best provable adversarial accuracies yet.”
A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks (2019, methodology): “This can be done by recursively solving ( O ) with speciﬁc choices of c and c 0 , which is a common technique used in many works (Wong & Kolter, 2018; Dvijotham et al., 2018d).”
Strong mixed-integer programming formulations for trained neural networks (2018, methodology): “Note that we make no attempts to utilize recent techniques that train the networks to be verifiable [21,53,54,56].”