两种近似的故事:通过欠近似收紧深度神经网络鲁棒性验证的过近似
机器学习
2023-05-29 v1 人工智能
摘要
深度神经网络(DNNs)的鲁棒性对宿主系统的可靠性和安全性至关重要。形式化验证已被证明能有效地提供可证明的鲁棒性保证。为提升其可扩展性,通过线性约束对DNN中的非线性激活函数进行过近似已被广泛采用,从而将验证问题转化为可高效求解的线性规划问题。许多研究致力于定义所谓的紧近似,以减少过近似带来的高估。本文中,我们研究现有方法并识别出定义紧近似的一个主导因素,即激活函数的近似域。我们发现,在近似域上定义的紧近似可能不如在其实际域上定义的紧近似紧,而现有方法都仅依赖于近似域。基于该观察,我们提出一种新颖的双重近似方法以收紧过近似,利用激活函数的欠估计域来定义紧近似边界。我们将该方法以基于蒙特卡洛模拟和梯度下降的两种互补算法实现到一个称为DualApp的工具中。我们在一个包含不同架构DNN的综合基准上对其评估。实验结果表明,DualApp显著优于最先进的方法,在已验证鲁棒性比例上提升100%–1000%,在认证下界上平均提升10.64%(最高达66.53%)。
引用
@article{arxiv.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},
journal= {arXiv preprint arXiv:2305.16998},
year = {2023}
}
备注
16 pages, 11 figures, 5 tables, ISSTA 2023. arXiv admin note: substantial text overlap with arXiv:2211.11186