Publication Type
Conference Proceeding Article
Version
acceptedVersion
Publication Date
10-2022
Abstract
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.
Keywords
Quantized neural network, formal verification, integer linear programming, robustness
Discipline
OS and Networks | Software Engineering
Research Areas
Information Systems and Management
Publication
Proceedings of 37th IEEE/ACM International Conference on Automated Software Engineering, Rochester, USA, 2022 October 10-14
First Page
1
Last Page
13
Identifier
10.1145/3551349.3556916
Publisher
ACM
City or Country
Rochester, USA
Citation
ZHANG, Yedi; ZHAO, Zhe; CHEN, Guangke; SONG, Fu; ZHANG, Min; CHEN, Taolue; and SUN, Jun.
QVIP: An ILP-based formal verification approach for quantized neural networks. (2022). Proceedings of 37th IEEE/ACM International Conference on Automated Software Engineering, Rochester, USA, 2022 October 10-14. 1-13.
Available at: https://ink.library.smu.edu.sg/sis_research/7281
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
http://doi.org/10.1145/3551349.3556916