一句话：提出双重近似方法，利用激活函数的下近似域收紧线性过近似，提升 DNN 鲁棒性验证的紧致度与可扩展性。
DNN 鲁棒性的形式验证能提供可证明的保证，但非线性激活的线性过近似会引入过估。已有工作多基于近似域定义最紧线性界，本文指出近似域是决定紧致度的主导因素，并发现基于近似域的紧界在激活函数实际域上未必足够紧。为此，作者提出双重近似方法：利用激活函数被低估的下近似域来定义更紧的过近似界。该方法以 Monte Carlo 模拟和梯度下降两种互补算法实现，并集成到工具 DualApp 中。在覆盖多种 DNN 架构的综合基准上，DualApp 显著优于现有最先进方法：验证鲁棒比例提升 100%–1000%，认证下界平均提升 10.64%，最高提升 66.53%。
The robustness of deep neural networks (DNNs) is crucial to the hosting system’s reliability and security. Formal verification has been demonstrated to be effective in providing provable robustness guarantees. To improve its scalability, over-approximating the non-linear activation functions in DNNs by linear constraints has been widely adopted, which transforms the verification problem into an efficiently solvable linear programming problem. Many efforts have been dedicated to defining the so-called tightest approximations to reduce overestimation imposed by over-approximation. In this paper, we study existing approaches and identify a dominant factor in defining tight approximation, namely the approximation domain of the activation function. We find out that tight approximations defined on approximation domains may not be as tight as the ones on their actual domains, yet existing approaches all rely only on approximation domains. Based on this observation, we propose a novel dual-approximation approach to tighten overapproximations, leveraging an activation function’s underestimated domain to define tight approximation bounds. We implement our approach with two complementary algorithms based respectively on Monte Carlo simulation and gradient descent into a tool called DualApp. We assess it on a comprehensive benchmark of DNNs with different architectures. Our experimental results show that DualApp significantly outperforms the state-of-the-art approaches with 100% − 1000% improvement on the verified robustness ratio and 10.64% on average (up to 66.53%) on the certified lower bound.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2305-16998,
title = {A Tale of Two Approximations: Tightening Over-Approximation for DNN Robustness Verification via Under-Approximation},
author = {Zhiyi Xue and Si Liu and Zhaodi Zhang and Yiting Wu and Min Zhang},
booktitle = {ISSTA},
year = {2023},
doi = {10.1145/3597926.3598127}
}