{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T22:42:53Z","timestamp":1784328173672,"version":"3.55.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"12","license":[{"start":{"date-parts":[[2022,9,8]],"date-time":"2022-09-08T00:00:00Z","timestamp":1662595200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,9,8]],"date-time":"2022-09-08T00:00:00Z","timestamp":1662595200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"TAILOR","award":["952215"],"award-info":[{"award-number":["952215"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mach Learn"],"published-print":{"date-parts":[[2022,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Despite their great success in recent years, neural networks have been found to be vulnerable to adversarial attacks. These attacks are often based on slight perturbations of given inputs that cause them to be misclassified. Several methods have been proposed to formally prove robustness of a given network against such attacks. However, these methods typically give rise to high computational demands, which severely limit their scalability. Recent state-of-the-art approaches state the verification task as a minimisation problem, which is formulated and solved as a mixed-integer linear programming (MIP) problem. We extend this approach by leveraging automated algorithm configuration techniques and, more specifically, construct a portfolio of MIP solver configurations optimised for the neural network verification task. We test this approach on two recent, state-of-the-art MIP-based verification engines, <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathrm {MIPVerify}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>MIPVerify<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathrm {Venus}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>Venus<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, and achieve substantial improvements in CPU time by average factors of up to 4.7 and 10.3, respectively.<\/jats:p>","DOI":"10.1007\/s10994-022-06212-w","type":"journal-article","created":{"date-parts":[[2022,9,8]],"date-time":"2022-09-08T22:03:07Z","timestamp":1662674587000},"page":"4565-4584","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Speeding up neural network robustness verification via algorithm configuration and an optimised mixed integer linear programming solver portfolio"],"prefix":"10.1007","volume":"111","author":[{"given":"Matthias","family":"K\u00f6nig","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Holger H.","family":"Hoos","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan N. van","family":"Rijn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,9,8]]},"reference":[{"key":"6212_CR1","unstructured":"Akintunde, M., Lomuscio, A., Maganti, L., & Pirovano, E. (2018) Reachability analysis for neural agent-environment systems. In Proceedings of The Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR2018)"},{"key":"6212_CR2","unstructured":"Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A., & Criminisi, A. (2016). Measuring neural net robustness with constraints. In Proceedings of the 30th Conference on Neural Information Processing Systems (NeurIPS 2016), pp 2613\u20132621"},{"issue":"3","key":"6212_CR3","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/TEVC.2015.2474158","volume":"20","author":"LC Bezerra","year":"2015","unstructured":"Bezerra, L. C., L\u00f3pez-Ib\u00e1nez, M., & St\u00fctzle, T. (2015). Automatic component-wise design of multiobjective evolutionary algorithms. IEEE Transactions on Evolutionary Computation, 20(3), 403\u2013417.","journal-title":"IEEE Transactions on Evolutionary Computation"},{"key":"6212_CR4","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 Proceedings of The Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI20) (pp.\u00a03291\u20133299)","DOI":"10.1609\/aaai.v34i04.5729"},{"issue":"1","key":"6212_CR5","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1010933404324","volume":"45","author":"L Breiman","year":"2001","unstructured":"Breiman, L. (2001). Random forests. Machine Learning, 45(1), 5\u201332.","journal-title":"Machine Learning"},{"key":"6212_CR6","unstructured":"Bunel, R .R ., Turkaslan, I., Torr, P., Kohli, P., & Mudigonda, P. K. (2018). A unified view of piecewise linear neural network verification. In Proceedings of the 32nd Conference on Neural Information Processing Systems (NeurIPS 2018), pp.\u00a04790\u20134799"},{"key":"6212_CR7","doi-asserted-by":"crossref","unstructured":"Carlini, N., & Wagner, D. (2017). Towards evaluating the robustness of neural networks. In Proceedings of the 38th IEEE Symposium on Security and Privacy (IEEE S &P 2017), pp.\u00a039\u201357","DOI":"10.1109\/SP.2017.49"},{"key":"6212_CR8","unstructured":"Carlini, N., Katz, G., Barrett, C., & Dill, D. L. (2017) Provably Minimally-Distorted Adversarial Examples. arXiv preprint arXiv:1709.10207"},{"key":"6212_CR9","doi-asserted-by":"crossref","unstructured":"Chen, P. Y., Sharma, Y., Zhang, H., Yi, J., & Hsieh, C. J. (2018). Ead: Elastic-net attacks to deep neural networks via adversarial examples. In Proceedings of The Thirty-Second AAAI Conference on Artificial Intelligence (AAAI18)","DOI":"10.1609\/aaai.v32i1.11302"},{"key":"6212_CR10","doi-asserted-by":"crossref","unstructured":"Cheng, C. H., N\u00fchrenberg, G., & Ruess , H. (2017). Maximum resilience of artificial neural networks. In Proceedings of The 15th International Symposium on Automated Technology for Verification and Analysis (ATVA2017), pp.\u00a0251\u2013268.","DOI":"10.1007\/978-3-319-68167-2_18"},{"key":"6212_CR11","unstructured":"Chiarandini, M., Fawcett, C., & Hoos, H. H. (2008). A Modular Multiphase Heuristic Solver for Post Enrolment Course Timetabling. In Proceedings of the 7th International Conference on the Practice and Theory of Automated Timetabling (PATAT 2008)."},{"key":"6212_CR12","unstructured":"Cohen, J., Rosenfeld, E., & Kolter, Z. (2019). Certified adversarial robustness via randomized smoothing. In Proceedings of the Thirty-Sixth International Conference on Machine Learning (ICML2019), pp 1310\u20131320."},{"key":"6212_CR13","doi-asserted-by":"crossref","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., & Tiwari, A. (2018) Output range analysis for deep neural networks. In Proceedings of The Tenth NASA Formal Methods Symposium (NFM 2018), pp.\u00a0121\u2013138.","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"6212_CR14","unstructured":"Dvijotham, K., Stanforth, R., Gowal, S., Mann, T. A., & Kohli, P. (2018). A Dual Approach to Scalable Verification of Deep Networks. In Proceedings of the 38th Conference on Uncertainty in Artificial Intelligence (UAI 2018), pp.\u00a0550\u2013559."},{"key":"6212_CR15","doi-asserted-by":"crossref","unstructured":"Ehlers, R. (2017). Formal verification of piece-wise linear feed-forward neural networks. In Proceedings of the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA 2017), pp.\u00a0269\u2013286.","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"6212_CR16","doi-asserted-by":"crossref","unstructured":"Feurer, M., Springenberg, J. T., & Hutter, F. (2015). Initializing Bayesian hyperparameter optimization via meta-learning. In Proceedings of The Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI15)","DOI":"10.1609\/aaai.v29i1.9354"},{"issue":"3","key":"6212_CR17","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.","journal-title":"Constraints"},{"key":"6212_CR18","doi-asserted-by":"crossref","unstructured":"Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T., Schneider, M. T., & Ziller, S. (2011). A portfolio solver for answer set programming: Preliminary report. In Proceedings of The Tenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR2019), pp.\u00a0352\u2013357.","DOI":"10.1007\/978-3-642-20895-9_40"},{"key":"6212_CR19","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., & Vechev, M. (2018). AI2: Safety and robustness certification of neural networks with abstract interpretation. In Proceedings of the 39th IEEE Symposium on Security and Privacy (IEEE S &P 2018), pp.\u00a03\u201318.","DOI":"10.1109\/SP.2018.00058"},{"key":"6212_CR20","unstructured":"Goodfellow, I. J., Shlens, J., & Szegedy, C. (2014). Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.6572"},{"key":"6212_CR21","doi-asserted-by":"crossref","unstructured":"Hutter, F., Babic, D., Hoos, H. H., & Hu, A. J. (2007). Boosting verification by automatic tuning of decision procedures. In Formal Methods in Computer Aided Design (FMCAD\u201907), pp.\u00a027\u201334","DOI":"10.1109\/FAMCAD.2007.9"},{"key":"6212_CR22","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1613\/jair.2861","volume":"36","author":"F Hutter","year":"2009","unstructured":"Hutter, F., Hoos, H. H., Leyton-Brown, K., & St\u00fctzle, T. (2009). ParamILS: An automatic algorithm configuration framework. Journal of Artificial Intelligence Research, 36, 267\u2013306.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"6212_CR23","doi-asserted-by":"crossref","unstructured":"Hutter, F., Hoos, H. H., & Leyton-Brown, K. (2010). Automated Configuration of Mixed Integer Programming Solvers. In Proceedings of the 7th International Conference on Integration of Artificial Intelligence (AI) and Operations Research (OR) Techniques in Constraint Programming (CPAIOR 2010), pp.\u00a0186\u2013202","DOI":"10.1007\/978-3-642-13520-0_23"},{"key":"6212_CR24","doi-asserted-by":"crossref","unstructured":"Hutter, F., Hoos, H. H., Leyton-Brown, K. (2011). Sequential model-based optimization for general algorithm configuration. In Proceedings of the 5th International Conference on Learning and Intelligent Optimization (LION 5), pp.\u00a0507\u2013523","DOI":"10.1007\/978-3-642-25566-3_40"},{"key":"6212_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2016.09.006","volume":"243","author":"F Hutter","year":"2017","unstructured":"Hutter, F., Lindauer, M., Balint, A., Bayless, S., Hoos, H., & Leyton-Brown, K. (2017). The configurable SAT solver challenge (CSSC). Artificial Intelligence, 243, 1\u201325.","journal-title":"Artificial Intelligence"},{"key":"6212_CR26","doi-asserted-by":"crossref","unstructured":"Julian, K. D., Lopez, J., Brush, J. S., Owen, M. P., & Kochenderfer, M. J. (2016). Policy compression for aircraft collision avoidance systems. In Proceedings of the Thirty-Fifth Digital Avionics Systems Conference (DASC2016), pp.\u00a01\u201310","DOI":"10.1109\/DASC.2016.7778091"},{"key":"6212_CR27","doi-asserted-by":"crossref","unstructured":"Kadioglu, S., Malitsky, Y., Sabharwal, A., Samulowitz, H., & Sellmann, M. (2011). Algorithm selection and scheduling. In Proceedings of the Seventeenth International Conference on Principles and Practice of Constraint Programming (CP2011), pp.\u00a0454\u2013469","DOI":"10.1007\/978-3-642-23786-7_35"},{"key":"6212_CR28","unstructured":"Kashgarani, H., & Kotthoff, L. (2021). Is algorithm selection worth it? Comparing selecting single algorithms and parallel execution. In AAAI Workshop on Meta-Learning and MetaDL Challenge, pp.\u00a058\u201364."},{"key":"6212_CR29","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 Proceedings of the 29th International Conference on Computer Aided Verification(CAV 2017), pp.\u00a097\u2013117","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"6212_CR30","unstructured":"K\u00f6nig, M., Hoos, H. H., van Rijn, J. N. (2021). Speeding up neural network verification via automated algorithm configuration. In ICLR Workshop on Security and Safety in Machine Learning Systems."},{"key":"6212_CR31","doi-asserted-by":"crossref","unstructured":"Kotthoff, L. (2016). Algorithm selection for combinatorial search problems: A survey. In Data Mining and Constraint Programming. Springer, pp.\u00a0149\u2013190.","DOI":"10.1007\/978-3-319-50137-6_7"},{"key":"6212_CR32","unstructured":"Kurakin, A., Goodfellow, I., & Bengio, S. (2016). Adversarial examples in the physical world. arXiv preprint arXiv:1607.02533"},{"key":"6212_CR33","doi-asserted-by":"crossref","unstructured":"Lecuyer, M., Atlidakis, V., Geambasu, R., Hsu, D., & Jana S (2019) Certified robustness to adversarial examples with differential privacy. In Proceedings of The Fortieth IEEE Symposium on Security and Privacy (SP2019), IEEE, pp 656\u2013672.","DOI":"10.1109\/SP.2019.00044"},{"key":"6212_CR34","doi-asserted-by":"publisher","first-page":"745","DOI":"10.1613\/jair.4726","volume":"53","author":"M Lindauer","year":"2015","unstructured":"Lindauer, M., Hoos, H. H., Hutter, F., & Schaub, T. (2015). AutoFolio: An automatically configured algorithm selector. Journal of Artificial Intelligence Research, 53, 745\u2013778.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"6212_CR35","unstructured":"Lomuscio, A., & Maganti, L. (2017). An approach to reachability analysis for feed-forward ReLU neural networks. arXiv preprint arXiv:1706.07351"},{"issue":"3","key":"6212_CR36","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1016\/j.ejor.2013.10.043","volume":"235","author":"M Lopez-Ibanez","year":"2014","unstructured":"Lopez-Ibanez, M., & St\u00fctzle, T. (2014). Automatically improving the anytime behaviour of optimisation algorithms. European Journal of Operational Research, 235(3), 569\u2013582.","journal-title":"European Journal of Operational Research"},{"key":"6212_CR37","doi-asserted-by":"crossref","unstructured":"Malitsky, Y., Sabharwal, A., Samulowitz, H., & Sellmann, M. (2012). Parallel SAT Solver Selection and Scheduling. In Proceedings of the Eighteenth International Conference on Principles and Practice of Constraint Programming (CP2012), pp.\u00a0512\u2013526","DOI":"10.1007\/978-3-642-33558-7_38"},{"key":"6212_CR38","unstructured":"Mohapatra, J., Ko, C. Y., Weng, L., Chen, P. Y., Liu, S., & Daniel, L. (2021). Hidden cost of randomized smoothing. In Proceedings of The 24th International Conference on Artificial Intelligence and Statistics (AISTATS2021), pp 4033\u20134041."},{"key":"6212_CR39","doi-asserted-by":"crossref","unstructured":"Papernot, N., McDaniel, P., Wu, X., Jha, S., & Swami, A. (2016). Distillation as a defense to adversarial perturbations against deep neural networks. In Proceedings of the 37th IEEE Symposium on Security and Privacy (IEEE S &P 2016), pp. 582\u2013597.","DOI":"10.1109\/SP.2016.41"},{"key":"6212_CR40","unstructured":"Raghunathan, A., Steinhardt, J., & Liang, P. (2018). Certified defenses against adversarial examples. arXiv preprint arXiv:1801.09344"},{"key":"6212_CR41","unstructured":"Scheibler, K., Winterer, L., Wimmer, R., & Becker, B. (2015). Towards verification of artificial neural networks. In Proceedings of the 18th Workshop on Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV 2015), pp. 30\u201340."},{"key":"6212_CR42","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., \\& Fergus, R. (2014). Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199"},{"key":"6212_CR43","doi-asserted-by":"crossref","unstructured":"Thornton, C., Hutter, F., Hoos, H. H., \\& Leyton-Brown, K. (2013). Auto-WEKA: Combined selection and hyperparameter optimization of classification algorithms. In Proceedings of the 19th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining (KDD2013), pp. 847\u2013855","DOI":"10.1145\/2487575.2487629"},{"key":"6212_CR44","unstructured":"Tjeng, V., Xiao, .K, & Tedrake, R. (2019). Evaluating robustness of neural networks with mixed integer programming. In Proceedings of the 7th International Conference on Learning Representations (ICLR 2019)"},{"key":"6212_CR45","doi-asserted-by":"crossref","unstructured":"Vallati, M., Fawcett, C., Gerevini, A. E., Hoos, H., \\& Saetti, A. (2013). Automatic generation of efficient domain-specific planners from generic parametrized planners. In Proceedings of the 6th Annual Symposium on Combinatorial Search (SOCS), pp. 184\u2013192.","DOI":"10.1609\/socs.v4i1.18293"},{"key":"6212_CR46","unstructured":"Wong, E., & Kolter, Z. (2018.) Provable defenses against adversarial examples via the convex outer adversarial polytope. In Proceedings of The Thirty-Fifth International Conference on Machine Learning (ICML2018), pp 5286\u20135295."},{"issue":"11","key":"6212_CR47","doi-asserted-by":"publisher","first-page":"5777","DOI":"10.1109\/TNNLS.2018.2808470","volume":"29","author":"W Xiang","year":"2018","unstructured":"Xiang, W., Tran, H. D., & Johnson, T. T. (2018). Output Reachable Set Estimation and Verification for Multilayer Neural Networks. IEEE Transactions on Neural Networks and Learning Systems, 29(11), 5777\u20135783.","journal-title":"IEEE Transactions on Neural Networks and Learning Systems"},{"key":"6212_CR48","doi-asserted-by":"crossref","unstructured":"Xu L, Hoos H, Leyton-Brown K (2010) Hydra: Automatically Configuring Algorithms for Portfolio-Based Selection. In: Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence (AAAI10)","DOI":"10.1609\/aaai.v24i1.7565"},{"key":"6212_CR49","unstructured":"Xu, L., Hutter, F., Hoos, H. H., Leyton-Brown, K. (2011). Hydra-MIP: Automated algorithm configuration and selection for mixed integer programming. In RCRA Workshop on Experimental evaluation of Algorithms for Solving Problems with Combinatorial Explosion, pp. 16\u201330"}],"container-title":["Machine Learning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10994-022-06212-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10994-022-06212-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10994-022-06212-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,29]],"date-time":"2022-11-29T22:28:08Z","timestamp":1669760888000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10994-022-06212-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,8]]},"references-count":49,"journal-issue":{"issue":"12","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["6212"],"URL":"https:\/\/doi.org\/10.1007\/s10994-022-06212-w","relation":{},"ISSN":["0885-6125","1573-0565"],"issn-type":[{"value":"0885-6125","type":"print"},{"value":"1573-0565","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,9,8]]},"assertion":[{"value":"14 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 April 2022","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 June 2022","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 September 2022","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"All authors certify that they have no affiliations with or involvement in any organization or entity with any financial interest or non-financial interest in the subject matter or materials discussed in this manuscript.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}},{"value":"All authors declare that there is no recent, present, or anticipated employment by any organization that may gain or lose financially through publication of this manuscript.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Employment"}},{"value":"Not applicable: this research did not involve human participants, nor did it involve animals.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Research involving human participants"}},{"value":"Not applicable: this research does not involve personal data, and publishing of this manuscript will not result in the disruption of any individual\u2019s privacy.","order":5,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent for publication"}}]}}