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 and storage space by quantizing the weights and/or activation tensors of a DNN into lower bit-width fixed-point numbers, resulting in quantized neural networks (QNNs). While it has been empirically shown to introduce minor accuracy loss, critical verified properties of a DNN might become invalid once quantized. Existing verification methods focus on either individual neural networks (DNNs or QNNs) or quantization error bound for partial quantization. In this work, we propose a quantization error bound verification method, named QEBVerif, where both weights and activation tensors are quantized. QEBVerif consists of two parts, i.e., a differential reachability analysis (DRA) and a mixed-integer linear programming (MILP) based verification method. DRA performs difference analysis between the DNN and its quantized counterpart layer-by-layer to compute a tight quantization error interval efficiently. If DRA fails to prove the error bound, then we encode the verification problem into an equivalent MILP problem which can be solved by off-the-shelf solvers. Thus, QEBVerif is sound, complete, and reasonably efficient. We implement QEBVerif and conduct extensive experiments, showing its effectiveness and efficiency.

翻译：为缓解深度神经网络在边缘设备上部署的实际限制，量化被广泛视为一种有前景的技术。它通过将深度神经网络的权重和/或激活张量量化为更低比特宽度的定点数，从而降低计算能力和存储空间的资源需求，最终形成量化神经网络。尽管经验表明这仅会引入微小的精度损失，但深度神经网络的已验证关键属性在量化后可能失效。现有验证方法要么针对单一神经网络（深度神经网络或量化神经网络），要么针对部分量化的量化误差界限。本文提出一种名为QEBVerif的量化误差界限验证方法，其中权重和激活张量均被量化。QEBVerif由两部分组成：差分可达性分析和基于混合整数线性规划的验证方法。差分可达性分析通过逐层计算深度神经网络与其量化版本之间的差分，高效地推导出紧致的量化误差区间。若差分可达性分析无法证明误差界限，则将验证问题编码为等价的混合整数线性规划问题，并借助现成求解器求解。因此，QEBVerif具有完备性、合理性和较高效率。我们实现了QEBVerif并通过大量实验验证了其有效性与高效性。