Document Open Access Logo

Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees

Authors Guanqin Zhang , Kota Fukuda , Zhenya Zhang , H.M.N. Dilum Bandara , Shiping Chen , Jianjun Zhao , Yulei Sui

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.36.pdf
  • Filesize: 3.04 MB
  • 29 pages
HTML5 Logo HTML (experimental)
LIPIcs.ECOOP.2025.36.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Software and its engineering → Software testing and debugging
Keywords
  • neural network verification
  • branch and bound
  • counterexample potentiality
  • simulated annealing
  • stochastic optimization

Metrics

Abstract

The vulnerability of neural networks to adversarial perturbations has necessitated formal verification techniques that can rigorously certify the quality of neural networks. As the state-of-the-art, branch-and-bound (BaB) is a "divide-and-conquer" strategy that applies off-the-shelf verifiers to sub-problems for which they perform better. While BaB can identify the sub-problems that are necessary to be split, it explores the space of these sub-problems in a naive "first-come-first-served" manner, thereby suffering from an issue of inefficiency to reach a verification conclusion. To bridge this gap, we introduce an order over different sub-problems produced by BaB, concerning with their different likelihoods of containing counterexamples. Based on this order, we propose a novel verification framework Oliva that explores the sub-problem space by prioritizing those sub-problems that are more likely to find counterexamples, in order to efficiently reach the conclusion of the verification. Even if no counterexample can be found in any sub-problem, it only changes the order of visiting different sub-problems and so will not lead to a performance degradation. Specifically, Oliva has two variants, including Oliva^GR, a greedy strategy that always prioritizes the sub-problems that are more likely to find counterexamples, and Oliva^SA, a balanced strategy inspired by simulated annealing that gradually shifts from exploration to exploitation to locate the globally optimal sub-problems. We experimentally evaluate the performance of Oliva on 690 verification problems spanning over 5 models with datasets MNIST and CIFAR-10. Compared to the state-of-the-art approaches, we demonstrate the speedup of Oliva for up to 25× in MNIST, and up to 80× in CIFAR-10.

Cite As Get BibTex

Guanqin Zhang, Kota Fukuda, Zhenya Zhang, H.M.N. Dilum Bandara, Shiping Chen, Jianjun Zhao, and Yulei Sui. Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 36:1-36:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.36

Author Details

Guanqin Zhang
  • University of New South Wales, Sydney, Australia
  • CSIRO’s Data61, Sydney, Australia
Kota Fukuda
  • Kyushu University, Fukuoka, Japan
Zhenya Zhang
  • Kyushu University, Fukuoka, Japan
  • National Institute of Informatics, Tokyo, Japan
H.M.N. Dilum Bandara
  • CSIRO’s Data61, Sydney, Australia
  • University of New South Wales, Sydney, Australia
Shiping Chen
  • CSIRO’s Data61, Sydney, Australia
  • University of New South Wales, Sydney, Australia
Jianjun Zhao
  • Kyushu University, Fukuoka, Japan
Yulei Sui
  • University of New South Wales, Sydney, Australia

Funding

  • Zhang, Guanqin: CSIRO’s Data61 PhD Scholarship
  • Fukuda, Kota: JST BOOST Grant No. JPMJBS2406
  • Zhang, Zhenya: JST BOOST Grant No. JPMJBY24D7 and JSPS Grant No. JP25K21179
  • Zhao, Jianjun: JSPS KAKENHI Grant No. JP23H0337
  • Sui, Yulei: Australian Research Council Grants No. FT220100391 and No. DP250101396

Supplementary Materials

References

  1. Greg Anderson, Shankara Pailoor, Isil Dillig, and Swarat Chaudhuri. Optimization and abstraction: a synergistic approach for analyzing neural network robustness. In Proceedings of the 40th ACM SIGPLAN conference on programming language design and implementation, pages 731-744, 2019. URL: https://doi.org/10.1145/3314221.3314614.
  2. R Anderson, J Huchette, C Tjandraatmadja, and JP Vielma. Strong convex relaxations and mixed-integer programming formulations for trained neural networks (2018), 1811. Google Scholar
  3. Maksym Andriushchenko, Francesco Croce, Nicolas Flammarion, and Matthias Hein. Square attack: a query-efficient black-box adversarial attack via random search. In European conference on computer vision, pages 484-501. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58592-1_29.
  4. Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, and M. Pawan Kumar. Branch and bound for piecewise linear neural network verification. CoRR, abs/1909.06588, 2019. URL: https://doi.org/10.48550/arXiv.1909.06588.
  5. Rudy Bunel, P Mudigonda, Ilker Turkaslan, Philip Torr, Jingyue Lu, and Pushmeet Kohli. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21(2020), 2020. URL: https://jmlr.org/papers/v21/19-468.html.
  6. Nicholas Carlini and David Wagner. Towards evaluating the robustness of neural networks. In 2017 ieee symposium on security and privacy (sp), pages 39-57. Ieee, 2017. URL: https://doi.org/10.1109/SP.2017.49.
  7. Chih-Hong Cheng, Georg Nührenberg, and Harald Ruess. Maximum resilience of artificial neural networks. In Deepak D'Souza and K. Narayan Kumar, editors, Automated Technology for Verification and Analysis, pages 251-268. Springer Int. Publishing, 2017. URL: https://doi.org/10.1007/978-3-319-68167-2_18.
  8. Moumita Das, Rajarshi Ray, Swarup Kumar Mohalik, and Ansuman Banerjee. Fast falsification of neural networks using property directed testing. arXiv preprint arXiv:2104.12418, 2021. URL: https://doi.org/10.48550/arXiv.2104.12418.
  9. Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Uesato, Rudy R Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy S Liang, et al. Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming. Advances in Neural Information Processing Systems, 33:5318-5331, 2020. Google Scholar
  10. Alessandro De Palma, Rudy Bunel, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip HS Torr, and M Pawan Kumar. Improved branch and bound for neural network verification via lagrangian decomposition. arXiv preprint arXiv:2104.06718, 2021. Google Scholar
  11. Hai Duong, Linhan Li, ThanhVu Nguyen, and Matthew B. Dwyer. A DPLL(T) framework for verifying deep neural networks. CoRR, abs/2307.10266, 2023. URL: https://doi.org/10.48550/arXiv.2307.10266.
  12. Hai Duong, Dong Xu, ThanhVu Nguyen, and Matthew B Dwyer. Harnessing neuron stability to improve dnn verification. Proceedings of the ACM on Software Engineering, 1(FSE):859-881, 2024. URL: https://doi.org/10.1145/3643765.
  13. Krishnamurthy Dj Dvijotham, Robert Stanforth, Sven Gowal, Chongli Qin, Soham De, and Pushmeet Kohli. Efficient neural network verification with exactness characterization. In Uncertainty in artificial intelligence, pages 497-507. PMLR, 2020. Google Scholar
  14. Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In Automated Technology for Verification and Analysis: 15th Int. Symp., ATVA 2017, Proceedings 15, pages 269-286. Springer, October 2017. Google Scholar
  15. Mahyar Fazlyab, Manfred Morari, and George J Pappas. Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. IEEE Transactions on Automatic Control, 67(1):1-15, 2020. Google Scholar
  16. Claudio Ferrari, Mark Niklas Muller, Nikola Jovanovic, and Martin Vechev. Complete verification via multi-neuron relaxation guided branch-and-bound. arXiv preprint arXiv:2205.00263, 2022. URL: https://doi.org/10.48550/arXiv.2205.00263.
  17. Xiang Gao, Ripon K Saha, Mukul R Prasad, and Abhik Roychoudhury. Fuzz testing based data augmentation to improve robustness of deep neural networks. In Proceedings of the acm/ieee 42nd international conference on software engineering, pages 1147-1158, 2020. URL: https://doi.org/10.1145/3377811.3380415.
  18. Ian J. Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. In 3rd Int. Conf. on Learning Representations (ICLR'15), San Diego, CA, United States, 2015. Int. Conf. on Learning Representations, ICLR. Google Scholar
  19. Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2023. URL: https://www.gurobi.com.
  20. Karthik Hanumanthaiah and Samik Basu. Iterative counter-example guided robustness verification for neural networks. In International Symposium on AI Verification, pages 179-187. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65112-0_9.
  21. Patrick Henriksen and Alessio Lomuscio. Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis. In IJCAI, pages 2549-2555, 2021. URL: https://doi.org/10.24963/ijcai.2021/351.
  22. Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In Computer Aided Verification: 29th Int. Conf., CAV 2017, Part I 30, pages 3-29. Springer, July 2017. URL: https://doi.org/10.1007/978-3-319-63387-9_1.
  23. Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Rupak Majumdar and Viktor Kunčak, editors, Computer Aided Verification, pages 97-117. Springer Int. Publishing, 2017. URL: https://doi.org/10.1007/978-3-319-63387-9_5.
  24. Scott Kirkpatrick, C Daniel Gelatt Jr, and Mario P Vecchi. Optimization by simulated annealing. science, 220(4598):671-680, 1983. URL: https://doi.org/10.1126/science.220.4598.671.
  25. Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, Mykel J Kochenderfer, et al. Algorithms for verifying deep neural networks. Foundations and Trends® in Optimization, 4(3-4):244-404, 2021. URL: https://doi.org/10.1561/2400000035.
  26. Jingyue Lu and M Pawan Kumar. Neural network branching for neural network verification. arXiv preprint arXiv:1912.01329, 2019. URL: https://arxiv.org/abs/1912.01329.
  27. Zhongkui Ma, Jiaying Li, and Guangdong Bai. Relu hull approximation. Proceedings of the ACM on Programming Languages, 8(POPL):2260-2287, 2024. URL: https://doi.org/10.1145/3632917.
  28. Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. In 6th Int. Conf. on Learning Representations (ICLR'18), Vancouver, Canada, 2018. Google Scholar
  29. Christoph Müller, Gagandeep Singh, Markus Püschel, and Martin T Vechev. Neural network robustness verification on gpus. CoRR, abs/2007.10868, 2020. Google Scholar
  30. Mark Niklas Müller, Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T Johnson. 3rd international verification of neural networks competition (VNN-COMP 2022): Summary and results. arXiv preprint arXiv:2212.10376, 2022. URL: https://doi.org/10.48550/arXiv.2212.10376.
  31. Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. Precise multi-neuron abstractions for neural network certification. arXiv preprint arXiv:2103.03638, 2021. URL: https://arxiv.org/abs/2103.03638.
  32. Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. Prima: general and precise neural network certification via scalable convex hull approximations. ACM on Programming Languages, 6(POPL):1-33, 2022. URL: https://doi.org/10.1145/3498704.
  33. Augustus Odena, Catherine Olsson, David Andersen, and Ian Goodfellow. Tensorfuzz: Debugging neural networks with coverage-guided fuzzing. In International Conference on Machine Learning, pages 4901-4911. PMLR, 2019. URL: http://proceedings.mlr.press/v97/odena19a.html.
  34. Matan Ostrovsky, Clark Barrett, and Guy Katz. An abstraction-refinement approach to verifying convolutional neural networks. In International Symposium on Automated Technology for Verification and Analysis, pages 391-396. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-19992-9_25.
  35. Kexin Pei, Yinzhi Cao, Junfeng Yang, and Suman Jana. Deepxplore: Automated whitebox testing of deep learning systems. In 26th Symp. on Operating Systems Principles, pages 1-18, 2017. URL: https://doi.org/10.1145/3132747.3132785.
  36. Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for certifying robustness to adversarial examples. Advances in neural information processing systems, 31, 2018. Google Scholar
  37. Vicenc Rubies-Royo, Roberto Calandra, Dusan M Stipanovic, and Claire Tomlin. Fast neural network verification via shadow prices. arXiv preprint arXiv:1902.07247, 2019. URL: https://arxiv.org/abs/1902.07247.
  38. Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh, and Huan Zhang. Neural network verification with branch-and-bound for general nonlinearities. arXiv preprint arXiv:2405.21063, 2024. URL: https://doi.org/10.48550/arXiv.2405.21063.
  39. Zhouxing Shi, Yihan Wang, Huan Zhang, J Zico Kolter, and Cho-Jui Hsieh. Efficiently computing local lipschitz constants of neural networks via bound propagation. Advances in Neural Information Processing Systems, 35:2350-2364, 2022. Google Scholar
  40. Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. Advances in Neural Information Processing Systems, 32, 2019. Google Scholar
  41. Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. In Advances in Neural Information Processing Systems, volume 31, 2018. Google Scholar
  42. Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. Advances in neural information processing systems, 31, 2018. URL: https://proceedings.neurips.cc/paper/2018/hash/f2f446980d8e971ef3da97af089481c3-Abstract.html.
  43. Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Boosting robustness certification of neural networks. In Int. Conf. on learning representations, 2018. Google Scholar
  44. Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. ACM on Programming Languages, 3(POPL):1-30, 2019. URL: https://doi.org/10.1145/3290354.
  45. Yuchi Tian, Kexin Pei, Suman Jana, and Baishakhi Ray. Deeptest: Automated testing of deep-neural-network-driven autonomous cars. In 40th Int. Conf. on Software Engineering, pages 303-314, 2018. URL: https://doi.org/10.1145/3180155.3180220.
  46. Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Kishor Patel, and Juan Pablo Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. Advances in Neural Information Processing Systems, 33:21675-21686, 2020. Google Scholar
  47. Vincent Tjeng, Kai Y Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In Int. Conf. on Learning Representations, 2018. Google Scholar
  48. Shubham Ugare, Debangshu Banerjee, Sasa Misailovic, and Gagandeep Singh. Incremental verification of neural networks. ACM on Programming Languages, 7(PLDI):1920-1945, 2023. URL: https://doi.org/10.1145/3591299.
  49. Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. Advances in neural information processing systems, 31, 2018. URL: https://proceedings.neurips.cc/paper/2018/hash/2ecd2bd94734e5dd392d8678bc64cdab-Abstract.html.
  50. Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In 27th USENIX Security Symp. (USENIX Security 18), pages 1599-1614, 2018. URL: https://www.usenix.org/conference/usenixsecurity18/presentation/wang-shiqi.
  51. Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems, 34:29909-29921, 2021. URL: https://proceedings.neurips.cc/paper/2021/hash/fac7fead96dafceaf80c1daffeae82a4-Abstract.html.
  52. Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, and Clark W. Barrett. Marabou 2.0: A versatile formal analyzer of neural networks. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II, volume 14682 of Lecture Notes in Computer Science, pages 249-264. Springer, Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65630-9_13.
  53. Cihang Xie, Zhishuai Zhang, Yuyin Zhou, Song Bai, Jianyu Wang, Zhou Ren, and Alan L Yuille. Improving transferability of adversarial examples with input diversity. In Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, pages 2730-2739, 2019. URL: https://doi.org/10.1109/CVPR.2019.00284.
  54. Xiaoyong Xue, Xiyue Zhang, and Meng Sun. kprop: Multi-neuron relaxation method for neural network robustness verification. In International Conference on Fundamentals of Software Engineering, pages 142-156. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-42441-0_11.
  55. Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue, and Lijun Zhang. Improving neural network verification through spurious region guided refinement. In Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, pages 389-408. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72016-2_21.
  56. Yang Yu, Hong Qian, and Yi-Qi Hu. Derivative-free optimization via classification. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 30, 2016. URL: https://doi.org/10.1609/aaai.v30i1.10289.
  57. Guanqin Zhang, Zhenya Zhang, H.M.N. Dilum Bandara, Shiping Chen, Jianjun Zhao, and Yulei Sui. Efficient incremental verification of neural networks guided by counterexample potentiality. Proc. ACM Program. Lang., 9(OOPSLA1), April 2025. URL: https://doi.org/10.1145/3720417.
  58. Huan Zhang, Shiqi Wang, Kaidi Xu, Yihan Wang, Suman Jana, Cho-Jui Hsieh, and Zico Kolter. A branch and bound framework for stronger adversarial attacks of relu networks. In International Conference on Machine Learning, pages 26591-26604. PMLR, 2022. URL: https://proceedings.mlr.press/v162/zhang22ae.html.
  59. Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. Advances in Neural Information Processing Systems, 31, 2018. URL: https://proceedings.neurips.cc/paper/2018/hash/d04863f100d59b3eb688a11f95b0ae60-Abstract.html.
  60. Zhe Zhao, Yedi Zhang, Guangke Chen, Fu Song, Taolue Chen, and Jiaxiang Liu. Cleverest: accelerating cegar-based neural network verification via adversarial attacks. In International Static Analysis Symposium, pages 449-473. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-22308-2_20.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact