Complete verification of deep neural networks (DNNs) can exactly determine whether the DNN satisfies a desired trustworthy property (e.g., robustness, fairness) on an infinite set of inputs or not. Despite the tremendous progress to improve the scalability of complete verifiers over the years on individual DNNs, they are inherently inefficient when a deployed DNN is updated to improve its inference speed or accuracy. The inefficiency is because the expensive verifier needs to be run from scratch on the updated DNN. To improve efficiency, we propose a new, general framework for incremental and complete DNN verification based on the design of novel theory, data structure, and algorithms. Our contributions implemented in a tool named IVAN yield an overall geometric mean speedup of 2.4x for verifying challenging MNIST and CIFAR10 classifiers and a geometric mean speedup of 3.8x for the ACAS-XU classifiers over the state-of-the-art baselines.

翻译：深度神经网络（DNN）的完全验证能够精确判定该网络在无限输入集上是否满足期望的可信属性（如鲁棒性、公平性）。尽管多年来针对单个DNN的完全验证器在可扩展性方面取得了巨大进步，但当已部署的DNN为提升推理速度或准确率而更新时，现有方法本质上是低效的——因为昂贵的验证器需要在更新后的DNN上从头运行。为解决此效率问题，我们提出一种基于新型理论、数据结构与算法设计的通用增量式完全DNN验证框架。基于该框架实现的工具IVAN，在验证具有挑战性的MNIST与CIFAR10分类器时，总体几何平均加速比达2.4倍；在验证ACAS-XU分类器时，相比当前最优基线方法获得3.8倍的几何平均加速比。