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验证通用框架。基于该框架实现的工具IVAN，在最具挑战性的MNIST与CIFAR10分类器验证任务上取得2.4倍几何平均加速比，在ACAS-XU分类器验证任务上较当前最优基线方法实现3.8倍几何平均加速比。