Piecewise Linear Neural Network verification: A comparative study

By Rudy Bunel, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, M. Pawan Kumar. 2017

73 citations recorded by the source corpus.

The success of Deep Learning and its potential use in many important safety- critical applications has motivated research on formal verification of Neural Network (NN) models. Despite the reputation of learned NN models to behave as black boxes and the theoretical hardness of proving their properties, researchers have been successful in verifying some classes of models by exploiting their piecewise linear structure. Unfortunately, most of these approaches test their algorithms without comparison with other approaches. As a result, the pros and cons of the different algorithms are not well understood. Motivated by the need to accelerate progress in this very important area, we investigate the trade-offs of a number of different approaches based on Mixed Integer Programming, Satisfiability Modulo Theory, as well as a novel method based on the Branch-and-Bound framework. We also propose a new data set of benchmarks, in addition to a collection of pre- viously released testcases that can be used to compare existing methods. Our analysis not only allows a comparison to be made between different strategies, the comparison of results from different solvers also revealed implementation bugs in published methods. We expect that the availability of our benchmark and the analysis of the different approaches will allow researchers to develop and evaluate promising approaches for making progress on this important topic.

Subfields: Artificial Intelligence

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

Citations in the corpus

Reachability Analysis of Deep Neural Networks with Provable Guarantees (2018, methodology): “…solved by MILP [Lomuscio and Maganti, 2017; Cheng et al., 2017; Bunel et al., 2017; Xiang et al., 2017], SAT [Narodytska et al., 2017] or SMT [Katz et al., 2017; Bunel et al., 2017] techniques, or applying search algorithms over discretised vector spaces [Huang et al., 2017; Wicker et al., 2018].”
A Dual Approach to Scalable Verification of Deep Networks (2018, methodology): “This is a significant advantage compared to previous approaches used in [Bunel et al., 2017].”
Adversarial Risk and the Dangers of Evaluating Against Weak Attacks (2018, methodology): “In this vein, we note the growing community on verification of neural networks (Katz et al., 2017; Bunel et al., 2017; Carlini et al., 2017), which provide techniques to compute provably worst-case adversarial examples.”
On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models (2018, methodology): “Substantial progress has been made: from complete methods that use Satisfiability Modulo Theory (SMT) [14–16] or Mixed-Integer Programming (MIP) [13, 17, 18] to incomplete methods that rely on solving a convex relaxation of the verification problem [19–26].”
On the Robustness of Semantic Segmentation Models to Adversarial Attacks (2017, background): “Recently, progress has been made on formal verification of neural networks [49, 14] which can provably compute whether adversarial examples with a particular norm exist for a network.”
Achieving Verified Robustness to Symbol Substitutions via Interval Bound Propagation (2019, methodology): “Previous work can be categorised into complete methods that use MixedInteger Programming (MIP) (Bunel et al., 2017; Cheng et al., 2017) or Satisfiability Modulo Theory (SMT) (Katz et al.”
The Marabou Framework for Verification and Analysis of Deep Neural Networks (2019, methodology): “Due to technical difficulties, ReluVal was not run on the CollisionDetection and TwinStream benchmarks.”
A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability (2018, background): “Additionally, [Bunel et al., 2017] presents a branch and bound (B&B) algorithm and claims that both SAT/SMT-based and MILP-based approaches can be regarded as its special cases.”
Evaluating Robustness of Neural Networks with Mixed Integer Programming (2017, methodology): “Our work relates most closely to other work on veriﬁcation of piecewise-linear neural networks; [5] provides a good overview of the ﬁeld.”
Lipschitz-Certifiable Training with a Tight Outer Bound (2020, methodology): “Thus, many veriﬁcation methods are proposed to guarantee stable prediction of input within a perturbation set [18, 5, 9, 16, 38, 34, 23, 11, 3, 30, 8, 43, 2].”