Improving Scalability of DNN Verification via Abstraction

Diganta Mukhopadhyay

Masaryk University

Due to advances in deep learning several problems that were previously considered intractable, like language modelling and image classification, can now be solved by training Deep Neural Networks (DNNs) on appropriate datasets. However, these DNNs have been shown to lack robusness and be vulnerable to adversarial attacks [13,5]. Due to this, DNNs still only find limited applicability in safety critical domains such as medical imaging and autonomous vehicles. This is because even plausible real-world inputs can be adversarial for the DNN being deployed, and lead to a safety violation [7]. Therefore, before a DNN can be deployed to a safety critical setting, it is necessary to provide formal guarantees that the DNN is not vulnerable to adversarial attacks that may lead to safety violations.

One way to provide such guarantees is via Formal Verification, and the community has developed several algorithms and solvers to formally verify safety properties for DNNs [9]. However, scalability of these methods to large DNNs remains a challenge. Inspired by the extensive use of abstraction in other areas within formal methods [3], and the intuition that to argue safety of a given DNN one may not need to analyise its behavior in complete detail, a line of work has attempted to solve this scalability issue via abstraction [6,4,14,1,2,11,8,12,10]. Specifically, these techniques reduce the given DNN and safety property pair to an abstract DNN by combining neurons within the given DNN, such that if the abstract DNN is safe, one can derive that the original DNN must also be safe. This abstract DNN then may be verified using any existing solver. In this talk, I will begin by introducing DNN Abstraction by providing an overview of existing work. Then, I will describe the work I am currently doing in collaboration with Yizhak Elboher and Prof. Jan Kretinsky to extend the existing techniques to new kinds of neural networks. Finally, I will discuss open directions for future research.

  1. Ashok, P., Hashemi, V., Kretínský, J., Mohr, S.: Deepabstract: Neural network abstraction for accelerating verification. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12302, pp. 92–107. Springer (2020)

  2. Chau, C., Kretínský, J., Mohr, S.: Syntactic vs semantic linear abstraction and refinement of neural networks. In: André, É., Sun, J. (eds.) Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14215, pp. 401–421. Springer (2023)

  3. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J.ACM 50(5), 752–794 (2003)

  4. Cohen, E., Elboher, Y.Y., Barrett, C.W., Katz, G.: Tighter abstract queries in neural network verification. In: Piskac, R., Voronkov, A. (eds.) LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023. EPiC Series in Computing, vol. 94, pp. 124–143. EasyChair (2023)

  5. Costa, J.C., Roxo, T., Proença, H., Inácio, P.R.M.: How deep learning sees the world: A survey on adversarial attacks & defenses. IEEE Access 12, 61113–61136 (2024).

  6. Elboher, Y.Y., Gottschlich, J., Katz, G.: An abstraction-based framework for neural network verification. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12224, pp. 43–65. Springer (2020)

  7. Eykholt, K., Evtimov, I., Fernandes, E., Li, B., Rahmati, A., Xiao, C., Prakash, A., Kohno, T., Song, D.: Robust physical-world attacks on deep learning visual classification. In: 2018 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2018, Salt Lake City, UT, USA, June 18-22, 2018. pp. 1625–1634. Computer Vision Foundation / IEEE Computer Society (2018).

  8. Kanav, S., Kretínský, J., Rieder, S.: A literature review on verification and abstraction of neural networks within the formal methods community. In: Jansen, N., Junges, S., Kaminski, B.L., Matheja, C., Noll, T., Quatmann, T., Stoelinga, M., Volk, M. (eds.) Principles of Verification: Cycling the Probabilistic Landscape – Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III. pp. 39–65. Lecture Notes in Computer Science, Springer (2024).

  9. Kaulen, K., Ladner, T., Bak, S., Brix, C., Duong, H., Flinkow, T., Johnson, T.T., Koller, L., Manino, E., Nguyen, T.H., Wu, H.: The 6th international verification of neural networks competition (VNN-COMP 2025): Summary and results. CoRR abs/2512.19007 (2025).

  10. Mukhopadhyay, D., Siddiqui, S., Karmarkar, H., Madhukar, K., Katz, G.: Learning DNN abstractions using gradient descent. In: Filkov, V., Ray, B., Zhou, M. (eds.) Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE 2024, Sacramento, CA, USA, October 27 - November 1, 2024. pp. 2299–2303. ACM (2024).

  11. Ostrovsky, M., Barrett, C.W., Katz, G.: An abstraction-refinement approach to verifying convolutional neural networks. In: Bouajjani, A., Holík, L., Wu, Z. (eds.) Automated Technology for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13505, pp. 391–396. Springer (2022)

  12. Siddiqui, S., Mukhopadhyay, D., Afzal, M., Karmarkar, H., Madhukar, K.: Unifying syntactic and semantic abstractions for deep neural networks. In: Haxthausen, A.E., Serwe, W. (eds.) Formal Methods for Industrial Critical Systems - 29th International Conference, FMICS 2024, Milan, Italy, September 9-11, 2024, Proceedings. pp. 201–219. Lecture Notes in Computer Science, Springer (2024).

  13. Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I.J., Fergus, R.: Intriguing properties of neural networks. In: Bengio, Y., LeCun, Y. (eds.) 2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Conference Track Proceedings (2014).

  14. Zhao, Z., Zhang, Y., Chen, G., Song, F., Chen, T., Liu, J.: CLEVEREST: accelerating cegar-based neural network verification via adversarial attacks. In: Singh, G., Urban, C. (eds.) Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5-7, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13790, pp. 449–473. Springer (2022)