ShanghaiTech University Knowledge Management System
Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks | |
2022-07-02 | |
状态 | 已发表 |
摘要 | As a new programming paradigm, deep neural networks (DNNs) have been increasingly deployed in practice, but the lack of robustness hinders their applications in safety-critical domains. While there are techniques for verifying DNNs with formal guarantees, they are limited in scalability and accuracy. In this paper, we present a novel abstraction-refinement approach for scalable and exact DNN verification. Specifically, we propose a novel abstraction to break down the size of DNNs by over-approximation. The result of verifying the abstract DNN is always conclusive if no spurious counterexample is reported. To eliminate spurious counterexamples introduced by abstraction, we propose a novel counterexample-guided refinement that refines the abstract DNN to exclude a given spurious counterexample while still over-approximating the original one. Our approach is orthogonal to and can be integrated with many existing verification techniques. For demonstration, we implement our approach using two promising and exact tools Marabou and Planet as the underlying verification engines, and evaluate on widely-used benchmarks ACAS Xu, MNIST and CIFAR-10. The results show that our approach can boost their performance by solving more problems and reducing up to 86.3% and 78.0% verification time, respectively. Compared to the most relevant abstraction-refinement approach, our approach is 11.6-26.6 times faster. |
DOI | arXiv:2207.00759 |
相关网址 | 查看原文 |
出处 | Arxiv |
WOS记录号 | PPRN:12204412 |
WOS类目 | Computer Science, Artificial Intelligence ; Computer Science, Software Engineering |
文献类型 | 预印本 |
条目标识符 | https://kms.shanghaitech.edu.cn/handle/2MSLDSTB/348565 |
专题 | 信息科学与技术学院_PI研究组_宋富组 |
作者单位 | 1.Shenzhen Univ, Shenzhen, Peoples R China 2.ShanghaiTech Univ, Shanghai, Peoples R China |
推荐引用方式 GB/T 7714 | Liu, Jiaxiang,Xing, Yunhan,Shi, Xiaomu,et al. Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks. 2022. |
条目包含的文件 | ||||||
文件名称/大小 | 文献类型 | 版本类型 | 开放类型 | 使用许可 |
修改评论
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。