2019/04/22 by Greg Anderson, Shankara Pailoor, Isil Dillig +1 · 1 voice
Computer Science · #cs.LG #cs.PL
paper · pdf · doi:10.1145/3314221.3314614
arxiv published 2019/04/22 · arxiv created 2019/05/01 · arxiv updated 2019/05/02
In recent years, the notion of local robustness (or robustness for short) has emerged as a desirable property of deep neural networks. Intuitively, robustness means that small perturbations to an input do not cause the network to perform misclassifications. In this paper, we present a novel algorithm for verifying robustness properties of neural networks. Our method synergistically combines gradient-based optimization methods for counterexample search with abstraction-based proof search to obtain a sound and (δ-)complete decision procedure. Our method also employs a data-driven approach to learn a verification policy that guides abstract interpretation during proof search. We have implemented the proposed approach in a tool called Charon and experimentally evaluated it on hundreds of benchmarks. Our experiments show that the proposed approach significantly outperforms three state-of-the-art tools, namely AI2 , Reluplex, and Reluval.