{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:34Z","timestamp":1784793814950,"version":"3.55.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Modern neural network verifiers often encode neural network verification as constraint satisfaction problems. When dealing with standard piecewise-linear activation functions, such as ReLUs, verifiers typically employ branching heuristics that break a complex constraint satisfaction problem into multiple, simpler problems. The verifier\u2019s performance depends heavily on the order in which this branching is performed: a poor selection may give rise to exponentially many sub-problems, hampering scalability. Here, we focus on the setting in which many related verification queries must be solved for the same neural network. The core idea is to use past experience to make good branching decisions, expediting verification. We present a reinforcement-learning-based branching heuristic that achieves this, by applying Deep Q-learning from Demonstrations (DQfD). Our experimental evaluation demonstrates a substantial reduction in average verification time and in the average number of iterations required, compared to modern splitting heuristics. These results highlight the great potential of reinforcement learning in the context of neural network verification.<\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_1","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:30Z","timestamp":1784791050000},"page":"3-15","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Learning to\u00a0Split: A Reinforcement-Learning-Guided Splitting Heuristic for\u00a0Neural Network Verification (Invited Talk)"],"prefix":"10.1007","author":[{"given":"Maya","family":"Swisa","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guy","family":"Katz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Brix, C., Bak, S., Johnson, T., Wu, H.: The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results. Technical report (2024). https:\/\/arxiv.org\/abs\/2412.19985. https:\/\/doi.org\/10.48550\/arXiv.2412.19985","DOI":"10.48550\/arXiv.2412.19985"},{"issue":"42","key":"1_CR2","first-page":"1","volume":"21","author":"R Bunel","year":"2020","unstructured":"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(42), 1\u201339 (2020)","journal-title":"J. Mach. Learn. Res."},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Carlini, N., Wagner, D.: Towards evaluating the robustness of neural networks. In: Proceedings of IEEE Symposium on Security and Privacy (S&P), pp. 39\u201357 (2017)","DOI":"10.1109\/SP.2017.49"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Casadio, M., et al.: Neural network robustness as a verification property: a principled case study. In: Proceedings of 34th International Conference on Computer Aided Verification (CAV), pp. 219\u2013231 (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_11","DOI":"10.1007\/978-3-031-13185-1_11"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Elboher, Y., et al.: Robustness assessment of a runway object classifier for safe aircraft taxiing. In: Proceedings of 43rd Digital Avionics Systems Conference (DASC), pp. 1\u20136 (2024)","DOI":"10.1109\/DASC62030.2024.10748680"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Ferrari, C., M\u00fcller, M.N., Jovanovic, N., Vechev, M.: Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound. Technical report (2022). https:\/\/arxiv.org\/abs\/2205.00263. https:\/\/doi.org\/10.48550\/arXiv.2205.00263","DOI":"10.48550\/arXiv.2205.00263"},{"key":"1_CR7","unstructured":"Goodfellow, I., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: Proceedings of International Conference on Learning Representations (ICLR) (2015)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"He, K., Zhang, X., Ren, S., Sun, J.: Deep residual learning for image recognition. In: Proceedings of IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pp. 770\u2013778 (2016)","DOI":"10.1109\/CVPR.2016.90"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Hester, T., et al.: Deep Q-learning from demonstrations. In: Proceedings of AAAI Conference on Artificial Intelligence, vol. 32, no. 1 (2018)","DOI":"10.1609\/aaai.v32i1.11757"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Jaeckle, F., Lu, J., Kumar, M.P.: Neural Network Branch-and-Bound for Neural Network Verification. Technical report (2021). https:\/\/arxiv.org\/abs\/2107.12855. https:\/\/doi.org\/10.48550\/arXiv.2107.12855","DOI":"10.48550\/arXiv.2107.12855"},{"issue":"3","key":"1_CR11","doi-asserted-by":"publisher","first-page":"598","DOI":"10.2514\/1.G003724","volume":"42","author":"K Julian","year":"2019","unstructured":"Julian, K., Kochenderfer, M., Owen, M.: Deep neural network compression for aircraft collision avoidance systems. J. Guid. Control. Dyn. 42(3), 598\u2013608 (2019)","journal-title":"J. Guid. Control. Dyn."},{"key":"1_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-021-00363-7","author":"G Katz","year":"2021","unstructured":"Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: a calculus for reasoning about deep neural networks. Formal Methods Syst. Des. (FMSD) (2021). https:\/\/doi.org\/10.1007\/s10703-021-00363-7","journal-title":"Formal Methods Syst. Des. (FMSD)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"Computer Aided Verification","author":"G Katz","year":"2019","unstructured":"Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443\u2013452. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Katz, G., Levy, N., Refaeli, I., Yerushalmi, R.: DEM: a method for certifying deep neural network classifier outputs in aerospace. In: Proceedings of 43rd Digital Avionics Systems Conference (DASC), pp. 1\u20138 (2024)","DOI":"10.1109\/DASC62030.2024.10748779"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Kessler, C., et al.: Neural network verification for gliding drone control: a case study. In: Proceedings of International Symposium on AI Verification (SAIV) (2025)","DOI":"10.1007\/978-3-031-99991-8_9"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Liang, J., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Proceedings of 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 123\u2013140 (2016)","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"1_CR18","unstructured":"OpenAI. ChatGPT (2022). https:\/\/chatgpt.com"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Qu, Q., et al.: An Improved Reinforcement Learning Algorithm for Learning to Branch. Technical report (2022). https:\/\/arxiv.org\/abs\/2201.06213. https:\/\/doi.org\/10.48550\/arXiv.2201.06213","DOI":"10.48550\/arXiv.2201.06213"},{"key":"1_CR20","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT Press (2018)"},{"key":"1_CR21","unstructured":"Swisa, M., Katz, G.: Learning to Split: A Reinforcement-Learning-Guided Splitting Heuristic for Neural Network Verification (Code) (2025). https:\/\/github.com\/mayaswissa\/LearningToSplit"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Szegedy, C., et al.: Intriguing Properties of Neural Networks. Technical report (2013). https:\/\/arxiv.org\/abs\/1312.6199. https:\/\/doi.org\/10.48550\/arXiv.1312.6199","DOI":"10.48550\/arXiv.1312.6199"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"van Hasselt, H., Guez, A., Silver, D.: Deep reinforcement learning with double Q-learning. In: Proceedings of AAAI Conference on Artificial Intelligence, vol. 30, no. 1, pp. 2094\u20132100 (2016)","DOI":"10.1609\/aaai.v30i1.10295"},{"key":"1_CR24","unstructured":"Wang, S., et al.: Beta-CROWN: efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: Proceedings of 35th Conference on Neural Information Processing Systems (NeurIPS) (2021)"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Wu, H., et al.: Parallelization techniques for verifying neural networks. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD), pp. 128\u2013137 (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_20","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_20"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-030-99524-9_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Wu","year":"2022","unstructured":"Wu, H., Zelji\u0107, A., Katz, G., Barrett, C.: Efficient neural network analysis with sum-of-infeasibilities. In: TACAS 2022. LNCS, vol. 13243, pp. 143\u2013163. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_8"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32519-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:35Z","timestamp":1784791055000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}