DNNV: A Framework for Deep Neural Network Verification
arXiv:2105.12841 · doi:10.1007/978-3-030-81685-8_6
Abstract
Despite the large number of sophisticated deep neural network (DNN) verification algorithms, DNN verifier developers, users, and researchers still face several challenges. First, verifier developers must contend with the rapidly changing DNN field to support new DNN operations and property types. Second, verifier users have the burden of selecting a verifier input format to specify their problem. Due to the many input formats, this decision can greatly restrict the verifiers that a user may run. Finally, researchers face difficulties in re-using benchmarks to evaluate and compare verifiers, due to the large number of input formats required to run different verifiers. Existing benchmarks are rarely in formats supported by verifiers other than the one for which the benchmark was introduced. In this work we present DNNV, a framework for reducing the burden on DNN verifier researchers, developers, and users. DNNV standardizes input and output formats, includes a simple yet expressive DSL for specifying DNN properties, and provides powerful simplification and reduction operations to facilitate the application, development, and comparison of DNN verifiers. We show how DNNV increases the support of verifiers for existing benchmarks from 30% to 74%.
References in corpus (9)
- End to End Learning for Self-Driving Cars
- Provable defenses against adversarial examples via the convex outer adversarial polytope
- Certified Defenses against Adversarial Examples
- Efficient Neural Network Robustness Certification with General Activation Functions
- Evaluating Robustness of Neural Networks with Mixed Integer Programming
- Formal Security Analysis of Neural Networks using Symbolic Intervals
- Efficient Formal Safety Analysis of Neural Networks
- Towards Fast Computation of Certified Robustness for ReLU Networks
- A Unified View of Piecewise Linear Neural Network Verification