Write a Blog >>

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-of-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., our approach is two orders of magnitude faster and able to solve more verification tasks in the same time limit than the state-of-the-art methods.

Thu 13 Oct

Displayed time zone: Eastern Time (US & Canada) change

16:00 - 18:00
Technical Session 32 - Formal Methods and Models IITool Demonstrations / Journal-first Papers / Research Papers at Banquet B
Chair(s): Khouloud Gaaloul University of Michigan - Dearborn
CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory
Tool Demonstrations
Bernd Fischer Stellenbosch University, South Africa, Salvatore La Torre Università degli Studi di Salerno, Gennaro Parlato University of Molise, Peter Schrammel University of Sussex and Diffblue Ltd
Research paper
Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses
Research Papers
Elias Kuiter Otto-von-Guericke-University Magdeburg, Sebastian Krieter University of Ulm, Chico Sundermann University of Ulm, Thomas Thüm University of Ulm, Gunter Saake University of Magdeburg, Germany
A three-valued model abstraction framework for PCTL* stochastic model checkingVirtual
Journal-first Papers
Yang Liu Shanghai Maritime University/National University of Singapore, Yan Ma Nanjing University of Finance and Economics / National University of Singapore, Yongsheng Yang Shanghai Maritime University
File Attached
Research paper
Finding and Understanding Incompleteness Bugs in SMT SolversVirtual
Research Papers
Mauro Bringolf ETH Zurich, Dominik Winterer ETH Zurich, Zhendong Su ETH Zurich
Research paper
Checking LTL Satisfiability via End-to-end LearningVirtual
Research Papers
Weilin Luo School of Computer Science and Engineering, Sun Yat-sen University, Hai Wan School of Data and Computer Science, Sun Yat-sen University, Delong Zhang SUN YAT-SEN UNIVERSITY, Jianfeng Du Guangdong University of Foreign Studies, Hengdi Su SUN YAT-SEN UNIVERSITY
Research paper
QVIP: An ILP-based Formal Verification Approach for Quantized Neural NetworksVirtual
Research Papers
Yedi Zhang ShanghaiTech University, Zhe Zhao ShanghaiTech University, Guangke Chen ShanghaiTech University, Fu Song ShanghaiTech University, Min Zhang East China Normal University, Taolue Chen Birkbeck University of London, Jun Sun Singapore Management University