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量化的感知网络上评估了所提方法。结果表明，与现有最优技术相比，本方案在量化网络验证中具有更好的可扩展性和效率。