DNNV: A Framework for Deep Neural Network Verification
DNNV: A Framework for Deep Neural Network Verification
复制标题
DOI：
10.1007/978-3-030-81685-8_6
复制
发表时间：
2021-05
期刊：
影响因子：
--
通讯作者：
David Shriver;Sebastian G. Elbaum;Matthew B. Dwyer
中科院分区：
文献类型：
--
作者：
David Shriver;Sebastian G. Elbaum;Matthew B. Dwyer
尽管有大量复杂的深度神经网络（DNN）验证算法，但DNN验证器的开发人员、用户和研究人员仍然面临着一些挑战。首先，验证器开发人员必须应对快速变化的DNN领域，以支持新的DNN操作和属性类型。其次，验证器用户有选择验证器输入格式来指定他们的问题的负担。由于有许多输入格式，这个决定会极大地限制用户可以运行的验证器。最后，研究人员面临的困难，重新使用基准评估和比较验证，由于大量的输入格式需要运行不同的验证。现有的基准测试很少采用被验证者支持的格式，除了引入基准测试的格式之外。在这项工作中，我们提出了DNNV，一个框架，用于减轻DNN验证器研究人员，开发人员和用户的负担。DNNV简化输入和输出格式，包括一个简单而富有表现力的DSL用于指定DNN属性，并提供强大的简化和减少操作，以促进DNN验证器的应用，开发和比较。我们展示了DNNV如何将验证器对现有基准的支持从30%提高到74%。
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.DNNVstandardizes 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%.