  We present a new approach to assessing the robustness of neural networks
based on estimating the proportion of inputs for which a property is violated.
Specifically, we estimate the probability of the event that the property is
violated under an input model. Our approach critically varies from the formal
verification framework in that when the property can be violated, it provides
an informative notion of how robust the network is, rather than just the
conventional assertion that the network is not verifiable. Furthermore, it
provides an ability to scale to larger networks than formal verification
approaches. Though the framework still provides a formal guarantee of
satisfiability whenever it successfully finds one or more violations, these
advantages do come at the cost of only providing a statistical estimate of
unsatisfiability whenever no violation is found. Key to the practical success
of our approach is an adaptation of multi-level splitting, a Monte Carlo
approach for estimating the probability of rare events, to our statistical
robustness framework. We demonstrate that our approach is able to emulate
formal verification procedures on benchmark problems, while scaling to larger
networks and providing reliable additional information in the form of accurate
estimates of the violation probability.
