Towards Efficient Verification of Quantized Neural Networks
Quantization replaces floating point arithmetic with integer arithmetic in deep neural network models, providing more efficient on-device inference with less power and memory. In this work, we propose a framework for formally verifying properties of quantized neural networks. Our baseline technique is based on integer linear programming which guarantees both soundness and completeness. We then show how efficiency can be improved by utilizing gradient-based heuristic search methods and also bound-propagation techniques. We evaluate our approach on perception networks quantized with PyTorch. Our results show that we can verify quantized networks with better scalability and efficiency than the previous state of the art.
Code (1)
Tasks
Heuristic SearchQuantizationSimilar Papers 제목 키워드 기반
Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable
We introduce a logical language for reasoning about quantized aggregate-combine graph neural networks with global readout (ACR-GNNs). We provide a logical characterization and use it to prove that verification tasks for …
Scalable Verification of Quantized Neural Networks (Technical Report)
Formal verification of neural networks is an active topic of research, and recent advances have significantly increased the size of the networks that verification tools can handle. However, most methods are designed for …
Computational EfficiencyQuantizationQEBVerif: Quantization Error Bound Verification of Neural Networks
To alleviate the practical constraints for deploying deep neural networks (DNNs) on edge devices, quantization is widely regarded as one promising technique. It reduces the resource requirements for computational power a…
QuantizationVerifying Quantized Graph Neural Networks is PSPACE-complete
In this paper, we investigate verification of quantized Graph Neural Networks (GNNs), where some fixed-width arithmetic is used to represent numbers. We introduce the linear-constrained validity (LVP) problem for verifyi…
TranslationQVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks
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 pra…
Quantization