Abstract
The robustness of deep neural networks has received extensive attention and is considered to need guarantees by formal verification. For ReLU neural network verification, there are abundant studies and various techniques. However, verifying sigmoid-like neural networks still relies on linear approximation, which inevitably introduces errors and leads to imprecise results. To reduce error and get better results, we present a branch and bound framework for sigmoid-like neural network verification in this paper. In this framework, we design a neuron splitting method and a branching strategy. The splitting method can split neurons with non-linear sigmoid-like activation functions, and the branching strategy reduces the size of the branch and bound tree, which improves the verification performance. We implement our verification framework as SigBaB and evaluate its performance on open source benchmarks. Experiment results show that our method can produce more precise verification results than other state-of-the-art methods and our branching strategy shows superior performance compared to other strategies.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Boopathy, A., Weng, T., Chen, P., Liu, S., Daniel, L.: CNN-Cert: an efficient framework for certifying robustness of convolutional neural networks. In: The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, pp. 3240–3247. AAAI Press (2019)
Bunel, R., Lu, J., Turkaslan, I., Torr, P.H.S., Kohli, P., Kumar, M.P.: Branch and bound for piecewise linear neural network verification. J. Mach. Learn. Res. 21, 1–39 (2020)
Carlini, N., Wagner, D.: Towards evaluating the robustness of neural networks. In: 2017 IEEE Symposium on Security and Privacy (SP), pp. 39–57. IEEE (2017)
Chen, Z., Huang, X.: End-to-end learning for lane keeping of self-driving cars. In: 2017 IEEE Intelligent Vehicles Symposium (IV), pp. 1856–1860. IEEE (2017)
Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 269–286. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68167-2_19
Gagandeep, S., et al.: ERAN verification dataset. https://github.com/eth-sri/eran. [online]
Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: 3rd International Conference on Learning Representations (ICLR), Conference Track Proceedings (2015)
Henriksen, P., Lomuscio, A.R.: Efficient neural network verification via adaptive refinement and adversarial search. In: Giacomo, G.D., et al. (eds.) ECAI 2020. Frontiers in Artificial Intelligence and Applications, vol. 325, pp. 2513–2520. IOS Press (2020)
Julian, K.D., Lopez, J., Brush, J.S., Owen, M.P., Kochenderfer, M.J.: Policy compression for aircraft collision avoidance systems. In: 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC), pp. 1–10. IEEE (2016)
Kos, J., Fischer, I., Song, D.: Adversarial examples for generative models. In: 2018 IEEE Security and Privacy Workshops (SPW), pp. 36–42. IEEE (2018)
LeCun, Y., Bottou, L., Bengio, Y., Haffner, P.: Gradient-based learning applied to document recognition. Proc. IEEE 86(11), 2278–2324 (1998)
Lin, W., et al.: Robustness verification of classification deep neural networks via linear programming. In: IEEE Conference on Computer Vision and Pattern Recognition, CVPR, pp. 11418–11427. Computer Vision Foundation / IEEE (2019)
Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward ReLU neural networks (2017). https://arxiv.org/abs/1706.07351
Palma, A.D., et al.: Improved branch and bound for neural network verification via Lagrangian decomposition (2021). https://arxiv.org/abs/2104.06718
Singh, G., Ganvir, R., Püschel, M., Vechev, M.: Beyond the single neuron convex barrier for neural network certification. In: Advances in Neural Information Processing Systems (NeurIPS), vol. 32, pp. 15072–15083 (2019)
Singh, G., Gehr, T., Püschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proc. ACM Programm. Lang. 3(POPL), 1–30 (2019)
Szegedy, C., et al.: Intriguing properties of neural networks. In: 2nd International Conference on Learning Representations (ICLR), Conference Track Proceedings (2014)
Wang, S., et al.: Beta-CROWN: efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: Advances in Neural Information Processing Systems (NeurIPS), vol. 34, pp. 29909–29921 (2021)
Wong, E., Kolter, J.Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsmässan, Stockholm, Sweden, 10–15 July 2018. Proceedings of Machine Learning Research, vol. 80, pp. 5283–5292. PMLR (2018)
Wu, Y., Zhang, M.: Tightening robustness verification of convolutional neural networks with fine-grained linear approximation. In: Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, pp. 11674–11681. AAAI Press (2021)
Xiao, H., Rasul, K., Vollgraf, R.: Fashion-MNIST: a novel image dataset for benchmarking machine learning algorithms. CoRR abs/1708.07747 (2017)
Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Advances in Neural Information Processing Systems (NeurIPS), vol. 31, pp. 4944–4953 (2018)
Zhang, Z., Wu, Y., Liu, S., Liu, J., Zhang, M.: Provably tightest linear approximation for robustness verification of sigmoid-like neural networks. In: 37th IEEE/ACM International Conference on Automated Software Engineering, ASE 2022, pp. 1–13. ACM (2022)
Acknowledgements
This research was sponsored by the National Natural Science Foundation of China under Grant No. 62172019.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Xue, X., Sun, M. (2023). Branch and Bound for Sigmoid-Like Neural Network Verification. In: Li, Y., Tahar, S. (eds) Formal Methods and Software Engineering. ICFEM 2023. Lecture Notes in Computer Science, vol 14308. Springer, Singapore. https://doi.org/10.1007/978-981-99-7584-6_9
Download citation
DOI: https://doi.org/10.1007/978-981-99-7584-6_9
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-99-7583-9
Online ISBN: 978-981-99-7584-6
eBook Packages: Computer ScienceComputer Science (R0)