Scalable verification of quantized neural networks

conference paper Scalable verification of quantized neural networks Technical Tracks published yes Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000-0002-2985-7724 Mathias Lechner author 3DC22916-F248-11E8-B48F-1D18A9856A87 Dorde Zikelic author 294AA7A6-F248-11E8-B48F-1D18A9856A870000-0002-4681-1699 GradSch department ToHe department AAAI: Association for the Advancement of Artificial Intelligence International IST Doctoral Program project Formal methods for the design and analysis of complex systems project Formal Methods for Stochastic Models: Algorithms and Applications project 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. https://research-explorer.ista.ac.at/download/10665/10684/16496-Article Text-19990-1-2-20210518 (1).pdf application/pdfno AAAI Press2021Virtual eng Proceedings of the AAAI Conference on Artificial Intelligence 2159-5399 2374-3468 978-1-57735-866-4 2012.08185 355A3787-3795 https://research-explorer.ista.ac.at/record/11362 T.A. Henzinger, M. Lechner, D. Zikelic, in:, Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press, 2021, pp. 3787–3795. Henzinger, Thomas A., et al. “Scalable Verification of Quantized Neural Networks.” Proceedings of the AAAI Conference on Artificial Intelligence, vol. 35, no. 5A, AAAI Press, 2021, pp. 3787–95. T. A. Henzinger, M. Lechner, and D. Zikelic, “Scalable verification of quantized neural networks,” in Proceedings of the AAAI Conference on Artificial Intelligence, Virtual, 2021, vol. 35, no. 5A, pp. 3787–3795. Henzinger, Thomas A, Mathias Lechner, and Dorde Zikelic. “Scalable Verification of Quantized Neural Networks.” In Proceedings of the AAAI Conference on Artificial Intelligence, 35:3787–95. AAAI Press, 2021. Henzinger, T. A., Lechner, M., & Zikelic, D. (2021). Scalable verification of quantized neural networks. In Proceedings of the AAAI Conference on Artificial Intelligence (Vol. 35, pp. 3787–3795). Virtual: AAAI Press. Henzinger TA, Lechner M, Zikelic D. Scalable verification of quantized neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence. Vol 35. AAAI Press; 2021:3787-3795. Henzinger TA, Lechner M, Zikelic D. 2021. Scalable verification of quantized neural networks. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Association for the Advancement of Artificial Intelligence, Technical Tracks, vol. 35, 3787–3795. 106652022-01-25T15:15:02Z2026-04-07T14:21:58Z