A Unified View of Piecewise Linear Neural Network Verification
The success of Deep Learning and its potential use in many 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 and taking insights from formal methods such as Satisifiability Modulo Theory. These methods are however still far from scaling to realistic neural networks. To facilitate progress on this crucial area, we make two key contributions. First, we present a unified framework that encompasses previous methods. This analysis results in the identification of new methods that combine the strengths of multiple existing approaches, accomplishing a speedup of two orders of magnitude compared to the previous state of the art. Second, we propose a new data set of benchmarks which includes a collection of previously released testcases. We use the benchmark to provide the first experimental comparison of existing algorithms and identify the factors impacting the hardness of verification problems.
The main contribution of this paper is to provide a framework for NN verification based on Branch and Bound optimization which allows for reframing existing state-of-the-art verification methods as special cases of this framework. With this unified framework, the authors were able to identify algorithmic improvements in the verification process that lead to a speed-up of almost two orders of magnitude.   In order to design a unified framework, the authors convert the verification problem into a global optimization problem. The idea is to convert any boolean formula over linear inequalities into a sequence of linear and max-pooling layers.  The verification problem is then reduced to finding out the sign of the global minimum of this network. To find this global minimum, the authors present an approach based on Branch and Bound paradigm.  They also show how verification methods based on Satisfiability Modulo Theory (SMT) fit in this framework. A generic branch and bound based algorithm is presented to find a global minimum for the verification problem. The authors also show how some of the published works for NN verification based on SMT theory (like Reluplex by Katz et.al and Planet by Ehlers et.al) can be converted to branch and bound framework for verification. With this unified framework, the authors were able to come up with many promising suggestions to improve the speed-up of verification algorithms which they include in their proposed algorithm. They evaluate their method against SMT based methods like Reluplex and Planet, MIP solvers based like MIPplanet. They use Collision Detection, Airborne Collision Avoidance System (ACAS) and PCAMNIST as their datasets for evaluation. PCAMNIST is a novel dataset introduced by the authors to understand the factors that influence various verification methods.   The authors observe that on the CollisionDectection dataset most of the solvers succeeded within 10s. In particular, they found SMT based solvers to be extremely fast on this dataset. On ACAS, most of the solvers could not verify within the timelimit of 2 hours. However, their method was able to achieve 98.40% within an hour as compared to the baseline Reluplex which achieved only 79.26% success within the two hour limit.  In addition to the evaluation, the authors do an ablation study on what changes made the most impact in terms of performance on the methods that they proposed. They come up with the following conclusions on their study: a) Smart branching contributes significantly to the performance gap b) Branching over inputs rather than over activations does not contribute much improvement c) Better bounds contribute to the rest of the performance gap In their experiments, they also observe the following: a) Larger the number of inputs, harder is the verification problem b) Wider networks take more time to solve as they have more non-linearities c) Properties with large satisfiability margin are easy to prove Quality:  This paper proposes a novel framework for NN verification. They make a strong case on how this framework can be instrumental in bringing about rapid improvements in the performance of NN verifications. They provide thorough analysis on what makes their proposed algorithm perform better than the other state-of-the-art approaches. The amount of speed-up that their approach achieves is also significant. Though this approach shows promising results on smaller networks, it would be interesting to see how it scales on larger networks.  Overall, the quality of this paper is good.  Clarity: The paper is quite clear in presenting the contributions that it makes in the field of verification methods for neural networks. Their main idea has been illustrated with simple examples that are easy to understand. The results and conclusions have been presented well with graphs. However, in Section 5.1 Figure1(b), the y axis is not visible clearly.    Originality: The field of formal verification of Neural networks has emerged fairly recently during the last few years. Most of the published works so far have used either SMT theory or MIP formulation to solve the verification problem. To the best of my knowledge, there has been no study that proposes a unified framework for this problem. The authors present a unique and interesting approach that enables us to convert any SMT based verification method or MIP based verification method to a branch and bound based paradigm. This framework makes it easier to come up with solutions to improve the verification process as the authors demonstrate through the various experiments.   Significance: Deep neural networks are now increasingly becoming a major component of many safety-critical applications. Thus, formal verification of neural networks has become an important research problem that needs to be solved in order to scale deep neural networks in safety-critical applications. By proposing a unified framework for NN verification, this paper comes up with significant improvements in runtime for verification algorithms. It would be interesting for the research community to analyze this framework which might lead to even more efficient algorithms.       A few detailed comments:  In Section 5.1 Figure1(b), the y-axis is not visible clearly. In Figure 4. (c) The values on x-axis are not clearly visible.  Though this approach shows promising results on smaller networks, it would be good to include larger networks and observe how the algorithm scales. Although the authors in this work focus on piecewise-linear NN’s, adding a few lines as to the feasibility of scaling this framework to general Neural networks might be helpful in motivating other research groups to study this framework further.