DNNV: A Framework for Deep Neural Network Verification

TL;DR

DNNV is a comprehensive framework that standardizes formats and provides tools to simplify the development, application, and comparison of deep neural network verifiers, addressing key challenges in the field.

Contribution

It introduces a unified framework with standardized formats and a DSL, improving verifier support and benchmarking consistency in DNN verification.

Findings

Support for existing benchmarks increased from 30% to 74%.

Standardized input/output formats facilitate verifier development.

A new DSL simplifies property specification.

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%.