{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:16:02Z","timestamp":1775873762149,"version":"3.50.1"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906428","type":"print"},{"value":"9783031906435","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"Abstract<\/jats:title>\n \nBranch-and-bound (BaB) is among the most effective techniques for neural network (NN) verification. However, existing works on BaB for NN verification have mostly focused on NNs with piecewise linear activations, especially ReLU networks. In this paper, we develop a general framework, named GenBaB, to conduct BaB on general nonlinearities to verify NNs with general architectures, based on linear bound propagation for NN verification. To decide which neuron to branch, we design a new branching heuristic which leverages linear bounds as shortcuts to efficiently estimate the potential improvement after branching. To decide nontrivial branching points for general nonlinear functions, we propose to pre-optimize branching points, which can be efficiently leveraged during verification with a lookup table. We demonstrate the effectiveness of our GenBaB on verifying a wide range of NNs, including NNs with activation functions such as Sigmoid, Tanh, Sine and GeLU, as well as NNs involving multi-dimensional nonlinear operations such as multiplications in LSTMs and Vision Transformers. Our framework also allows the verification of general nonlinear computation graphs and enables verification applications beyond simple NNs, particularly for AC Optimal Power Flow (ACOPF). GenBaB is part of the latest \n \n $$\\alpha ,\\!\\beta $$<\/jats:tex-math>\n \n \n \u03b1<\/mml:mi>\n ,<\/mml:mo>\n \n \u03b2<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>-CROWN\n \n $$^6$$<\/jats:tex-math>\n \n \n \n 6<\/mml:mn>\n <\/mml:msup>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> (https:\/\/github.com\/Verified-Intelligence\/alpha-beta-CROWN<\/jats:ext-link>), the winner of the 4th and the 5th International Verification of Neural Networks Competition (VNN-COMP 2023 and 2024). Code for reproducing the experiments is available at https:\/\/github.com\/shizhouxing\/GenBaB<\/jats:ext-link>. Appendices can be found at http:\/\/arxiv.org\/abs\/2405.21063<\/jats:ext-link>.<\/jats:p>","DOI":"10.1007\/978-3-031-90643-5_17","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:15Z","timestamp":1745993295000},"page":"315-335","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Neural Network Verification with Branch-and-Bound for General Nonlinearities"],"prefix":"10.1007","author":[{"given":"Zhouxing","family":"Shi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qirui","family":"Jin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zico","family":"Kolter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Suman","family":"Jana","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cho-Jui","family":"Hsieh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Bonaert, G., Dimitrov, D.I., Baader, M., Vechev, M.: Fast and precise certification of transformers. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 466\u2013481 (2021)","DOI":"10.1145\/3453483.3454056"},{"key":"17_CR2","doi-asserted-by":"publisher","unstructured":"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, pp. 3240\u20133247 (2019), https:\/\/doi.org\/10.1609\/aaai.v33i01.33013240","DOI":"10.1609\/aaai.v33i01.33013240"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Brix, C., Bak, S., Liu, C., Johnson, T.T.: The fourth international verification of neural networks competition (vnn-comp 2023): Summary and results. arXiv preprint arXiv:2312.16760 (2023)","DOI":"10.1007\/s10009-023-00703-4"},{"key":"17_CR4","unstructured":"Bunel, R., Mudigonda, P., Turkaslan, I., Torr, P., Lu, J., Kohli, P.: Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research 21(2020) (2020)"},{"key":"17_CR5","unstructured":"Bunel, R., Turkaslan, I., Torr, P.H.S., Kohli, P., Mudigonda, P.K.: A unified view of piecewise linear neural network verification. In: Advances in Neural Information Processing Systems, pp. 4795\u20134804 (2018)"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Choi, S.W., Ivashchenko, M., Nguyen, L.V., Tran, H.D.: Reachability analysis of sigmoidal neural networks. ACM Transactions on Embedded Computing Systems (2023)","DOI":"10.1145\/3627991"},{"key":"17_CR7","unstructured":"De\u00a0Palma, A., Bunel, R., Desmaison, A., Dvijotham, K., Kohli, P., Torr, P.H., Kumar, M.P.: Improved branch and bound for neural network verification via lagrangian decomposition. arXiv preprint arXiv:2104.06718 (2021)"},{"key":"17_CR8","unstructured":"Dosovitskiy, A., Beyer, L., Kolesnikov, A., Weissenborn, D., Zhai, X., Unterthiner, T., Dehghani, M., Minderer, M., Heigold, G., Gelly, S., Uszkoreit, J., Houlsby, N.: An image is worth 16x16 words: Transformers for image recognition at scale. In: International Conference on Learning Representations (2021)"},{"key":"17_CR9","doi-asserted-by":"publisher","unstructured":"Du, T., Ji, S., Shen, L., Zhang, Y., Li, J., Shi, J., Fang, C., Yin, J., Beyah, R., Wang, T.: Cert-rnn: Towards certifying the robustness of recurrent neural networks. In: Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, p. 516\u2013534, CCS \u201921 (2021), ISBN 9781450384544, https:\/\/doi.org\/10.1145\/3460120.3484538","DOI":"10.1145\/3460120.3484538"},{"key":"17_CR10","unstructured":"Dvijotham, K., Stanforth, R., Gowal, S., Mann, T.A., Kohli, P.: A dual approach to scalable verification of deep networks. In: Proceedings of the Thirty-Fourth Conference on Uncertainty in Artificial Intelligence, UAI 2018, Monterey, California, USA, August 6-10, 2018, pp. 550\u2013559 (2018)"},{"key":"17_CR11","unstructured":"Ferrari, C., Mueller, M.N., Jovanovi\u0107, N., Vechev, M.: Complete verification via multi-neuron relaxation guided branch-and-bound. In: International Conference on Learning Representations (2021)"},{"key":"17_CR12","unstructured":"Geng, C., Le, N., Xu, X., Wang, Z., Gurfinkel, A., Si, X.: Towards reliable neural specifications. In: International Conference on Machine Learning, pp. 11196\u201311212, PMLR (2023)"},{"key":"17_CR13","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: International Conference on Learning Representations (2015)"},{"key":"17_CR14","unstructured":"Guha, N., Wang, Z., Wytock, M., Majumdar, A.: Machine learning for ac optimal power flow. arXiv preprint arXiv:1910.08842 (2019)"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Henriksen, P., Lomuscio, A.: Efficient neural network verification via adaptive refinement and adversarial search. In: ECAI 2020, pp. 2513\u20132520, IOS Press (2020)","DOI":"10.3233\/FAIA200385"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Henriksen, P., Lomuscio, A.: Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis. In: IJCAI, pp. 2549\u20132555 (2021)","DOI":"10.24963\/ijcai.2021\/351"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Hochreiter, S., Schmidhuber, J.: Long short-term memory. Neural computation 9(8), 1735\u20131780 (1997)","DOI":"10.1162\/neco.1997.9.8.1735"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient smt solver for verifying deep neural networks. In: International Conference on Computer Aided Verification, pp. 97\u2013117 (2017)","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"17_CR19","unstructured":"Ko, C., Lyu, Z., Weng, L., Daniel, L., Wong, N., Lin, D.: POPQORN: quantifying robustness of recurrent neural networks. In: International Conference on Machine Learning, Proceedings of Machine Learning Research, vol.\u00a097, pp. 3468\u20133477 (2019)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Kouvaros, P., Lomuscio, A.: Towards scalable complete verification of relu neural networks via dependency-based branching. In: IJCAI, pp. 2643\u20132650 (2021)","DOI":"10.24963\/ijcai.2021\/364"},{"key":"17_CR21","unstructured":"Krizhevsky, A., Hinton, G., et\u00a0al.: Learning multiple layers of features from tiny images. Technical Report TR-2009 (2009)"},{"key":"17_CR22","unstructured":"LeCun, Y., Cortes, C., Burges, C.: Mnist handwritten digit database. ATT Labs [Online]. Available: http:\/\/yann.lecun.com\/exdb\/mnist2 (2010)"},{"key":"17_CR23","unstructured":"Lu, J., Mudigonda, P.: Neural network branching for neural network verification. In: Proceedings of the International Conference on Learning Representations (ICLR 2020), Open Review (2020)"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Lyu, Z., Ko, C., Kong, Z., Wong, N., Lin, D., Daniel, L.: Fastened CROWN: tightened neural network robustness certificates. In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, pp. 5037\u20135044 (2020)","DOI":"10.1609\/aaai.v34i04.5944"},{"key":"17_CR25","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: International Conference on Learning Representations (2018)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Mohammadinejad, S., Paulsen, B., Deshmukh, J.V., Wang, C.: Diffrnn: Differential verification of recurrent neural networks. In: Formal Modeling and Analysis of Timed Systems: 19th International Conference, FORMATS 2021, Paris, France, August 24\u201326, 2021, Proceedings 19, pp. 117\u2013134, Springer (2021)","DOI":"10.1007\/978-3-030-85037-1_8"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"M\u00fcller, M.N., Makarchuk, G., Singh, G., P\u00fcschel, M., Vechev, M.: Prima: general and precise neural network certification via scalable convex hull approximations. Proceedings of the ACM on Programming Languages 6(POPL), 1\u201333 (2022)","DOI":"10.1145\/3498704"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Paulsen, B., Wang, C.: Linsyn: Synthesizing tight linear bounds for arbitrary neural network activation functions. In: Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2\u20137, 2022, Proceedings, Part I, pp. 357\u2013376, Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_19"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Ryou, W., Chen, J., Balunovic, M., Singh, G., Dan, A., Vechev, M.: Scalable polyhedral verification of recurrent neural networks. In: International Conference on Computer Aided Verification, pp. 225\u2013248 (2021)","DOI":"10.1007\/978-3-030-81685-8_10"},{"key":"17_CR30","unstructured":"Shi, Z., Wang, Y., Zhang, H., Kolter, J.Z., Hsieh, C.J.: Efficiently computing local lipschitz constants of neural networks via bound propagation. Advances in Neural Information Processing Systems 35, 2350\u20132364 (2022)"},{"key":"17_CR31","unstructured":"Shi, Z., Zhang, H., Chang, K., Huang, M., Hsieh, C.: Robustness verification for transformers. In: International Conference on Learning Representations (2020)"},{"key":"17_CR32","unstructured":"Shi, Z., Zhang, H., Chang, K.W., Huang, M., Hsieh, C.J.: Robustness verification for transformers. In: International Conference on Learning Representations (2019)"},{"key":"17_CR33","unstructured":"Singh, G., Ganvir, R., P\u00fcschel, M., Vechev, M.T.: Beyond the single neuron convex barrier for neural network certification. In: Advances in Neural Information Processing Systems, pp. 15072\u201315083 (2019)"},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages 3(POPL), 41 (2019)","DOI":"10.1145\/3290354"},{"key":"17_CR35","unstructured":"Sitzmann, V., Martel, J., Bergman, A., Lindell, D., Wetzstein, G.: Implicit neural representations with periodic activation functions. Advances in Neural Information Processing Systems 33, 7462\u20137473 (2020)"},{"key":"17_CR36","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I.J., Fergus, R.: Intriguing properties of neural networks. In: International Conference on Learning Representations (2014)"},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Tran, H.D., Choi, S.W., Yang, X., Yamaguchi, T., Hoxha, B., Prokhorov, D.: Verification of recurrent neural networks with star reachability. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201313 (2023)","DOI":"10.1145\/3575870.3587128"},{"key":"17_CR38","unstructured":"Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A.N., Kaiser, L., Polosukhin, I.: Attention is all you need. In: Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pp. 5998\u20136008 (2017)"},{"key":"17_CR39","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: Advances in Neural Information Processing Systems, pp. 6369\u20136379 (2018)"},{"key":"17_CR40","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: 27th $$\\{$$USENIX$$\\}$$ Security Symposium ($$\\{$$USENIX$$\\}$$ Security 18), pp. 1599\u20131614 (2018)"},{"key":"17_CR41","unstructured":"Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., Kolter, J.Z.: Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems 34, 29909\u201329921 (2021)"},{"key":"17_CR42","unstructured":"Wei, D., Wu, H., Wu, M., Chen, P.Y., Barrett, C., Farchi, E.: Convex bounds on the softmax function with applications to robustness verification. In: International Conference on Artificial Intelligence and Statistics, pp. 6853\u20136878, PMLR (2023)"},{"key":"17_CR43","unstructured":"Wong, E., Kolter, J.Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: International Conference on Machine Learning, Proceedings of Machine Learning Research, vol.\u00a080, pp. 5283\u20135292 (2018)"},{"key":"17_CR44","doi-asserted-by":"crossref","unstructured":"Wu, H., Tagomori, T., Robey, A., Yang, F., Matni, N., Pappas, G., Hassani, H., Pasareanu, C., Barrett, C.: Toward certified robustness against real-world distribution shifts. arXiv preprint arXiv:2206.03669 (2022)","DOI":"10.1109\/SaTML54575.2023.00042"},{"key":"17_CR45","unstructured":"Xu, K., Shi, Z., Zhang, H., Wang, Y., Chang, K., Huang, M., Kailkhura, B., Lin, X., Hsieh, C.: Automatic perturbation analysis for scalable certified robustness and beyond. In: Advances in Neural Information Processing Systems (2020)"},{"key":"17_CR46","unstructured":"Xu, K., Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X., Hsieh, C.: Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In: International Conference on Learning Representations (2021)"},{"key":"17_CR47","unstructured":"Zhang, H., Chen, H., Xiao, C., Gowal, S., Stanforth, R., Li, B., Boning, D.S., Hsieh, C.: Towards stable and efficient training of verifiably robust neural networks. In: International Conference on Learning Representations (2020)"},{"key":"17_CR48","unstructured":"Zhang, H., Weng, T., Chen, P., Hsieh, C., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Advances in Neural Information Processing Systems, pp. 4944\u20134953 (2018)"},{"key":"17_CR49","unstructured":"Zhang, Y., Du, T., Ji, S., Tang, P., Guo, S.: Rnn-guard: Certified robustness against multi-frame attacks for recurrent neural networks. arXiv preprint arXiv:2304.07980 (2023)"},{"key":"17_CR50","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Shen, L., Guo, S., Ji, S.: Galileo: General linear relaxation framework for tightening robustness certification of transformers. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a038, pp. 21797\u201321805 (2024)","DOI":"10.1609\/aaai.v38i19.30180"},{"key":"17_CR51","unstructured":"Zhou, X., Xu, H., Xu, A., Shi, Z., Hsieh, C.J., Zhang, H.: Testing neural network verifiers: A soundness benchmark with hidden counterexamples. arXiv preprint arXiv:2412.03154 (2024)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90643-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:54Z","timestamp":1745993334000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90643-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906428","9783031906435"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90643-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}