  Formal verification of neural networks is an active topic of research, and
recent advances have significantly increased the size of the networks that
verification tools can handle. However, most methods are designed for
verification of an idealized model of the actual network which works over real
arithmetic and ignores rounding imprecisions. This idealization is in stark
contrast to network quantization, which is a technique that trades numerical
precision for computational efficiency and is, therefore, often applied in
practice. Neglecting rounding errors of such low-bit quantized neural networks
has been shown to lead to wrong conclusions about the network's correctness.
Thus, the desired approach for verifying quantized neural networks would be one
that takes these rounding errors into account. In this paper, we show that
verifying the bit-exact implementation of quantized neural networks with
bit-vector specifications is PSPACE-hard, even though verifying idealized
real-valued networks and satisfiability of bit-vector specifications alone are
each in NP. Furthermore, we explore several practical heuristics toward closing
the complexity gap between idealized and bit-exact verification. In particular,
we propose three techniques for making SMT-based verification of quantized
neural networks more scalable. Our experiments demonstrate that our proposed
methods allow a speedup of up to three orders of magnitude over existing
approaches.
