Towards Efficient Verification of Quantized Neural Networks

TL;DR

This paper introduces a formal verification framework for quantized neural networks that improves scalability and efficiency over previous methods, enabling more reliable on-device AI applications.

Contribution

It presents a novel verification approach combining integer linear programming with heuristic search and bound-propagation techniques for quantized neural networks.

Findings

Verified quantized networks with improved scalability

Achieved more efficient verification than previous state-of-the-art methods

Demonstrated effectiveness on PyTorch-quantized perception networks

Abstract

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.