一句话：提出差分跟踪与 DiffPoly 抽象域，实现高精度可扩展的 DNN 输入关系验证器 RaVeN。
论文关注深度神经网络（DNN）上的输入关系性质验证，如对通用对抗扰动的鲁棒性、单调性等。这类性质需要同时推理同一 DNN 的多次执行，而非单次执行的输入-输出约束，因此现有方法精度不足。作者提出“差分跟踪”（difference tracking）这一新概念，在每一层上计算同一 DNN 两次执行输出之间的差异，并为此设计新的抽象域 DiffPoly，使其能够扩展到大型网络。DiffPoly 配备了针对常见激活函数（ReLU、Tanh、Sigmoid 等）与仿射层的定制抽象变换器，可生成精确的跨执行线性约束。作者基于该抽象域与线性规划公式实现了验证器 RaVeN，可处理多种输入关系性质。在多个数据集、网络和性质的挑战性基准上，RaVeN 借助跨执行精确线性约束，精度显著优于基线方法。
We consider the verification of input-relational properties defined over deep neural networks (DNNs) such as robustness against universal adversarial perturbations, monotonicity, etc. Precise verification of these properties requires reasoning about multiple executions of the same DNN. We introduce a novel concept of difference tracking to compute the difference between the outputs of two executions of the same DNN at all layers. We design a new abstract domain, DiffPoly for efficient difference tracking that can scale large DNNs. DiffPoly is equipped with custom abstract transformers for common activation functions (ReLU, Tanh, Sigmoid, etc.) and affine layers and can create precise linear cross-execution constraints. We implement an input-relational verifier for DNNs called RaVeN which uses DiffPoly and linear program formulations to handle a wide range of input-relational properties. Our experimental results on challenging benchmarks show that by leveraging precise linear constraints defined over multiple executions of the DNN, RaVeN gains substantial precision over baselines on a wide range of datasets, networks, and input-relational properties.
@article{BanerjeeXS24,
title = {Input-Relational Verification of Deep Neural Networks},
author = {Debangshu Banerjee and Changming Xu and Gagandeep Singh},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656377}
}