Neural networks are increasingly deployed in real-world safety-critical domains such as autonomous driving, aircraft collision avoidance, and malware detection. However, these networks have been shown to often mispredict on inputs with minor adversarial or even accidental perturbations. Consequences of such errors can be disastrous and even potentially fatal as shown by the recent Tesla autopilot crash. Thus, there is an urgent need for formal analysis systems that can rigorously check neural networks for violations of different safety properties such as robustness against adversarial perturbations within a certain L-norm of a given image. An effective safety analysis system for a neural network must be able to either ensure that a safety property is satisfied by the network or find a counterexample, i.e., an input for which the network will violate the property. Unfortunately, most existing techniques for performing such analysis struggle to scale beyond very small networks and the ones that can scale to larger networks suffer from high false positives and cannot produce concrete counterexamples in case of a property violation. In this paper, we present a new efficient approach for rigorously checking different safety properties of neural networks that significantly outperforms existing approaches by multiple orders of magnitude. Our approach can check different safety properties and find concrete counterexamples for networks that are 10x larger than the ones supported by existing analysis techniques. We believe that our approach to estimating tight output bounds of a network for a given input range can also help improve the explainability of neural networks and guide the training process of more robust neural networks.

The paper improves on previous methods for formal verification of neural network properties over small intervals, such as formally verifying resistance to Linf adversarial examples in a ball around one point at a time. The paper is a significant ( 1 OOM) improvement relative to previous work on this problem. I am somewhat unconvinced of the importance of this type of verification given that (1) these techniques provide absolute confidence about a tiny sliver of the possible attack space, (2) as-is they are many orders of magnitude too expensive to use at training time, and therefore not much of an improvement given that most networks do not satisfy even the safety properties these techniques can check, and (3) have little to no hope of scaling to interestingly sized networks such as ImageNet models. However, since this paper is an order of magnitude speed improvement relative to previous work, I am marginally in favor of setting those concerns aside and accepting it on speed merits. The paper proceeds by maintaining two types of bounds on every value in a relu network: a concrete interval bound and a linear interval bound whose lower and upper components are linear functions in terms of other values in the network.

Neural networks are increasingly deployed in real-world safety-critical domains such as autonomous driving, aircraft collision avoidance, and malware detection. However, these networks have been shown to often mispredict on inputs with minor adversarial or even accidental perturbations. Consequences of such errors can be disastrous and even potentially fatal as shown by the recent Tesla autopilot crash. Thus, there is an urgent need for formal analysis systems that can rigorously check neural networks for violations of different safety properties such as robustness against adversarial perturbations within a certain L-norm of a given image. An effective safety analysis system for a neural network must be able to either ensure that a safety property is satisfied by the network or find a counterexample, i.e., an input for which the network will violate the property.