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.

翻译：量化通过将深度神经网络模型中的浮点运算替换为整数运算，以更低的功耗和内存实现更高效的设备端推理。本文提出一种形式化验证量化神经网络属性的框架。基础技术基于整数线性规划，可同时保证可靠性与完备性。我们进一步展示如何利用基于梯度的启发式搜索方法与边界传播技术提升验证效率。在PyTorch框架下训练的感知网络量化模型上评估表明，相较于现有最优方法，本方法能实现更具可扩展性与高效性的量化网络验证。