一句话：提出增量且完备的 DNN 验证框架与工具 IVAN，避免网络更新后从头验证并显著加速。
深度神经网络（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.
@article{paperbot1946,
title = {Incremental Verification of Neural Networks},
author = {Shubham Ugare and Debangshu Banerjee and Sasa Misailovic and Gagandeep Singh},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591299}
}