Incremental Verification of Neural Networks
Incremental Verification of Neural Networks
复制标题
DOI：
10.1145/3591299
复制
发表时间：
2023-04
影响因子：
--
通讯作者：
Shubham Ugare;Debangshu Banerjee;Sasa Misailovic;Gagandeep Singh
中科院分区：
文献类型：
--
作者：
Shubham Ugare;Debangshu Banerjee;Sasa Misailovic;Gagandeep Singh
深度神经网络(DNN)的完全验证可以准确地确定DNN在无限输入集上是否满足期望的可信性质(例如，稳健性、公平性)。尽管多年来在提高单个DNN上的完整验证器的可伸缩性方面取得了巨大的进步，但当更新已部署的DNN以提高其推理速度或准确性时，它们固有地效率低下。效率低下是因为昂贵的验证器需要在更新后的DNN上从头开始运行。为了提高验证效率，我们在设计新的理论、数据结构和算法的基础上，提出了一种新的、通用的增量式、完备式DNN验证框架。我们的贡献在一个名为Ivan的工具中实现，在验证具有挑战性的MNIST和CIFAR10分类器时，总体几何平均加速比为2.4倍，在最先进的基线上，ACAS-XU分类器的几何平均加速比为3.8倍。
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.