{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:33:23Z","timestamp":1781238803340,"version":"3.54.1"},"reference-count":179,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T00:00:00Z","timestamp":1722643200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T00:00:00Z","timestamp":1722643200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100019521","name":"Clore Israel Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100019521","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["683\/18"],"award-info":[{"award-number":["683\/18"]}],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["683\/18"],"award-info":[{"award-number":["683\/18"]}],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["683\/18"],"award-info":[{"award-number":["683\/18"]}],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003816","name":"Huawei Technologies","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003816","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003483","name":"Hebrew University of Jerusalem","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100003483","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Deep neural networks (DNNs) play a crucial role in the field of machine learning, demonstrating state-of-the-art performance across various application domains. However, despite their success, DNN-based models may occasionally exhibit challenges with<jats:italic>generalization<\/jats:italic>, i.e., may fail to handle inputs that were not encountered during training. This limitation is a significant challenge when it comes to deploying deep learning for safety-critical tasks, as well as in real-world settings characterized by substantial variability. We introduce a novel approach for harnessing DNN verification technology to identify DNN-driven decision rules that exhibit robust generalization to previously unencountered input domains. Our method assesses generalization within an input domain by measuring the level of agreement between<jats:italic>independently trained<\/jats:italic>deep neural networks for inputs in this domain. We also efficiently realize our approach by using off-the-shelf DNN verification engines, and extensively evaluate it on both supervised and unsupervised DNN benchmarks, including a deep reinforcement learning (DRL) system for Internet congestion control\u2014demonstrating the applicability of our approach for real-world settings. Moreover, our research introduces a fresh objective for formal verification, offering the prospect of mitigating the challenges linked to deploying DNN-driven systems in real-world scenarios.<\/jats:p>","DOI":"10.1007\/s10817-024-09704-7","type":"journal-article","created":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T16:02:04Z","timestamp":1722700924000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Verifying the Generalization of Deep Learning to Out-of-Distribution Domains"],"prefix":"10.1007","volume":"68","author":[{"given":"Guy","family":"Amir","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Osher","family":"Maayan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tom","family":"Zelazny","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guy","family":"Katz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Schapira","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,8,3]]},"reference":[{"key":"9704_CR1","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/j.inffus.2021.05.008","volume":"76","author":"M Abdar","year":"2021","unstructured":"Abdar, M., Pourpanah, F., Hussain, S., Rezazadegan, D., Liu, L., Ghavamzadeh, M., Fieguth, P., Cao, X., Khosravi, A., Acharya, U., Makarenkov, V., Nahavandi, S.: A review of uncertainty quantification in deep learning: techniques, applications and challenges. Inf. Fusion 76, 243\u2013297 (2021)","journal-title":"Inf. Fusion"},{"key":"9704_CR2","unstructured":"Achiam, J., Held, D., Tamar, A., Abbeel, P.: Constrained policy optimization. In: Proc. 34th Int. Conf. on Machine Learning (ICML), pp. 22\u201331 (2017)"},{"key":"9704_CR3","unstructured":"Alamdari, P., Avni, G., Henzinger, T., Lukina, A.: Formal methods with a touch of magic. In: Proc. 20th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 138\u2013147 (2020)"},{"key":"9704_CR4","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A.: Introduction to Neural Network Verification. verifieddeeplearning.com (2021)","DOI":"10.1561\/9781680839111"},{"issue":"22","key":"9704_CR5","doi-asserted-by":"publisher","first-page":"4862","DOI":"10.1093\/bioinformatics\/btz422","volume":"35","author":"M AlQuraishi","year":"2019","unstructured":"AlQuraishi, M.: AlphaFold at CASP13. Bioinformatics 35(22), 4862\u20134865 (2019)","journal-title":"Bioinformatics"},{"key":"9704_CR6","doi-asserted-by":"crossref","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: Proc. of the 32nd AAAI Conference on Artificial Intelligence, pp. 2669\u20132678 (2018)","DOI":"10.1609\/aaai.v32i1.11797"},{"key":"9704_CR7","doi-asserted-by":"crossref","unstructured":"Amir, G., Corsi, D., Yerushalmi, R., Marzari, L., Harel, D., Farinelli, A., Katz, G.: Verifying learning-based robotic navigation systems. In: Proc. 29th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 607\u2013627 (2023)","DOI":"10.1007\/978-3-031-30823-9_31"},{"key":"9704_CR8","doi-asserted-by":"crossref","unstructured":"Amir, G., Freund, Z., Katz, G., Mandelbaum, E., Refaeli, I.: veriFIRE: verifying an industrial, learning-based wildfire detection system. In: Proc. 25th Int. Symposium on Formal Methods (FM), pp. 648\u2013656 (2023)","DOI":"10.1007\/978-3-031-27481-7_38"},{"key":"9704_CR9","doi-asserted-by":"crossref","unstructured":"Amir, G., Maayan, O., Zelazny, T., Katz, G., Schapira, M.: Verifying generalization in deep learning. In: Proc. 35th Int. Conf. on Computer Aided Verification (CAV), pp. 438\u2013455 (2023)","DOI":"10.1007\/978-3-031-37703-7_21"},{"key":"9704_CR10","doi-asserted-by":"crossref","unstructured":"Amir, G., Maayan, O., Zelazny, T., Katz, G., Schapira, M.: Verifying the generalization of deep learning to out-of-distribution domains: Artifact. https:\/\/zenodo.org\/records\/10448320 (2024)","DOI":"10.1007\/s10817-024-09704-7"},{"key":"9704_CR11","unstructured":"Amir, G., Schapira, M., Katz, G.: Towards scalable verification of deep reinforcement learning. In: Proc. 21st Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 193\u2013203 (2021)"},{"key":"9704_CR12","doi-asserted-by":"crossref","unstructured":"Amir, G., Wu, H., Barrett, C., Katz, G.: An SMT-based approach for verifying binarized neural networks. In: Proc. 27th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 203\u2013222 (2021)","DOI":"10.1007\/978-3-030-72013-1_11"},{"key":"9704_CR13","unstructured":"Amir, G., Zelazny, T., Katz, G., Schapira, M.: Verification-aided deep ensemble selection. In: Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 27\u201337 (2022)"},{"key":"9704_CR14","doi-asserted-by":"crossref","unstructured":"Anderson, G., Pailoor, S., Dillig, I., Chaudhuri, S.: Optimization and abstraction: a synergistic approach for analyzing neural network robustness. In: Proc. 40th ACM SIGPLAN Conf. on Programming Languages Design and Implementations (PLDI), pp. 731\u2013744 (2019)","DOI":"10.1145\/3314221.3314614"},{"key":"9704_CR15","doi-asserted-by":"crossref","unstructured":"Ashok, P., Hashemi, V., Kretinsky, J., Mohr, S.: DeepAbstract: neural network abstraction for accelerating verification. In: Proc. 18th Int. Symp. on Automated Technology for Verification and Analysis (ATVA), pp. 92\u2013107 (2020)","DOI":"10.1007\/978-3-030-59152-6_5"},{"key":"9704_CR16","doi-asserted-by":"crossref","unstructured":"Avni, G., Bloem, R., Chatterjee, K., Henzinger, T., K\u00f6nighofer, B., Pranger, S.: Run-time optimization for learned controllers through quantitative games. In: Proc. 31st Int. Conf. on Computer Aided Verification (CAV), pp. 630\u2013649 (2019)","DOI":"10.1007\/978-3-030-25540-4_36"},{"key":"9704_CR17","doi-asserted-by":"crossref","unstructured":"Bacci, E., Giacobbe, M., Parker, D.: Verifying reinforcement learning up to infinity. In: Proc. 30th Int. Joint Conf. on Artificial Intelligence (IJCAI) (2021)","DOI":"10.24963\/ijcai.2021\/297"},{"key":"9704_CR18","unstructured":"Baena-Garc\u0131a, M., Campo-\u00c1vila, J., Fidalgo, R., Bifet, A., Gavalda, R., Morales-Bueno, R.: Early drift detection method. In: Proc. 4th Int. Workshop on Knowledge Discovery from Data Streams, vol. 6, pp. 77\u201386 (2006)"},{"key":"9704_CR19","doi-asserted-by":"crossref","unstructured":"Bagnall, A., Stewart, G.: Certifying the true error: machine learning in Coq with verified generalization guarantees. In: Proc. 33th AAAI Conf. on Artificial Intelligence (AAAI), pp. 2662\u20132669 (2019)","DOI":"10.1609\/aaai.v33i01.33012662"},{"key":"9704_CR20","doi-asserted-by":"crossref","unstructured":"Baluta, T., Shen, S., Shinde, S., Meel, K., Saxena, P.: Quantitative verification of neural networks and its security applications. In: Proc. ACM SIGSAC Conf. on Computer and Communications Security (CCS), pp. 1249\u20131264 (2019)","DOI":"10.1145\/3319535.3354245"},{"key":"9704_CR21","doi-asserted-by":"crossref","unstructured":"Barto, A., Sutton, R., Anderson, C.: Neuronlike adaptive elements that can solve difficult learning control problems. In: Proc. of IEEE Systems Man and Cybernetics Conference (SMC), pp. 834\u2013846 (1983)","DOI":"10.1109\/TSMC.1983.6313077"},{"key":"9704_CR22","unstructured":"Bassan, S., Amir, G., Corsi, D., Refaeli, I., Katz, G.: Formally explaining neural networks within reactive systems. In: Proc. 23rd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 10\u201322 (2023)"},{"key":"9704_CR23","doi-asserted-by":"crossref","unstructured":"Bassan, S., Katz, G.: Towards formal approximated minimal explanations of neural networks. In: Proc. 29th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 187\u2013207 (2023)","DOI":"10.1007\/978-3-031-30823-9_10"},{"key":"9704_CR24","doi-asserted-by":"crossref","unstructured":"Benussi, E., Patane, A., Wicker, M., Laurenti, L., Kwiatkowska, M.: Individual fairness guarantees for neural networks. In: Proc. 31st Int. Joint Conf. on Artificial Intelligence (IJCAI) (2022)","DOI":"10.24963\/ijcai.2022\/92"},{"key":"9704_CR25","doi-asserted-by":"crossref","unstructured":"Bloem, R., K\u00f6nighofer, B., K\u00f6nighofer, R., Wang, C.: Shield synthesis: - runtime enforcement for reactive systems. In: Proc. of the 21st Int. Conf. in Tools and Algorithms for the Construction and Analysis of Systems, (TACAS), vol. 9035, pp. 533\u2013548 (2022)","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"9704_CR26","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.: End to end learning for self-driving cars. Technical report. arXiv:1604.07316 (2016)"},{"key":"9704_CR27","unstructured":"Brockman, G., Cheung, V., Pettersson, L., Schneider, J., Schulman, J., Tang, J., Zaremba, W.: OpenAI Gym. Technical report. arXiv:1606.01540 (2016)"},{"key":"9704_CR28","unstructured":"Bunel, R., Turkaslan, I., Torr, P., Kohli, P., Mudigonda, P.: A Unified view of piecewise linear neural network verification. In: Proc. 32nd Conf. on Neural Information Processing Systems (NeurIPS), pp. 4795\u20134804 (2018)"},{"key":"9704_CR29","doi-asserted-by":"crossref","unstructured":"Casadio, M., Komendantskaya, E., Daggitt, M., Kokke, W., Katz, G., Amir, G., Refaeli, I.: Neural network robustness as a verification property: a principled case study. In: Proc. 34th Int. Conf. on Computer Aided Verification (CAV), pp. 219\u2013231 (2022)","DOI":"10.1007\/978-3-031-13185-1_11"},{"key":"9704_CR30","unstructured":"Chen, W., Xu, Y., Wu, X.: Deep reinforcement learning for multi-resource multi-machine job scheduling. Technical report. arXiv:1711.07440 (2017)"},{"key":"9704_CR31","doi-asserted-by":"crossref","unstructured":"Choi, W., Finkbeiner, B., Piskac, R., Santolucito, M.: Can reactive synthesis and syntax-guided synthesis be friends? In: Proc. of the 43rd ACM SIGPLAN Int. Conf. on Programming Language Design and Implementation (PLDI), pp. 229\u2013243 (2022)","DOI":"10.1145\/3519939.3523429"},{"key":"9704_CR32","unstructured":"Cisse, M., Bojanowski, P., Grave, E., Dauphin, Y., Usunier, N.: Parseval networks: improving robustness to adversarial examples. In: Proc. 34th Int. Conf. on Machine Learning (ICML), pp. 854\u2013863 (2017)"},{"key":"9704_CR33","unstructured":"Cohen, E., Elboher, Y., Barrett, C., Katz, G.: Tighter abstract queries in neural network verification. In: Proc. 24th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) (2023)"},{"key":"9704_CR34","unstructured":"Cohen, J., Rosenfeld, E., Kolter, Z.: Certified adversarial robustness via randomized smoothing. In: Proc. 36th Int. Conf. on Machine Learning (ICML), pp. 1310\u20131320 (2019)"},{"key":"9704_CR35","first-page":"2493","volume":"12","author":"R Collobert","year":"2011","unstructured":"Collobert, R., Weston, J., Bottou, L., Karlen, M., Kavukcuoglu, K., Kuksa, P.: Natural language processing (Almost) from scratch. J. Mach. Learn. Res. 12, 2493\u20132537 (2011)","journal-title":"J. Mach. Learn. Res."},{"key":"9704_CR36","unstructured":"Corsi, D., Amir, G., Katz, G., Farinelli, A.: Analyzing adversarial inputs in deep reinforcement learning. Technical report. arXiv:2402.05284 (2024)"},{"key":"9704_CR37","unstructured":"Corsi, D., Marchesini, E., Farinelli, A.: Formal verification of neural networks for safety-critical tasks in deep reinforcement learning. In: Proc. 37th Conf. on Uncertainty in Artificial Intelligence (UAI), pp. 333\u2013343 (2021)"},{"key":"9704_CR38","unstructured":"Corsi, D., Yerushalmi, R., Amir, G., Farinelli, A., Harel, D., Katz, G.: Constrained reinforcement learning for robotics via scenario-based programming. Technical report. arXiv:2206.09603 (2022)"},{"key":"9704_CR39","doi-asserted-by":"crossref","unstructured":"Dietterich, T.: Ensemble methods in machine learning. In: Proc. 1st Int. Workshop on Multiple Classifier Systems (MCS), pp. 1\u201315 (2020)","DOI":"10.1007\/3-540-45014-9_1"},{"key":"9704_CR40","doi-asserted-by":"crossref","unstructured":"Dong, G., Sun, J., Wang, J., Wang, X., Dai, T.: Towards repairing neural networks correctly. Technical report. arXiv:2012.01872 (2020)","DOI":"10.1109\/QRS54544.2021.00081"},{"key":"9704_CR41","doi-asserted-by":"crossref","unstructured":"Dutta, S., Chen, X., Sankaranarayanan, S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: Proc. 22nd ACM Int. Conf. on Hybrid Systems: Computation and Control (HSCC), pp. 157\u2013168 (2019)","DOI":"10.1145\/3302504.3311807"},{"issue":"16","key":"9704_CR42","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/j.ifacol.2018.08.026","volume":"51","author":"S Dutta","year":"2018","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Learning and verification of feedback control systems using feedforward neural networks. IFAC-PapersOnLine 51(16), 151\u2013156 (2018)","journal-title":"IFAC-PapersOnLine"},{"key":"9704_CR43","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: Proc. 15th Int. Symp. on Automated Technology for Verification and Analysis (ATVA), pp. 269\u2013286 (2017)","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"9704_CR44","doi-asserted-by":"crossref","unstructured":"Elboher, Y., Cohen, E., Katz, G.: Neural network verification using residual reasoning. In: Proc. 20th Int. Conf. on Software Engineering and Formal Methods (SEFM), pp. 173\u2013189 (2022)","DOI":"10.1007\/978-3-031-17108-6_11"},{"key":"9704_CR45","doi-asserted-by":"crossref","unstructured":"Elboher, Y., Gottschlich, J., Katz, G.: An abstraction-based framework for neural network verification. In: Proc. 32nd Int. Conf. on Computer Aided Verification (CAV), pp. 43\u201365 (2020)","DOI":"10.1007\/978-3-030-53288-8_3"},{"key":"9704_CR46","doi-asserted-by":"crossref","unstructured":"Eliyahu, T., Kazak, Y., Katz, G., Schapira, M.: Verifying learning-augmented systems. In: Proc. Conf. of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication (SIGCOMM), pp. 305\u2013318 (2021)","DOI":"10.1145\/3452296.3472936"},{"issue":"3","key":"9704_CR47","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/s10009-011-0196-8","volume":"14","author":"Y Falcone","year":"2012","unstructured":"Falcone, Y., Fernandez, J., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transf. 14(3), 349\u2013382 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9704_CR48","doi-asserted-by":"crossref","unstructured":"Fawaz, H., Forestier, G., Weber, J., Idoumghar, L., Muller, P.-A.: Adversarial attacks on deep neural networks for time series classification. In: Proc. Int. Joint Conf. on Neural Networks (IJCNN), pp. 1\u20138 (2019)","DOI":"10.1109\/IJCNN48605.2020.9206721"},{"key":"9704_CR49","doi-asserted-by":"crossref","unstructured":"Fields, T., Hsieh, G., Chenou, J.: Mitigating drift in time series data with noise augmentation. In: Proc. Int. Conf. on Computational Science and Computational Intelligence (CSCI), pp. 227\u2013230 (2019)","DOI":"10.1109\/CSCI49370.2019.00046"},{"key":"9704_CR50","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Heim, P., Passing, N.: Temporal Stream Logic Modulo Theories. In: Proc of the 25th Int. Conf. on Foundations of Software Science and Computation Structures, (FOSSACS 2022). LNCS, vol. 13242, pp. 325\u2013346 (2022)","DOI":"10.1007\/978-3-030-99253-8_17"},{"key":"9704_CR51","doi-asserted-by":"crossref","unstructured":"Fulton, N., Platzer, A.: Safe reinforcement learning via formal methods: toward safe control through proof and learning. In: Proc. 32nd AAAI Conf. on Artificial Intelligence (AAAI) (2018)","DOI":"10.1609\/aaai.v32i1.12107"},{"key":"9704_CR52","doi-asserted-by":"publisher","DOI":"10.1016\/j.engappai.2022.105151","volume":"115","author":"M Ganaie","year":"2022","unstructured":"Ganaie, M., Hu, M., Malik, A., Tanveer, M., Suganthan, P.: Ensemble deep learning: a review. Eng. Appl. Artif. Intell. 115, 105151 (2022)","journal-title":"Eng. Appl. Artif. Intell."},{"issue":"1","key":"9704_CR53","first-page":"2096","volume":"17","author":"Y Ganin","year":"2016","unstructured":"Ganin, Y., Ustinova, E., Ajakan, H., Germain, P., Larochelle, H., Laviolette, F., Marchand, M., Lempitsky, V.: Domain-adversarial training of neural networks. J. Mach. Learn. Res. 17(1), 2096\u20132030 (2016)","journal-title":"J. Mach. Learn. Res."},{"issue":"1","key":"9704_CR54","first-page":"1437","volume":"16","author":"J Garc\u0131a","year":"2015","unstructured":"Garc\u0131a, J., Fern\u00e1ndez, F.: A comprehensive survey on safe reinforcement learning. J. Mach. Learn. Res. 16(1), 1437\u20131480 (2015)","journal-title":"J. Mach. Learn. Res."},{"key":"9704_CR55","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, E., Chaudhuri, S., Vechev, M.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: Proc. 39th IEEE Symposium on Security and Privacy (S &P) (2018)","DOI":"10.1109\/SP.2018.00058"},{"issue":"6","key":"9704_CR56","doi-asserted-by":"publisher","first-page":"1381","DOI":"10.1002\/widm.1381","volume":"10","author":"R Gemaque","year":"2020","unstructured":"Gemaque, R., Costa, A., Giusti, R., Dos Santos, E.: An overview of unsupervised drift detection methods. Wiley Interdiscip. Rev. Data Min. Knowl. Discov. 10(6), 1381 (2020)","journal-title":"Wiley Interdiscip. Rev. Data Min. Knowl. Discov."},{"key":"9704_CR57","unstructured":"Geng, C., Le, N., Xu, X., Wang, Z., Gurfinkel, A., Si, X.: Toward reliable neural specifications. Technical report. arXiv:2210.16114 (2022)"},{"issue":"5","key":"9704_CR58","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/37.236324","volume":"13","author":"S Geva","year":"1993","unstructured":"Geva, S., Sitte, J.: A Cartpole Experiment Benchmark for Trainable Controllers. IEEE Control Syst. Magaz. 13(5), 40\u201351 (1993)","journal-title":"IEEE Control Syst. Magaz."},{"key":"9704_CR59","doi-asserted-by":"crossref","unstructured":"Goldberger, B., Adi, Y., Keshet, J., Katz, G.: Minimal modifications of deep neural networks using verification. In: Proc. 23rd Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pp. 260\u2013278 (2020)","DOI":"10.29007\/699q"},{"key":"9704_CR60","unstructured":"Goodfellow, I., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. Technical report. arXiv:1412.6572 (2014)"},{"key":"9704_CR61","volume-title":"Deep Learning","author":"I Goodfellow","year":"2016","unstructured":"Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning. MIT Press, Cambridge, MA (2016)"},{"key":"9704_CR62","doi-asserted-by":"crossref","unstructured":"Gopinath, D., Katz, G., P\u01ces\u01cereanu, C., Barrett, C.: DeepSafe: a data-driven approach for assessing robustness of neural networks. In: Proc. 16th. Int. Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 3\u201319 (2018)","DOI":"10.1007\/978-3-030-01090-4_1"},{"key":"9704_CR63","doi-asserted-by":"crossref","unstructured":"Goubault, E., Palumby, S., Putot, S., Rustenholz, L., Sankaranarayanan, S.: Static analysis of ReLU neural networks with tropical polyhedra. In: Proc. 28th Int. Symposium on Static Analysis (SAS), pp. 166\u2013190 (2021)","DOI":"10.1007\/978-3-030-88806-0_8"},{"key":"9704_CR64","doi-asserted-by":"crossref","unstructured":"Gu, X., Easwaran, A.: Towards safe machine learning for CPS: infer uncertainty from training data. In: Proc. of the 10th ACM\/IEEE Int. Conf. on Cyber-Physical Systems (ICCPS), pp. 249\u2013258 (2019)","DOI":"10.1145\/3302509.3311038"},{"key":"9704_CR65","unstructured":"Haarnoja, T., Zhou, A., Abbeel, P., Levine, S.: Soft actor-critic: off-policy maximum entropy deep reinforcement learning with a stochastic actor. In: Int. Conf. on Machine Learning, pp. 1861\u20131870 (2018). PMLR"},{"key":"9704_CR66","unstructured":"Han, B., Yao, Q., Yu, X., Niu, G., Xu, M., Hu, W., Tsang, I., Sugiyama, M.: Co-teaching: robust training of deep neural networks with extremely noisy labels. Technical report. arXiv:1804.06872 (2018)"},{"key":"9704_CR67","doi-asserted-by":"crossref","unstructured":"Hashemi, V., K\u0159et\u00ednsky, J., Rieder, S., Schmidt, J.: Runtime monitoring for out-of-distribution detection in object detection neural networks. Technical report. arXiv:2212.07773 (2022)","DOI":"10.1007\/978-3-031-27481-7_36"},{"key":"9704_CR68","doi-asserted-by":"crossref","unstructured":"Hasselt, H., Guez, A., Silver, D.: Deep reinforcement learning with double Q-learning. In: Proc. 30th AAAI Conf. on Artificial Intelligence (AAAI) (2016)","DOI":"10.1609\/aaai.v30i1.10295"},{"key":"9704_CR69","doi-asserted-by":"crossref","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Proc. 29th Int. Conf. on Computer Aided Verification (CAV), pp. 3\u201329 (2017)","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"9704_CR70","unstructured":"Huang, S., Papernot, N., Goodfellow, I., Duan, Y., Abbeel, P.: Adversarial attacks on neural network policies. Technical report. arXiv:1702.02284 (2017)"},{"key":"9704_CR71","unstructured":"Isac, O., Barrett, C., Zhang, M., Katz, G.: Neural network verification with proof production. In: Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 38\u201348 (2022)"},{"key":"9704_CR72","doi-asserted-by":"crossref","unstructured":"Jacoby, Y., Barrett, C., Katz, G.: Verifying recurrent neural networks using invariant inference. In: Proc. 18th Int. Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 57\u201374 (2020)","DOI":"10.1007\/978-3-030-59152-6_3"},{"key":"9704_CR73","unstructured":"Jay, N., Rotman, N., Godfrey, B., Schapira, M., Tamar, A.: A deep reinforcement learning perspective on internet congestion control. In: Proc. 36th Int. Conf. on Machine Learning (ICML), pp. 3050\u20133059 (2019)"},{"key":"9704_CR74","doi-asserted-by":"crossref","unstructured":"Julian, K., Lopez, J., Brush, J., Owen, M., Kochenderfer, M.: Policy compression for aircraft collision avoidance systems. In: Proc. 35th Digital Avionics Systems Conf. (DASC), pp. 1\u201310 (2016)","DOI":"10.1109\/DASC.2016.7778091"},{"key":"9704_CR75","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: a calculus for reasoning about deep neural networks. Formal Methods in System Design (FMSD) (2021)","DOI":"10.1007\/s10703-021-00363-7"},{"key":"9704_CR76","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Proc. 29th Int. Conf. on Computer Aided Verification (CAV), pp. 97\u2013117 (2017)","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"9704_CR77","doi-asserted-by":"crossref","unstructured":"Katz, G., Huang, D., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zelji\u0107, A., Dill, D., Kochenderfer, M., Barrett, C.: The marabou framework for verification and analysis of deep neural networks. In: Proc. 31st Int. Conf. on Computer Aided Verification (CAV), pp. 443\u2013452 (2019)","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"9704_CR78","unstructured":"Khaki, S., Aditya, A., Karnin, Z., Ma, L., Pan, O., Chandrashekar, S.: Uncovering drift in textual data: an unsupervised method for detecting and mitigating drift in machine learning models (2023)"},{"key":"9704_CR79","unstructured":"Kingma, D., Ba, J.: Adam: A method for stochastic optimization . In: Proc. 3rd Int. Conf. on Learning Representations (ICLR) (2015)"},{"key":"9704_CR80","doi-asserted-by":"crossref","unstructured":"K\u00f6nighofer, B., Lorber, F., Jansen, N., Bloem, R.: Shield synthesis for reinforcement learning. In: Proc. Int. Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), pp. 290\u2013306 (2020)","DOI":"10.1007\/978-3-030-61362-4_16"},{"key":"9704_CR81","unstructured":"Krizhevsky, A., Sutskever, I., Hinton, G.: Imagenet classification with deep convolutional neural networks. In: Proc. 26th Conf. on Neural Information Processing Systems (NeurIPS), pp. 1097\u20131105 (2012)"},{"key":"9704_CR82","doi-asserted-by":"crossref","unstructured":"Krogh, A., Vedelsby, J.: Neural network ensembles, cross validation, and active learning. In: Proc. 7th Conf. on Neural Information Processing Systems (NeurIPS), pp. 231\u2013238 (1994)","DOI":"10.3233\/AIC-1994-73-412"},{"key":"9704_CR83","unstructured":"Kuper, L., Katz, G., Gottschlich, J., Julian, K., Barrett, C., Kochenderfer, M.: Toward scalable verification for safety-critical deep networks. Technical report. arXiv:1801.05950 (2018)"},{"key":"9704_CR84","unstructured":"Kurakin, A., Goodfellow, I., Bengio, S.: Adversarial examples in the physical world. Technical report. arXiv:1607.02533 (2016)"},{"key":"9704_CR85","unstructured":"Lakshminarayanan, B., Pritzel, A., Blundell, C.: Simple and scalable predictive uncertainty estimation using deep ensembles. In: Proc. 30th Conf. on Neural Information Processing Systems (NeurIPS) (2017)"},{"key":"9704_CR86","doi-asserted-by":"crossref","unstructured":"Lekharu, A., Moulii, K.Y., Sur, A., Sarkar, A.: Deep learning based prediction model for adaptive video streaming. In: Proc. 12th Int. Conf. on Communication Systems & Networks (COMSNETS), pp. 152\u2013159 (2020). IEEE","DOI":"10.1109\/COMSNETS48256.2020.9027383"},{"key":"9704_CR87","unstructured":"Li, Y.: Deep reinforcement learning: An Overview. Technical report. arXiv:1701.07274 (2017)"},{"issue":"3","key":"9704_CR88","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1109\/TNSE.2018.2835758","volume":"6","author":"W Li","year":"2018","unstructured":"Li, W., Zhou, F., Chowdhury, K.R., Meleis, W.: QTCP: adaptive congestion control with reinforcement learning. IEEE Trans. Netw. Sci. Eng. 6(3), 445\u2013458 (2018)","journal-title":"IEEE Trans. Netw. Sci. Eng."},{"issue":"3","key":"9704_CR89","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/1455526.1455532","volume":"12","author":"J Ligatti","year":"2009","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur. 12(3), 19\u201311941 (2009)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"9704_CR90","doi-asserted-by":"crossref","unstructured":"Liu, Y., Ding, J., Liu, X.: Ipo: Interior-point policy optimization under constraints. In: Proc. 34th AAAI Conf. on Artificial Intelligence (AAAI), pp. 4940\u20134947 (2020)","DOI":"10.1609\/aaai.v34i04.5932"},{"key":"9704_CR91","unstructured":"Liu, H., Long, M., Wang, J., Jordan, M.: Transferable adversarial training: a general approach to adapting deep classifiers. In: Proc. 36th Int. Conf. on Machine Learning (ICML), pp. 4013\u20134022 (2019)"},{"key":"9704_CR92","doi-asserted-by":"crossref","unstructured":"Liu, X., Xu, H., Liao, W., Yu, W.: Reinforcement learning for cyber-physical systems. In: Proc. IEEE Int. Conf. on Industrial Internet (ICII), pp. 318\u2013327 (2019)","DOI":"10.1109\/ICII.2019.00063"},{"key":"9704_CR93","unstructured":"Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward ReLU neural networks. Technical report. arXiv:1706.07351 (2017)"},{"key":"9704_CR94","doi-asserted-by":"crossref","unstructured":"Loquercio, A., Segu, M., Scaramuzza, D.: A general framework for uncertainty estimation in deep learning. In: Proc. Int. Conf. on Robotics and Automation (ICRA), pp. 3153\u20133160 (2020)","DOI":"10.1109\/LRA.2020.2974682"},{"issue":"1","key":"9704_CR95","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1109\/37.980245","volume":"22","author":"S Low","year":"2002","unstructured":"Low, S., Paganini, F., Doyle, J.: Internet congestion control. IEEE Control Syst. Magaz. 22(1), 28\u201343 (2002)","journal-title":"IEEE Control Syst. Magaz."},{"key":"9704_CR96","doi-asserted-by":"crossref","unstructured":"Lukina, A., Schilling, C., Henzinger, T.: Into the unknown: active monitoring of neural networks. In: Proc. 21st Int. Conf. on Runtime Verification (RV), pp. 42\u201361 (2021)","DOI":"10.1007\/978-3-030-88494-9_3"},{"key":"9704_CR97","doi-asserted-by":"crossref","unstructured":"Lyu, Z., Ko, C.Y., Kong, Z., Wong, N., Lin, D., Daniel, L.: Fastened crown: tightened neural network robustness certificates. In: Proc. 34th AAAI Conf. on Artificial Intelligence (AAAI), pp. 5037\u20135044 (2020)","DOI":"10.1609\/aaai.v34i04.5944"},{"key":"9704_CR98","unstructured":"Ma, J., Ding, S., Mei, Q.: Towards more practical adversarial attacks on graph neural networks. In: Proc. 34th Conf. on Neural Information Processing Systems (NeurIPS) (2020)"},{"key":"9704_CR99","unstructured":"Maderbacher, B., Bloem, R.: Reactive synthesis modulo theories using abstraction refinement. In: Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 315\u2013324 (2022)"},{"key":"9704_CR100","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. Technical report. arXiv:1706.06083 (2017)"},{"key":"9704_CR101","unstructured":"Madsen, A., Johansen, A.: Neural arithmetic units. In: Proc. 8th Int. Conf. on Learning Representations (ICLR) (2020)"},{"key":"9704_CR102","unstructured":"Mallick, A., Hsieh, K., Arzani, B., Joshi, G.: Matchmaker: Data drift mitigation in machine learning for large-scale systems. In: Proc. of Machine Learning and Systems (MLSys), pp. 77\u201394 (2022)"},{"key":"9704_CR103","doi-asserted-by":"crossref","unstructured":"Mammadli, R., Jannesari, A., Wolf, F.: Static neural compiler optimization via deep reinforcement learning. In: Proc. 6th IEEE\/ACM Workshop on the LLVM Compiler Infrastructure in HPC (LLVM-HPC) and Workshop on Hierarchical Parallelism for Exascale Computing (HiPar), pp. 1\u201311 (2020)","DOI":"10.1109\/LLVMHPCHiPar51896.2020.00006"},{"key":"9704_CR104","unstructured":"Mandal, U., Amir, G., Wu, H., Daukantas, I., Newell, F., Ravaioli, U., Meng, B., Durling, M., Ganai, M., Shim, T., Katz, G., Barrett, C.: Formally verifying deep reinforcement learning controllers with lyapunov barrier certificates. Technical report. arXiv:2405.14058 (2024)"},{"key":"9704_CR105","doi-asserted-by":"crossref","unstructured":"Mao, H., Alizadeh, M., Menache, I., Kandula, S.: Resource management with deep reinforcement learning. In: Proc. 15th ACM Workshop on Hot Topics in Networks (HotNets), pp. 50\u201356 (2016)","DOI":"10.1145\/3005745.3005750"},{"key":"9704_CR106","doi-asserted-by":"crossref","unstructured":"Mao, H., Netravali, R., Alizadeh, M.: Neural adaptive video streaming with pensieve. In: Proc. Conf. of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication (SIGCOMM), pp. 197\u2013210 (2017)","DOI":"10.1145\/3098822.3098843"},{"key":"9704_CR107","unstructured":"Mnih, V., Kavukcuoglu, K., Silver, D., Graves, A., Antonoglou, I., Wierstra, D., Riedmiller, M.: Playing atari with deep reinforcement learning. Technical report. arXiv:1312.5602 (2013)"},{"key":"9704_CR108","unstructured":"Moore, A.: Efficient memory-based learning for robot control. University of Cambridge (1990)"},{"key":"9704_CR109","doi-asserted-by":"crossref","unstructured":"Moosavi-Dezfooli, M.D., Fawzi, A., Frossard, P.: DeepFool: a simple and accurate method to fool deep neural networks. In: Proc. IEEE Conf. on Computer Vision and Pattern Recognition (CVPR) (2016)","DOI":"10.1109\/CVPR.2016.282"},{"issue":"4","key":"9704_CR110","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/1024908.1024910","volume":"14","author":"J Nagle","year":"1984","unstructured":"Nagle, J.: Congestion control in IP\/TCP internetworks. ACM SIGCOMM Comput. Commun. Rev. 14(4), 11\u201317 (1984)","journal-title":"ACM SIGCOMM Comput. Commun. Rev."},{"key":"9704_CR111","doi-asserted-by":"crossref","unstructured":"Okudono, T., Waga, M., Sekiyama, T., Hasuo, I.: Weighted automata extraction from recurrent neural networks via regression on state spaces. In: Proc. 34th AAAI Conf. on Artificial Intelligence (AAAI), pp. 5037\u20135044 (2020)","DOI":"10.1609\/aaai.v34i04.5977"},{"key":"9704_CR112","unstructured":"Ortega, L., Caba\u00f1as, R., Masegosa, A.: Diversity and generalization in neural network ensembles. In: Proc. 25th Int. Conf. on Artificial Intelligence and Statistics (AISTATS), pp. 11720\u201311743 (2022)"},{"key":"9704_CR113","unstructured":"Osband, I., Aslanides, J., Cassirer, A.: Randomized prior functions for deep reinforcement learning. In: Proc. 31st Int. Conf. on Neural Information Processing Systems (NeurIPS), pp. 8617\u20138629 (2018)"},{"key":"9704_CR114","doi-asserted-by":"crossref","unstructured":"Ostrovsky, M., Barrett, C., Katz, G.: An abstraction-refinement approach to verifying convolutional neural networks. In: Proc. 20th. Int. Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 391\u2013396 (2022)","DOI":"10.1007\/978-3-031-19992-9_25"},{"key":"9704_CR115","unstructured":"Ovadia, Y., Fertig, E., Ren, J., Nado, Z., Sculley, D., Nowozin, S., Dillon, J., Lakshminarayanan, B., Snoek, J.: Can you trust your model\u2019s uncertainty? evaluating predictive uncertainty under dataset shift. In: Proc. 33rd Conf. on Neural Information Processing Systems (NeurIPS), pp. 14003\u201314014 (2019)"},{"key":"9704_CR116","unstructured":"Packer, C., Gao, K., Kos, J., Kr\u00e4henb\u00fchl, P., Koltun, V., Song, D.: Assessing generalization in deep reinforcement learning. Technical report. arXiv:1810.12282 (2018)"},{"key":"9704_CR117","doi-asserted-by":"crossref","unstructured":"Papernot, N., McDaniel, P., Goodfellow, I., Jha, S., Celik, Z., Swami, A.: Practical black-box attacks against machine learning. In: Proc. ACM on Asia Conf. on Computer and Communications Security (CCS, pp. 506\u2013519 (2017)","DOI":"10.1145\/3052973.3053009"},{"key":"9704_CR118","doi-asserted-by":"crossref","unstructured":"Papernot, N., McDaniel, P., Jha, S., Fredrikson, M., Celik, Z., Swami, A.: The limitations of deep learning in adversarial settings. In: IEEE European Symposium on Security and Privacy (EuroS &P), pp. 372\u2013387 (2016)","DOI":"10.1109\/EuroSP.2016.36"},{"key":"9704_CR119","doi-asserted-by":"publisher","first-page":"579","DOI":"10.3390\/make2040031","volume":"2","author":"A Pereira","year":"2020","unstructured":"Pereira, A., Thomas, C.: Challenges of machine learning applied to Safety-critical cyber-physical systems. Mach. Learn. Knowl. Extract. 2, 579\u2013602 (2020)","journal-title":"Mach. Learn. Knowl. Extract."},{"key":"9704_CR120","unstructured":"Polgreen, E., Abboud, R., Kroening, D.: Counterexample guided neural synthesis. Technical report. arXiv:2001.09245 (2020)"},{"key":"9704_CR121","unstructured":"Prabhakar, P., Afzal, Z.: Abstraction based output range analysis for neural networks. Technical report. arXiv:2007.09527 (2020)"},{"key":"9704_CR122","doi-asserted-by":"crossref","unstructured":"Prabhakar, P.: Bisimulations for neural network reduction. In: Proc. 23rd Int. Conf. Verification on Model Checking, and Abstract Interpretation (VMCAI), pp. 285\u2013300 (2022)","DOI":"10.1007\/978-3-030-94583-1_14"},{"key":"9704_CR123","doi-asserted-by":"crossref","unstructured":"Pranger, S., K\u00f6nighofer, B., Posch, L., Bloem, R.: TEMPEST - synthesis tool for reactive systems and shields in probabilistic environments. In: Proc. 19th Int. Symposium in Automated Technology for Verification and Analysis, (ATVA), vol. 12971, pp. 222\u2013228 (2021)","DOI":"10.1007\/978-3-030-88885-5_15"},{"key":"9704_CR124","doi-asserted-by":"crossref","unstructured":"Pranger, S., K\u00f6nighofer, B., Tappler, M., Deixelberger, M., Jansen, N., Bloem, R.: Adaptive shielding under uncertainty. In: American Control Conference, (ACC), pp. 3467\u20133474 (2021)","DOI":"10.23919\/ACC50511.2021.9482889"},{"key":"9704_CR125","unstructured":"Qin, C., Martens, J., Gowal, S., Krishnan, D., Dvijotham, K., Fawzi, A., De, S., Stanforth, R., Kohli, P.: Adversarial robustness through local linearization. Technical report. arXiv:1907.02610 (2019)"},{"key":"9704_CR126","first-page":"1","volume":"22","author":"A Raffin","year":"2021","unstructured":"Raffin, A., Hill, A., Gleave, A., Kanervisto, A., Ernestus, M., Dormann, N.: Stable-baselines3: reliable reinforcement learning implementations. J. Mach. Learn. Res. 22, 1\u20138 (2021)","journal-title":"J. Mach. Learn. Res."},{"key":"9704_CR127","unstructured":"Ray, A., Achiam, J., Amodei, D.: Benchmarking safe exploration in deep reinforcement learning. Technical report. https:\/\/cdn.openai.com\/safexp-short.pdf (2019)"},{"key":"9704_CR128","doi-asserted-by":"crossref","unstructured":"Riedmiller, M.: Neural fitted Q iteration \u2014 first experiences with a data efficient neural reinforcement learning method. In: Proc. 16th European Conf. on Machine Learning (ECML), pp. 317\u2013328 (2005)","DOI":"10.1007\/11564096_32"},{"issue":"2","key":"9704_CR129","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1137\/1035044","volume":"35","author":"T Rockafellar","year":"1993","unstructured":"Rockafellar, T.: Lagrange multipliers and optimality. SIAM Rev. 35(2), 183\u2013238 (1993)","journal-title":"SIAM Rev."},{"key":"9704_CR130","unstructured":"Rotman, N., Schapira, M., Tamar, A.: Online safety assurance for deep reinforcement learning. In: Proc. 19th ACM Workshop on Hot Topics in Networks (HotNets), pp. 88\u201395 (2020)"},{"key":"9704_CR131","unstructured":"Roy, J., Girgis, R., Romoff, J., Bacon, P., Pal, C.: Direct behavior specification via constrained reinforcement learning. Technical report. arXiv:2112.12228 (2021)"},{"key":"9704_CR132","doi-asserted-by":"crossref","unstructured":"Ruan, W., Huang, X., Kwiatkowska, M.: Reachability analysis of deep neural networks with provable guarantees. In: Proc. 27th Int. Joint Conf. on Artificial Intelligence (IJCAI) (2018)","DOI":"10.24963\/ijcai.2018\/368"},{"key":"9704_CR133","unstructured":"Ruder, S.: An overview of gradient descent optimization algorithms. Technical report. arXiv:1609.04747 (2016)"},{"issue":"1150","key":"9704_CR134","doi-asserted-by":"publisher","first-page":"20220878","DOI":"10.1259\/bjr.20220878","volume":"96","author":"B Sahiner","year":"2023","unstructured":"Sahiner, B., Chen, W., Samala, R., Petrick, N.: Data drift in medical machine learning: implications and potential remedies. Br. J. Radiol. 96(1150), 20220878 (2023)","journal-title":"Br. J. Radiol."},{"key":"9704_CR135","doi-asserted-by":"crossref","unstructured":"Sargolzaei, A., Crane, C., Abbaspour, A., Noei, S.: A machine learning approach for fault detection in vehicular cyber-physical systems. In: Proc. 15th IEEE Int. Conf. on Machine Learning and Applications (ICMLA), pp. 636\u2013640 (2016)","DOI":"10.1109\/ICMLA.2016.0112"},{"issue":"1","key":"9704_CR136","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F Schneider","year":"2000","unstructured":"Schneider, F.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"9704_CR137","unstructured":"Schulman, J., Wolski, F., Dhariwal, P., Radford, A., Klimov, O.: Proximal policy optimization algorithms. Technical report. arXiv:1707.06347 (2017)"},{"key":"9704_CR138","doi-asserted-by":"crossref","unstructured":"Seshia, S., Desai, A., Dreossi, T., Fremont, D., Ghosh, S., Kim, E., Shivakumar, S., Vazquez-Chanlatte, M., Yue, X.: Formal specification for deep neural networks. In: Proc. 16th Int. Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 20\u201334 (2018)","DOI":"10.1007\/978-3-030-01090-4_2"},{"key":"9704_CR139","unstructured":"Shafahi, A., Najibi, M., Ghiasi, A., Xu, Z., Dickerson, J., Studer, C., Davis, L., Taylor, G., Goldstein, T.: Adversarial training for free! Technical report. arXiv:1904.12843 (2019)"},{"key":"9704_CR140","unstructured":"Shafahi, A., Saadatpanah, P., Zhu, C., Ghiasi, A., Studer, C., Jacobs, D., Goldstein, T.: Adversarially robust transfer learning. Technical report. arXiv:1905.08232 (2019)"},{"issue":"7587","key":"9704_CR141","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1038\/nature16961","volume":"529","author":"D Silver","year":"2016","unstructured":"Silver, D., Huang, A., Maddison, C., Guez, A., Sifre, L., Den Driessche, G., Schrittwieser, J., Antonoglou, I., Panneershelvam, V., Lanctot, M., Dieleman, S.: Mastering the game of go with deep neural networks and tree search. Nature 529(7587), 484\u2013489 (2016)","journal-title":"Nature"},{"key":"9704_CR142","unstructured":"Simonyan, K., Zisserman, A.: Very deep convolutional networks for large-scale image recognition. Technical report. arXiv:1409.1556 (2014)"},{"key":"9704_CR143","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., Puschel, M., Vechev, M.: An abstract domain for certifying neural networks. In: Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) (2019)","DOI":"10.1145\/3290354"},{"key":"9704_CR144","unstructured":"Sotoudeh, M., Thakur, A.: Correcting deep neural networks with small. In: Workshop on Safety and Robustness in Decision Making, Generalizing Patches. (2019)"},{"key":"9704_CR145","unstructured":"Stooke, A., Achiam, J., Abbeel, P.: Responsive safety in reinforcement learning by Pid lagrangian methods. In: Proc. 37th Int. Conf. on Machine Learning (ICML), pp. 9133\u20139143 (2020)"},{"key":"9704_CR146","doi-asserted-by":"crossref","unstructured":"Strong, C., Wu, H., Zelji\u0107, A., Julian, K., Katz, G., Barrett, C., Kochenderfer, M.: Global Optimization of Objective Functions Represented by ReLU Networks. J. Mach. Learn. 1\u201328 (2021)","DOI":"10.1007\/s10994-021-06050-2"},{"key":"9704_CR147","doi-asserted-by":"crossref","unstructured":"Sun, X., Khedr, H., Shoukry, Y.: Formal verification of neural network controlled autonomous systems. In: Proc. 22nd ACM Int. Conf. on Hybrid Systems: Computation and Control (HSCC) (2019)","DOI":"10.1145\/3302504.3311802"},{"key":"9704_CR148","unstructured":"Sutton, R., McAllester, D., Singh, S., Mansour, Y.: Policy gradient methods for reinforcement learning with function approximation. In: Proc. 12th Conf. on Neural Information Processing Systems (NeurIPS) (1999)"},{"key":"9704_CR149","volume-title":"Reinforcement learning: An Introduction","author":"R Sutton","year":"2018","unstructured":"Sutton, R., Barto, A.: Reinforcement learning: An Introduction. MIT Press, Cambridge, MA (2018)"},{"key":"9704_CR150","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks. Technical report. arXiv:1312.6199 (2013)"},{"key":"9704_CR151","unstructured":"Tjeng, V., Xiao, K., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: Proc. 7th Int. Conf. on Learning Representations (ICLR) (2019)"},{"key":"9704_CR152","unstructured":"Tjeng, V., Xiao, K., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: Proc. 7th Int. Conf. on Learning Representations (ICLR) (2019)"},{"key":"9704_CR153","unstructured":"Tolstoy, L.: Anna karenina. The Russian Messenger (1877)"},{"key":"9704_CR154","doi-asserted-by":"crossref","unstructured":"Tran, H., Bak, S., Johnson, T.: Verification of deep convolutional neural networks using imageStars. In: Proc. 32nd Int. Conf. on Computer Aided Verification (CAV), pp. 18\u201342 (2020)","DOI":"10.1007\/978-3-030-53288-8_2"},{"key":"9704_CR155","doi-asserted-by":"crossref","unstructured":"Tran, H., Cai, F., Diego, M., Musau, P., Johnson, T., Koutsoukos, X.: Safety verification of cyber-physical systems with reinforcement learning control. ACM Trans. Embed. Comput. Syst. 18 (2019)","DOI":"10.1145\/3358230"},{"key":"9704_CR156","unstructured":"Trask, A., Hill, F., Reed, S., Rae, J.C.D., Blunsom, P.: Neural arithmetic logic units. In: Proc. 32nd Conf. on Neural Information Processing Systems (NeurIPS) (2018)"},{"key":"9704_CR157","doi-asserted-by":"crossref","unstructured":"Urban, C., Christakis, M., W\u00fcstholz, V., Zhang, F.: Perfectly parallel fairness certification of neural networks. In: Proc. ACM Int. Conf. on Object Oriented Programming Systems Languages and Applications (OOPSLA), pp. 1\u201330 (2020)","DOI":"10.1145\/3428253"},{"key":"9704_CR158","doi-asserted-by":"crossref","unstructured":"Usman, M., Gopinath, D., Sun, Y., Noller, Y., P\u01ces\u01cereanu, C.: NNrepair: Constraint-based repair of neural network classifiers. Technical report. arXiv:2103.12535 (2021)","DOI":"10.1007\/978-3-030-81685-8_1"},{"key":"9704_CR159","doi-asserted-by":"crossref","unstructured":"Valadarsky, A., Schapira, M., Shahaf, D., Tamar, A.: Learning to Route with Deep RL. In: NeurIPS Deep Reinforcement Learning Symposium (2017)","DOI":"10.1145\/3152434.3152441"},{"key":"9704_CR160","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1016\/j.neunet.2022.03.022","volume":"151","author":"M Vasi\u0107","year":"2022","unstructured":"Vasi\u0107, M., Petrovi\u0107, A., Wang, K., Nikoli\u0107, M., Singh, R., Khurshid, S.: Mo\u00cbT: Mixture of expert trees and its application to verifiable reinforcement learning. Neural Netw. 151, 34\u201347 (2022)","journal-title":"Neural Netw."},{"key":"9704_CR161","unstructured":"Wachi, A., Sui, Y.: Safe reinforcement learning in constrained markov decision processes. In: Proc. 37th Int. Conf. on Machine Learning (ICML), pp. 9797\u20139806 (2020)"},{"key":"9704_CR162","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: Proc. 27th USENIX Security Symposium, pp. 1599\u20131614 (2018)"},{"key":"9704_CR163","unstructured":"Weng, T.-W., Zhang, H., Chen, H., Song, Z., Hsieh, C.-J., Boning, D., Dhillon, I., Daniel, L.: Towards fast computation of certified robustness for ReLU networks. Technical report. arXiv:1804.09699 (2018)"},{"key":"9704_CR164","unstructured":"Wong, E., Rice, L., Kolter, Z.: Fast is better than free: revisiting adversarial training. Technical report. arXiv:2001.03994 (2020)"},{"key":"9704_CR165","doi-asserted-by":"crossref","unstructured":"Wu, H., Isac, O., Zelji\u0107, A., Tagomori, T., Daggitt, M., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S.: Marabou 2.0: a versatile formal analyzer of neural networks. In: Proc. 36th Int. Conf. on Computer Aided Verification (CAV) (2024)","DOI":"10.1007\/978-3-031-65630-9_13"},{"key":"9704_CR166","unstructured":"Wu, H., Ozdemir, A., Zelji\u0107, A., Irfan, A., Julian, K., Gopinath, D., Fouladi, S., Katz, G., P\u0103s\u0103reanu, C., Barrett, C.: Parallelization techniques for verifying neural networks. In: Proc. 20th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 128\u2013137 (2020)"},{"key":"9704_CR167","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. Technical report. arXiv:2206.03669 (2022)","DOI":"10.1109\/SaTML54575.2023.00042"},{"key":"9704_CR168","doi-asserted-by":"crossref","unstructured":"Wu, M., Wang, J., Deshmukh, J., Wang, C.: Shield Synthesis for Real: Enforcing safety in cyber-physical systems. In: Proc. 19th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 129\u2013137 (2019)","DOI":"10.23919\/FMCAD.2019.8894264"},{"key":"9704_CR169","doi-asserted-by":"crossref","unstructured":"Wu, H., Zelji\u0107, A., Katz, K., Barrett, C.: Efficient neural network analysis with sum-of-infeasibilities. In: Proc. 28th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 143\u2013163 (2022)","DOI":"10.1007\/978-3-030-99524-9_8"},{"key":"9704_CR170","doi-asserted-by":"crossref","unstructured":"Xiang, W., Tran, H., Johnson, T.: Output reachable set estimation and verification for multi-layer neural networks. IEEE Trans. Neural Netw. Learn. Syst. (TNNLS) (2018)","DOI":"10.1109\/TNNLS.2018.2808470"},{"key":"9704_CR171","doi-asserted-by":"crossref","unstructured":"Yang, X., Yamaguchi, T., Tran, H., Hoxha, B., Johnson, T., Prokhorov, D.: Neural network repair with reachability analysis. In: Proc. 20th Int. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS), pp. 221\u2013236 (2022)","DOI":"10.1007\/978-3-031-15839-1_13"},{"key":"9704_CR172","doi-asserted-by":"publisher","unstructured":"Yang, J., Zeng, X., Zhong, S.g., Wu, S.: Effective neural network ensemble approach for improving generalization performance. IEEE Trans. Neural Netw. Learn. Syst. (TNNLS) 24(6), 878\u2013887 (2013) https:\/\/doi.org\/10.1109\/TNNLS.2013.2246578","DOI":"10.1109\/TNNLS.2013.2246578"},{"key":"9704_CR173","unstructured":"Yu, X., Han, B., Yao, J., Niu, G., Tsang, I., Sugiyama, M.: How does disagreement help generalization against label corruption? In: Proc. 36th Int. Conf. on Machine Learning (ICML), pp. 7164\u20137173 (2019)"},{"key":"9704_CR174","unstructured":"Zelazny, T., Wu, H., Barrett, C., Katz, G.: On reducing over-approximation errors for neural network verification. In: Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 17\u201326 (2022)"},{"key":"9704_CR175","unstructured":"Zhang, J., Kim, J., O\u2019Donoghue, B., Boyd, S.: Sample efficient reinforcement learning with REINFORCE. Technical report. arXiv:2010.11364 (2020)"},{"key":"9704_CR176","doi-asserted-by":"crossref","unstructured":"Zhang, J., Liu, Y., Zhou, K., Li, G., Xiao, Z., Cheng, B., Xing, J., Wang, Y., Cheng, T., Liu, L.: An end-to-end automatic cloud database tuning system using deep reinforcement learning. In: Proc. of the 2019 Int. Conf. on Management of Data (SIGMOD), pp. 415\u2013432 (2019)","DOI":"10.1145\/3299869.3300085"},{"key":"9704_CR177","unstructured":"Zhang, H., Shinn, M., Gupta, A., Gurfinkel, A., Le, N., Narodytska, N.: Verification of recurrent neural networks for cognitive tasks via reachability analysis. In: Proc. 24th European Conf. on Artificial Intelligence (ECAI), pp. 1690\u20131697 (2020)"},{"issue":"12","key":"9704_CR178","doi-asserted-by":"publisher","first-page":"5435","DOI":"10.1109\/TNNLS.2021.3084685","volume":"32","author":"L Zhang","year":"2021","unstructured":"Zhang, L., Zhang, R., Wu, T., Weng, R., Han, M., Zhao, Y.: Safe reinforcement learning with stability guarantee for motion planning of autonomous vehicles. IEEE Trans. Neural Netw. Learn. Syst. 32(12), 5435\u20135444 (2021)","journal-title":"IEEE Trans. Neural Netw. Learn. Syst."},{"key":"9704_CR179","doi-asserted-by":"crossref","unstructured":"Z\u00fcgner, D., Akbarnejad, A., G\u00fcnnemann, S.: Adversarial attacks on neural networks for graph data. In: Proc. 24th ACM SIGKDD Int. Conf. on Knowledge Discovery & Data Mining (KDD), pp. 2847\u20132856 (2018)","DOI":"10.1145\/3219819.3220078"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09704-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09704-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09704-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T22:00:20Z","timestamp":1732572020000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09704-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,3]]},"references-count":179,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,9]]}},"alternative-id":["9704"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09704-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,3]]},"assertion":[{"value":"1 January 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 May 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 August 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"We made use of Large Language Models (LLMs) for assistance in rephrasing certain parts of the text. We do not have further disclosures or declarations.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"17"}}