MpBP: verifying robustness of neural networks with multi-path bound propagation
Authors: 
Ye Zheng, 
Jiaxiang Liu, Xiaomu ShiAuthors Info & Claims
Pages 1692 - 1696
Abstract
Robustness of neural networks need be guaranteed in many safety-critical scenarios, such as autonomous driving and cyber-physical controlling. In this paper, we present MpBP, a tool for verifying the robustness of neural networks. MpBP is inspired by classical bound propagation methods for neural network verification, and aims to improve the effectiveness by exploiting the notion of propagation paths. Specifically, MpBP extends classical bound propagation methods, including forward bound propagation, backward bound propagation, and forward+backward bound propagation, with multiple propagation paths. MpBP is based on the widely-used PyTorch machine learning framework, hence providing efficient parallel verification on GPUs and user-friendly usage. We evaluate MpBP on neural networks trained on standard datasets MNIST, CIFAR-10 and Tiny ImageNet. The results demonstrate the effectiveness advantage of MpBP beyond two state-of-the-art bound propagation tools LiRPA and GPUPoly, with comparable efficiency to LiRPA and significantly higher efficiency than GPUPoly. A video demonstration that showcases the main features of MpBP can be found at https://youtu.be/3KyPMuPpfR8. Source code is available at https://github.com/formes20/MpBP and https://doi.org/10.5281/zenodo.7029261.
References
[1]
2012. Deep Neural Networks for Acoustic Modeling in Speech Recognition: The Shared Views of Four Research Groups. IEEE Signal Process. Mag., 29, 6 (2012), 82–97. https://doi.org/10.1109/MSP.2012.2205597
[2]
2021. 2nd International Verification of Neural Networks Competition (VNN-COMP’21). https://sites.google.com/view/vnn2021
[3]
2022. alpha-beta-CROWN: A Fast and Scalable Neural Network Verifier with Efficient Bound Propagation. https://github.com/huanzhang12/alpha-beta-CROWN
[4]
2022. PyTorch. https://pytorch.org/
[5]
2022. Tiny ImageNet. http://cs231n.stanford.edu/tiny-imagenet-200.zip
[6]
Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma. 2020. Strong mixed-integer programming formulations for trained neural networks. Math. Program., 183, 1 (2020), 3–39. https://doi.org/10.1007/s10107-020-01474-5
[7]
Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, and Ruth Misener. 2020. Efficient Verification of ReLU-Based Neural Networks via Dependency Analysis. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020. AAAI Press, 3291–3299. https://ojs.aaai.org/index.php/AAAI/article/view/5729
[8]
Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, and M. Pawan Kumar. 2020. Branch and Bound for Piecewise Linear Neural Network Verification. J. Mach. Learn. Res., 21 (2020), 42:1–42:39. http://jmlr.org/papers/v21/19-468.html
[9]
Rüdiger Ehlers. 2017. Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks. In Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings, Deepak D’Souza and K. Narayan Kumar (Eds.) (Lecture Notes in Computer Science, Vol. 10482). Springer, 269–286. https://doi.org/10.1007/978-3-319-68167-2_19
[10]
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin T. Vechev. 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA. IEEE Computer Society, 3–18. https://doi.org/10.1109/SP.2018.00058
[11]
Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017. Safety Verification of Deep Neural Networks. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, Rupak Majumdar and Viktor Kuncak (Eds.) (Lecture Notes in Computer Science, Vol. 10426). Springer, 3–29. https://doi.org/10.1007/978-3-319-63387-9_1
[12]
Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, Rupak Majumdar and Viktor Kuncak (Eds.) (Lecture Notes in Computer Science, Vol. 10426). Springer, 97–117. https://doi.org/10.1007/978-3-319-63387-9_5
[13]
Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, and Clark W. Barrett. 2019. The Marabou Framework for Verification and Analysis of Deep Neural Networks. In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, Isil Dillig and Serdar Tasiran (Eds.) (Lecture Notes in Computer Science, Vol. 11561). Springer, 443–452. https://doi.org/10.1007/978-3-030-25540-4_26
[14]
Alex Krizhevsky and Geoffrey Hinton. 2009. Learning multiple layers of features from tiny images.
[15]
SRI Lab. 2022. ETH Robustness Analyzer for Neural Networks (ERAN). https://github.com/eth-sri/eran
[16]
Yann LeCun. 1998. The MNIST database of handwritten digits. http://yann.lecun.com/exdb/mnist/
[17]
Geert Litjens, Thijs Kooi, Babak Ehteshami Bejnordi, Arnaud Arindra Adiyoso Setio, Francesco Ciompi, Mohsen Ghafoorian, Jeroen A. W. M. van der Laak, Bram van Ginneken, and Clara I. Sánchez. 2017. A survey on deep learning in medical image analysis. Medical Image Anal., 42 (2017), 60–88. https://doi.org/10.1016/j.media.2017.07.005
[18]
Matthew Mirman, Timon Gehr, and Martin T. Vechev. 2018. Differentiable Abstract Interpretation for Provably Robust Neural Networks. In Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsmässan, Stockholm, Sweden, July 10-15, 2018, Jennifer G. Dy and Andreas Krause (Eds.) (Proceedings of Machine Learning Research, Vol. 80). PMLR, 3575–3583. http://proceedings.mlr.press/v80/mirman18b.html
[19]
Christoph Müller, François Serre, Gagandeep Singh, Markus Püschel, and Martin T. Vechev. 2021. Scaling Polyhedral Neural Network Verification on GPUs. In Proceedings of Machine Learning and Systems 2021, MLSys 2021, virtual, April 5-9, 2021, Alex Smola, Alex Dimakis, and Ion Stoica (Eds.). mlsys.org.
[20]
Luca Pulina and Armando Tacchella. 2010. An Abstraction-Refinement Approach to Verification of Artificial Neural Networks. In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, Tayssir Touili, Byron Cook, and Paul B. Jackson (Eds.) (Lecture Notes in Computer Science, Vol. 6174). Springer, 243–257. https://doi.org/10.1007/978-3-642-14295-6_24
[21]
Olga Russakovsky, Jia Deng, Hao Su, Jonathan Krause, Sanjeev Satheesh, Sean Ma, Zhiheng Huang, Andrej Karpathy, Aditya Khosla, Michael S. Bernstein, Alexander C. Berg, and Fei-Fei Li. 2015. ImageNet Large Scale Visual Recognition Challenge. Int. J. Comput. Vis., 115, 3 (2015), 211–252. https://doi.org/10.1007/s11263-015-0816-y
[22]
Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. 2019. A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada, Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché-Buc, Emily B. Fox, and Roman Garnett (Eds.). 9832–9842.
[23]
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin T. Vechev. 2018. Fast and Effective Robustness Certification. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett (Eds.). 10825–10836. https://proceedings.neurips.cc/paper/2018/hash/f2f446980d8e971ef3da97af089481c3-Abstract.html
[24]
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T. Vechev. 2019. An abstract domain for certifying neural networks. Proc. ACM Program. Lang., 3, POPL (2019), 41:1–41:30. https://doi.org/10.1145/3290354
[25]
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T. Vechev. 2019. Boosting Robustness Certification of Neural Networks. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net. https://openreview.net/forum?id=HJgeEh09KQ
[26]
Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. 2014. Intriguing properties of neural networks. In 2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Conference Track Proceedings, Yoshua Bengio and Yann LeCun (Eds.). arxiv:1312.6199
[27]
Chris Urmson and William Whittaker. 2008. Self-Driving Cars and the Urban Challenge. IEEE Intell. Syst., 23, 2 (2008), 66–68. https://doi.org/10.1109/MIS.2008.34
[28]
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. 2021. Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification. In Advances in Neural Information Processing Systems, M. Ranzato, A. Beygelzimer, Y. Dauphin, P.S. Liang, and J. Wortman Vaughan (Eds.). 34, Curran Associates, Inc., 29909–29921. https://proceedings.neurips.cc/paper/2021/file/fac7fead96dafceaf80c1daffeae82a4-Paper.pdf
[29]
Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. 2020. Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond. In Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, Hugo Larochelle, Marc’Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin (Eds.).
[30]
Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. 2021. Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net. https://openreview.net/forum?id=nVZtXBI6LNn
[31]
Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue, and Lijun Zhang. 2021. Improving Neural Network Verification through Spurious Region Guided Refinement. In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I, Jan Friso Groote and Kim Guldstrand Larsen (Eds.) (Lecture Notes in Computer Science, Vol. 12651). Springer, 389–408. https://doi.org/10.1007/978-3-030-72016-2_21
[32]
Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. 2018. Efficient Neural Network Robustness Certification with General Activation Functions. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett (Eds.). 4944–4953.
[33]
Jie M. Zhang, Mark Harman, Lei Ma, and Yang Liu. 2022. Machine Learning Testing: Survey, Landscapes and Horizons. IEEE Trans. Software Eng., 48, 2 (2022), 1–36. https://doi.org/10.1109/TSE.2019.2962027
[34]
Ye Zheng, Xiaomu Shi, and Jiaxiang Liu. 2022. Multi-path Back-propagation for Neural Network Verification (in Chinese). Ruan Jian Xue Bao/Journal of Software, 33, 7 (2022), 07, 2464–2481. https://doi.org/10.13328/j.cnki.jos.006585
Index Terms
- MpBP: verifying robustness of neural networks with multi-path bound propagation
Index terms have been assigned to the content through auto-classification.
Recommendations
BERN-NN: Tight Bound Propagation For Neural Networks Using Bernstein Polynomial Interval Arithmetic
HSCC '23: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and ControlIn this paper, we present BERN-NN as an efficient tool to perform bound propagation of Neural Networks (NNs). Bound propagation is a critical step in wide range of NN model checkers and reachability analysis tools. Given a bounded input set, bound ...
Verifying Neural Networks by Approximating Convex Hulls
Formal Methods and Software EngineeringAbstractThe increasing prevalence of neural networks necessitates their verification in order to ensure security. Verifying neural networks is a challenge due to the use of non-linear activation functions. This work concentrates on approximating the ...
Quantitative Symbolic Robustness Verification for Quantized Neural Networks
Formal Methods and Software EngineeringAbstractWith the growing prevalence of neural networks in computer systems, addressing their dependability has become a critical verification problem. In this paper, we focus on quantitative robustness verification, i.e., whether small changes to the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
November 2022
1822 pages
ISBN:9781450394130
DOI:10.1145/3540250
- General Chair:
- Abhik Roychoudhury,
- Program Chairs:
- Cristian Cadar,
- Miryung Kim
Copyright © 2022 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 09 November 2022
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
Conference
ESEC/FSE '22: 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering
November 14 - 18, 2022
Singapore, Singapore
Acceptance Rates
Overall Acceptance Rate 112 of 543 submissions, 21%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 331Total Downloads
- Downloads (Last 12 months)112
- Downloads (Last 6 weeks)26
Reflects downloads up to 14 Feb 2025
Other Metrics
Citations
Cited By
View allView Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in