TY - CONF
AB - 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 bitexact implementation of quantized neural networks with bitvector 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.
AU - Henzinger, Thomas A
AU - Lechner, Mathias
AU - Zikelic, Dorde
ID - 10665
IS - 5A
SN - 2159-5399
T2 - Proceedings of the AAAI Conference on Artificial Intelligence
TI - Scalable verification of quantized neural networks
VL - 35
ER -