QVIP: An ILP-based formal verification approach for quantized  neural networks

doi:10.1145/3551349.3556916

	QVIP: An ILP-based formal verification approach for quantized neural networks
	Zhang, Yedi1 ; Zhao, Zhe1 ; Chen, Guangke1 ; Song, Fu1 ; Zhang, Min 2; Chen, Taolue 3; Sun, Jun 4
	2022
会议录名称	PROCEEDINGS OF THE 37TH IEEE/ ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, ASE 2022
ISSN	1527-1366
发表状态	已发表
DOI	10.1145/3551349.3556916
摘要	Deep learning has become a promising programming paradigm in software development, owing to its surprising performance in solving many challenging tasks. Deep neural networks (DNNs) are increasingly being deployed in practice, but are limited on resource-constrained devices owing to their demand for computational power. Quantization has emerged as a promising technique to reduce the size of DNNs with comparable accuracy as their floating-point numbered counterparts. The resulting quantized neural networks (QNNs) can be implemented energy-efficiently. Similar to their floating-point numbered counterparts, quality assurance techniques for QNNs, such as testing and formal verification, are essential but are currently less explored. In this work, we propose a novel and efficient formal verification approach for QNNs. In particular, we are the first to propose an encoding that reduces the verification problem of QNNs into the solving of integer linear constraints, which can be solved using off-the-shelf solvers. Our encoding is both sound and complete. We demonstrate the application of our approach on local robustness verification and maximum robustness radius computation. We implement our approach in a prototype tool QVIP and conduct a thorough evaluation. Experimental results on QNNs with different quantization bits confirm the effectiveness and efficiency of our approach, e.g., two orders of magnitude faster and able to solve more verification tasks in the same time limit than the state-of-the-art methods.
关键词	Quantized neural network formal verification integer linear programming robustness
会议名称	37th IEEE/ACM International Conference on Automated Software Engineering (ASE)
出版地	1601 Broadway, 10th Floor, NEW YORK, NY, UNITED STATES
会议地点	Oakland Univ,null,MI
会议日期	OCT 10-14, 2022
URL	查看原文
收录类别	EI ; CPCI-S
语种	英语
资助项目	National Key Research Program[2020AAA0107800]
WOS研究方向	Automation & Control Systems ; Computer Science
WOS类目	Automation & Control Systems ; Computer Science, Software Engineering ; Computer Science, Theory & Methods
WOS记录号	WOS:001062775200024
出版者	ASSOC COMPUTING MACHINERY
引用统计	正在获取...
文献类型	会议论文
条目标识符	https://kms.shanghaitech.edu.cn/handle/2MSLDSTB/243463
专题	信息科学与技术学院_博士生信息科学与技术学院_PI研究组_宋富组
通讯作者	Song, Fu
作者单位	1.ShanghaiTech University 2.East China Normal University 3.Birkbeck, University of London 4.Singapore Management University
第一作者单位	上海科技大学
通讯作者单位	上海科技大学
第一作者的第一单位	上海科技大学
推荐引用方式 GB/T 7714	Zhang, Yedi,Zhao, Zhe,Chen, Guangke,et al. QVIP: An ILP-based formal verification approach for quantized neural networks[C]. 1601 Broadway, 10th Floor, NEW YORK, NY, UNITED STATES:ASSOC COMPUTING MACHINERY,2022.