{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:59:04Z","timestamp":1779087544084,"version":"3.51.4"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"10","license":[{"start":{"date-parts":[[2021,10,20]],"date-time":"2021-10-20T00:00:00Z","timestamp":1634688000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2021,10,20]],"date-time":"2021-10-20T00:00:00Z","timestamp":1634688000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-18-C-009"],"award-info":[{"award-number":["FA8750-18-C-009"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mach Learn"],"published-print":{"date-parts":[[2023,10]]},"DOI":"10.1007\/s10994-021-06050-2","type":"journal-article","created":{"date-parts":[[2021,10,20]],"date-time":"2021-10-20T22:41:15Z","timestamp":1634769675000},"page":"3685-3712","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Global optimization of objective functions represented by ReLU networks"],"prefix":"10.1007","volume":"112","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8914-6852","authenticated-orcid":false,"given":"Christopher A.","family":"Strong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5077-144X","authenticated-orcid":false,"given":"Haoze","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0673-9327","authenticated-orcid":false,"given":"Aleksandar","family":"Zelji\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6247-1874","authenticated-orcid":false,"given":"Kyle D.","family":"Julian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5292-801X","authenticated-orcid":false,"given":"Guy","family":"Katz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7238-9663","authenticated-orcid":false,"given":"Mykel J.","family":"Kochenderfer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,10,20]]},"reference":[{"key":"6050_CR1","unstructured":"Bak, S., Liu, C., & Johnson, T. T. (2021). VNN21. https:\/\/sites.google.com\/view\/vnn2021. Accessed 17 July 2021"},{"key":"6050_CR2","unstructured":"Balunovic, M., Baader, M., Singh, G., Gehr, T., & Vechev, M. (2019). Certifying geometric robustness of neural networks. In Advances in neural information processing systems (NIPS) (pp. 15313\u201315323)."},{"key":"6050_CR3","doi-asserted-by":"crossref","unstructured":"Bjorner, N., Phan, A. D., & Fleckenstein, L. (2015). $$\\nu$$z-an optimizing SMT solver. In International conference on tools and algorithms for the construction and analysis of systems (TACAS) (pp. 194\u2013199). Springer.","DOI":"10.1007\/978-3-662-46681-0_14"},{"key":"6050_CR4","unstructured":"Bojarski, M., Del\u00a0Testa, D., Dworakowski, D., Firner, B., Flepp, B., Goyal, P., Jackel, L., Monfort, M., Muller, U., Zhang, J., Zhang, X., Zhao, J., & Zieba, K. (2016). End to end learning for self-driving cars. Technical Report. arXiv:1604.07316"},{"key":"6050_CR5","doi-asserted-by":"publisher","first-page":"3240","DOI":"10.1609\/aaai.v33i01.33013240","volume":"33","author":"A Boopathy","year":"2019","unstructured":"Boopathy, A., Weng, T. W., Chen, P. Y., Liu, S., & Daniel, L. (2019). Cnn-cert: An efficient framework for certifying robustness of convolutional neural networks. AAAI Conference on Artificial Intelligence, 33, 3240\u20133247.","journal-title":"AAAI Conference on Artificial Intelligence"},{"key":"6050_CR6","doi-asserted-by":"crossref","unstructured":"Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., & Misener, R. (2020). Efficient verification of relu-based neural networks via dependency analysis. In AAAI conference on artificial intelligence (AAAI).","DOI":"10.1609\/aaai.v34i04.5729"},{"issue":"2020","key":"6050_CR7","first-page":"1","volume":"21","author":"R Bunel","year":"2020","unstructured":"Bunel, R., Lu, J., Turkaslan, I., Kohli, P., Torr, P., & Mudigonda, P. (2020). Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21(2020), 1\u201339.","journal-title":"Journal of Machine Learning Research"},{"key":"6050_CR8","doi-asserted-by":"crossref","unstructured":"Carlini, N., & Wagner, D. (2017). Towards evaluating the robustness of neural networks. In 2017 IEEE symposium on security and privacy (SP) (pp. 39\u201357). IEEE.","DOI":"10.1109\/SP.2017.49"},{"key":"6050_CR9","unstructured":"Carlini, N., Katz, G., Barrett, C., & Dill, D. L. (2017). Provably minimally-distorted adversarial examples. arXiv preprint arXiv:170910207"},{"issue":"1","key":"6050_CR10","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1049\/cit2.12028","volume":"6","author":"A Chakraborty","year":"2021","unstructured":"Chakraborty, A., Alam, M., Dey, V., Chattopadhyay, A., & Mukhopadhyay, D. (2021). A survey on adversarial attacks and defences. CAAI Transactions on Intelligence Technology, 6(1), 25\u201345.","journal-title":"CAAI Transactions on Intelligence Technology"},{"key":"6050_CR11","doi-asserted-by":"crossref","unstructured":"Cheng, C. H., N\u00fchrenberg, G., & Ruess, H. (2017). Maximum resilience of artificial neural networks. In International symposium on automated technology for verification and analysis (pp. 251\u2013268). Springer.","DOI":"10.1007\/978-3-319-68167-2_18"},{"issue":"3","key":"6050_CR12","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/s10601-018-9285-6","volume":"23","author":"M Fischetti","year":"2018","unstructured":"Fischetti, M., & Jo, J. (2018). Deep neural networks and mixed integer linear optimization. Constraints, 23(3), 296\u2013309. https:\/\/doi.org\/10.1007\/s10601-018-9285-6.","journal-title":"Constraints"},{"key":"6050_CR13","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, E., Chaudhuri, S., & Vechev, M. (2018). AI2: Safety and robustness certification of neural networks with abstract interpretation. In IEEE symposium on security and privacy (S&P).","DOI":"10.1109\/SP.2018.00058"},{"key":"6050_CR14","unstructured":"Goodfellow, I., Shlens, J., & Szegedy, C. (2015). Explaining and harnessing adversarial examples. In International conference on learning representations. arxiv.org\/abs\/1412.6572"},{"key":"6050_CR15","unstructured":"Gurobi\u00a0Optimization L (2020). Gurobi optimizer reference manual. http:\/\/www.gurobi.com"},{"key":"6050_CR16","doi-asserted-by":"crossref","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., & Wu, M. (2017). Safety verification of deep neural networks. In International conference on computer-aided verification (pp. 3\u201329).","DOI":"10.1007\/978-3-319-63387-9_1"},{"issue":"6","key":"6050_CR17","doi-asserted-by":"publisher","first-page":"1083","DOI":"10.1016\/0005-1098(92)90053-I","volume":"28","author":"KJ Hunt","year":"1992","unstructured":"Hunt, K. J., Sbarbaro, D., Zbikowski, R., & Gawthrop, P. J. (1992). Neural networks for control systems\u2014a survey. Automatica, 28(6), 1083\u20131112.","journal-title":"Automatica"},{"key":"6050_CR18","unstructured":"Johnson, T. T., & Liu, C. (2020). Vnn20. https:\/\/sites.google.com\/view\/vnn20\/. Accessed 17 July 2021."},{"key":"6050_CR19","doi-asserted-by":"crossref","unstructured":"Julian, K., Lopez, J., Brush, J., Owen, M., & Kochenderfer, M. (2016). Policy compression for aircraft collision avoidance systems. In Digital avionics systems conf. (DASC) (pp. 1\u201310).","DOI":"10.1109\/DASC.2016.7778091"},{"key":"6050_CR20","doi-asserted-by":"crossref","unstructured":"Julian, K. D., Lee, R., & Kochenderfer, M. J. (2020). Validation of image-based neural network controllers through adaptive stress testing. In 2020 IEEE 23rd international conference on intelligent transportation systems (ITSC) (pp. 1\u20137).","DOI":"10.1109\/ITSC45102.2020.9294549"},{"key":"6050_CR21","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D. L., Julian, K., & Kochenderfer, M. J. (2017). Reluplex: An efficient smt solver for verifying deep neural networks. In International conference on computer-aided verification (pp. 97\u2013117). Springer.","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"6050_CR22","doi-asserted-by":"crossref","unstructured":"Katz, G., Huang, D. A., Ibelingm, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., & Zelji\u0107, A., et\u00a0al. (2019). The marabou framework for verification and analysis of deep neural networks. In International conference on computer-aided verification (pp. 443\u2013452). Springer.","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"6050_CR23","volume-title":"Algorithms for optimization","author":"MJ Kochenderfer","year":"2019","unstructured":"Kochenderfer, M. J., & Wheeler, T. A. (2019). Algorithms for optimization. London: MIT Press."},{"key":"6050_CR24","unstructured":"Krizhevsky, A., Sutskever, I., & Hinton, G. E. (2012). Imagenet classification with deep convolutional neural networks. In Advances in neural information processing systems (NIPS) (pp. 1097\u20131105)."},{"key":"6050_CR25","doi-asserted-by":"crossref","unstructured":"Le, Q. V. (2013). Building high-level features using large scale unsupervised learning. In IEEE international conference on acoustics, speech and signal processing(pp. 8595\u20138598).","DOI":"10.1109\/ICASSP.2013.6639343"},{"key":"6050_CR26","doi-asserted-by":"publisher","unstructured":"Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., & Kochenderfer, M. J. (2021). Algorithms for verifying deep neural networks. Foundations and Trends\u00ae in Optimization,4(3\u20134), 244\u2013404. https:\/\/doi.org\/10.1561\/2400000035","DOI":"10.1561\/2400000035"},{"key":"6050_CR27","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/j.neucom.2016.12.038","volume":"234","author":"W Liu","year":"2017","unstructured":"Liu, W., Wang, Z., Liu, X., Zeng, N., Liu, Y., & Alsaadi, F. E. (2017). A survey of deep neural network architectures and their applications. Neurocomputing, 234, 11\u201326.","journal-title":"Neurocomputing"},{"key":"6050_CR28","unstructured":"Lomuscio, A., & Maganti, L. (2017). An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:170607351"},{"key":"6050_CR29","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., & Vladu, A. (2018). Towards deep learning models resistant to adversarial attacks. In International conference on learning representations. https:\/\/openreview.net\/forum?id=rJzIBfZAb"},{"key":"6050_CR30","unstructured":"Makhorin, A. (2004). GLPK (Gnu linear programming kit), version 4.42. http:\/\/www.gnu.org\/software\/glpk"},{"key":"6050_CR31","unstructured":"M\u00fcller, C., Singh, G., P\u00fcschel, M., & Vechev, M.T. (2020). Neural network robustness verification on gpus. CoRR arxiv.org\/abs\/2007.10868"},{"key":"6050_CR32","unstructured":"Otter, D. W., Medina, J. R., & Kalita, J. K. (2020). A survey of the usages of deep learning for natural language processing. IEEE Transactions on Neural Networks and Learning Systems, 1\u201321."},{"key":"6050_CR33","doi-asserted-by":"crossref","unstructured":"Ribeiro, M. T., Singh, S., & Guestrin, C. (2016). \u201cWhy should I trust you?\u201d explaining the predictions of any classifier. In ACM SIGKDD International conference on knowledge discovery and data mining (pp. 1135\u20131144).","DOI":"10.1145\/2939672.2939778"},{"key":"6050_CR34","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/j.neunet.2014.09.003","volume":"61","author":"J Schmidhuber","year":"2015","unstructured":"Schmidhuber, J. (2015). Deep learning in neural networks: An overview. Neural Networks, 61, 85\u2013117.","journal-title":"Neural Networks"},{"key":"6050_CR35","doi-asserted-by":"crossref","unstructured":"Sebastiani, R., & Trentin, P. (2015). Pushing the envelope of optimization modulo theories with linear-arithmetic cost functions. In International conference on tools and algorithms for the construction and analysis of systems (TACAS) (pp. 335\u2013349). Springer.","DOI":"10.1007\/978-3-662-46681-0_27"},{"issue":"3","key":"6050_CR36","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-09508-6","volume":"64","author":"R Sebastiani","year":"2020","unstructured":"Sebastiani, R., & Trentin, P. (2020). Optimathsat: A tool for optimization modulo theories. Journal of Automated Reasoning, 64(3), 423\u2013460.","journal-title":"Journal of Automated Reasoning"},{"key":"6050_CR37","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., & Vechev, M. (2018a). Fast and effective robustness certification. In Advances in neural information processing systems (NIPS) (pp. 10802\u201310813)."},{"key":"6050_CR38","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., & Vechev, M. (2018b). Boosting robustness certification of neural networks. In International conference on learning representations."},{"key":"6050_CR39","unstructured":"Singh, G., Ganvir, R., P\u00fcschel, M., & Vechev, M. (2019a). Beyond the single neuron convex barrier for neural network certification. In Advances in neural information processing systems (NIPS) (pp. 15098\u201315109)."},{"key":"6050_CR40","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., & Vechev, M. (2019b). An abstract domain for certifying neural networks. In Proceedings of the ACM on programming languages 3(POPL) (pp. 1\u201330).","DOI":"10.1145\/3290354"},{"key":"6050_CR41","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., & Fergus, R. (2014). Intriguing properties of neural networks. In International conference on learning representations. arxiv.org\/abs\/1312.6199"},{"key":"6050_CR42","unstructured":"Tjeng, V., Xiao, K. Y., & Tedrake, R. (2019). Evaluating robustness of neural networks with mixed integer programming. In International conference on learning representations. https:\/\/openreview.net\/forum?id=HyGIdiRqtm"},{"key":"6050_CR43","doi-asserted-by":"crossref","unstructured":"Tran, H. D., Lopez, D. M., Musau, P., Yang, X., Nguyen, L. V., Xiang, W., & Johnson, T. T. (2019). Star-based reachability analysis of deep neural networks. In International symposium on formal methods (pp. 670\u2013686). Springer.","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"6050_CR44","doi-asserted-by":"crossref","unstructured":"Tran, H. D., Bak, S., Xiang, W., & Johnson, T. T. (2020a). Verification of deep convolutional neural networks using imagestars. In International conference on computer aided verification (pp. 18\u201342). Springer.","DOI":"10.1007\/978-3-030-53288-8_2"},{"key":"6050_CR45","first-page":"3","volume":"12224","author":"HD Tran","year":"2020","unstructured":"Tran, H. D., Yang, X., Lopez, D. M., Musau, P., Nguyen, L., Xiang, W., et al. (2020). Nnv: The neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. Computer Aided Verification, 12224, 3\u201317.","journal-title":"Computer Aided Verification"},{"key":"6050_CR46","doi-asserted-by":"crossref","unstructured":"Vincent, J. A., & Schwager, M. (2021). Reachable polyhedral marching (rpm): A safety verification algorithm for robotic systems with deep neural network components. In IEEE international conference on robotics and automation (ICRA).","DOI":"10.1109\/ICRA48506.2021.9561956"},{"key":"6050_CR47","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., & Jana, S. (2018a). Efficient formal safety analysis of neural networks. In Advances in neural information processing systems (NIPS) (pp. 6367\u20136377)."},{"key":"6050_CR48","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., & Jana, S. (2018b). Formal security analysis of neural networks using symbolic intervals. In $$USENIX$$security symposium (pp. 1599\u20131614)."},{"key":"6050_CR49","unstructured":"Weng, T. W., Zhang, H., Chen, H., Song, Z., Hsieh, C. J., Boning, D., Dhillon, I. S., & Daniel, L. (2018). Towards fast computation of certified robustness for relu networks. In International conference on machine learning (ICML)."},{"key":"6050_CR50","volume-title":"Integer programming","author":"LA Wolsey","year":"1998","unstructured":"Wolsey, L. A. (1998). Integer programming (Vol. 52). London: Wiley."},{"key":"6050_CR51","unstructured":"Wu, H., Ozdemir, A., Zelji\u0107, A., Julian, K., Irfan, A., Gopinath, D., Fouladi, S., Katz, G., Pasareanu, C., & Barrett, C. (2020). Parallelization techniques for verifying neural networks. In Formal methods in computer aided design (FMCAD)."},{"key":"6050_CR52","doi-asserted-by":"publisher","unstructured":"Xiang, W., Tran, H. D., Rosenfeld, J. A., & Johnson, T. T. (2018). Reachable set estimation and safety verification for piecewise linear systems with neural network controllers. In Annual American control conference (pp. 1574\u20131579). https:\/\/doi.org\/10.23919\/ACC.2018.8431048","DOI":"10.23919\/ACC.2018.8431048"},{"issue":"9","key":"6050_CR53","doi-asserted-by":"publisher","first-page":"2805","DOI":"10.1109\/TNNLS.2018.2886017","volume":"30","author":"X Yuan","year":"2019","unstructured":"Yuan, X., He, P., Zhu, Q., & Li, X. (2019). Adversarial examples: Attacks and defenses for deep learning. IEEE Transactions on Neural Networks and Learning Systems, 30(9), 2805\u20132824.","journal-title":"IEEE Transactions on Neural Networks and Learning Systems"},{"key":"6050_CR54","unstructured":"Zhang, H., Weng, T. W., Chen, P. Y., Hsieh, C. J., & Daniel, L. (2018). Efficient neural network robustness certification with general activation functions. In Advances in neural information processing systems (NeurIPS)."},{"issue":"4","key":"6050_CR55","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1145\/279232.279236","volume":"23","author":"C Zhu","year":"1997","unstructured":"Zhu, C., Byrd, R. H., Lu, P., & Nocedal, J. (1997). Algorithm 778: L-BFGS-B: Fortran subroutines for large-scale bound-constrained optimization. ACM Transactions on Mathematical Software (TOMS), 23(4), 550\u2013560.","journal-title":"ACM Transactions on Mathematical Software (TOMS)"}],"container-title":["Machine Learning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10994-021-06050-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10994-021-06050-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10994-021-06050-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,7]],"date-time":"2023-09-07T22:05:08Z","timestamp":1694124308000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10994-021-06050-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,20]]},"references-count":55,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2023,10]]}},"alternative-id":["6050"],"URL":"https:\/\/doi.org\/10.1007\/s10994-021-06050-2","relation":{},"ISSN":["0885-6125","1573-0565"],"issn-type":[{"value":"0885-6125","type":"print"},{"value":"1573-0565","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,20]]},"assertion":[{"value":"2 October 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 July 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 August 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 October 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}