Safety Veriﬁcation of Deep Neural Networks ∗

By Xiaowei Huang. 2017

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

Certified Robustness to Adversarial Examples with Differential Privacy (2018, background): “Second, several works seek to formally verify [24], [28] or lower bound [48], [58] the robustness of pre-trained ML models against adversarial attacks.”
Wild Patterns: Ten Years After the Rise of Adversarial Machine Learning (2017, background): “Another interesting avenue to provide reliable guarantees on the security of neural networks is formal veriﬁcation , which however has only been considered for simple network architectures [80].”
Certified Adversarial Robustness via Randomized Smoothing (2019, methodology): “Exact methods are usually based on Satisfiability Modulo Theories (Katz et al., 2017; Carlini et al., 2017; Ehlers, 2017; Huang et al., 2017) or mixed integer linear programming (Cheng et al., 2017; Lomuscio & Maganti, 2017; Dutta et al., 2017; Fischetti & Jo, 2018; Bunel et al., 2018).”
Efficient Formal Safety Analysis of Neural Networks (2018, background): “Several researchers have tried to extend and customize Satisﬁability Modulo Theory (SMT) solvers for estimating decision boundaries with strong guarantees [17, 18, 15, 10, 31].”
AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation (2018, methodology): “[18] showed a veriﬁcation framework, based on an SMT solver, which veriﬁed the robustness with respect to a certain set of functions that can manipulate the input and are minimal (a notion which they deﬁne).”
Evaluating the Robustness of Neural Networks: An Extreme Value Theory Approach (2018, background): “On the other hand, works done by Ehlers (2017); Katz et al. (2017a;b); Huang et al. (2017) focus on formally verifying the viability of certain properties in neural networks for any possible input, and transform this formal veriﬁcation problem into satisﬁability modulo theory (SMT) and large-scale…”
Provable defenses against adversarial examples via the convex outer adversarial polytope (2017, background): “The ﬁrst (which is a topic that is broader than merely adversarial examples), is the work in the veriﬁcation of neural networks [Huang et al., 2017, Katz et al., 2017, Ehlers, 2017].”
Certifying Some Distributional Robustness with Principled Adversarial Training (2017, background): “Alternative approaches that provide formal veriﬁcation of deep networks [31, 33, 34] are NP-hard in general; they require prohibitive computational expense even on small networks.”
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (2017, background): “…beyond the reach of general-purpose tools such as linear programming ( LP ) solvers or existing satisﬁability modulo theories ( SMT ) solvers [3, 10, 28], and thus far, dedicated tools have only been able to handle very small networks (e.g. a single hidden layer with only 10 to 20 hidden nodes…”
Efficient Defenses Against Adversarial Attacks (2017, background): “Furthermore, if one would try to prove that a model is indeed secure (that is, can withstand attacks yet to be designed), one would have to provide formal proof, say, through veriﬁcation [10].”
Verifiable Reinforcement Learning via Policy Extraction (2018, background): “There has been work on verifying machine learning systems [3, 30, 16, 6, 19, 18, 15].”
Reachability Analysis of Deep Neural Networks with Provable Guarantees (2018, methodology): “We show that the safety veriﬁcation problem [6] can be reduced to solving the reachability problem.”
Scaling provable adversarial defenses (2018, methodology): “…on using exact (combinatorial) solvers to verify the robustness properties of networks, either via Satisﬁability Modulo Theories (SMT) solvers [Huang et al., 2017, Ehlers, 2017, Carlini and Wagner, 2017] or integer programming approaches [Lomuscio and Maganti, 2017, Tjeng and Tedrake, 2017,…”
A Dual Approach to Scalable Verification of Deep Networks (2018, background): “In the formal veriﬁcation community, Satisﬁa-bility Modulo Theory (SMT) solvers have been adapted for veriﬁcation of neural networks [Ehlers, 2017, Huang et al., 2017, Katz et al., 2017].”
Ground-Truth Adversarial Examples (2017, background): “In recent years, new techniques have been proposed for the formal veriﬁcation of neural networks [4, 9, 12, 17, 18].”