  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.
