Reviews: Efficient Formal Safety Analysis of 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.