Cited By
View all- Aichernig BHavelund K(2023)AI-Assisted Programming with Test-Based RefinementBridging the Gap Between AI and Reality10.1007/978-3-031-73741-1_24(385-411)Online publication date: 23-Oct-2023
What, Indeed, is an Achievable Provable Guarantee for Learning-Enabled Safety-Critical Systems
Authors: 
Saddek Bensalem, Chih-Hong Cheng, Wei Huang, Xiaowei Huang, Changshun Wu, Xingyu ZhaoAuthors Info & Claims
Pages 55 - 76
Abstract
Machine learning has made remarkable advancements, but confidently utilising learning-enabled components in safety-critical domains still poses challenges. Among the challenges, it is known that a rigorous, yet practical, way of achieving safety guarantees is one of the most prominent. In this paper, we first discuss the engineering and research challenges associated with the design and verification of such systems. Then, based on the observation that existing works cannot actually achieve provable guarantees, we promote a two-step verification method for the ultimate achievement of provable statistical guarantees.
References
[1]
Kulstad, M., Carlin, L.: Leibniz’s philosophy of mind (1997)
[2]
Gunning D, Stefik M, Choi J, Miller T, Stumpf S, and Yang G-Z Xai-explainable artificial intelligence Sci. Rob. 2019 4 37 eaay7120
[3]
Lapuschkin S, Wäldchen S, Binder A, Montavon G, Samek W, and Müller K-R Unmasking clever hans predictors and assessing what machines really learn Nat. Commun. 2019 10 1 1096
[4]
Confalonieri R, Coba L, Wagner B, and Besold TR A historical perspective of explainable artificial intelligence Wiley Interdisc. Rev. Data Min. Knowl. Disc. 2021 11 1
[5]
Došilović, F.K., Brčić, M., Hlupić, N., Explainable artificial intelligence: a survey. In: 41st International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO), vol. 2018, pp. 0210–0215. IEEE (2018)
[6]
Huang X, Kwiatkowska M, Wang S, and Wu M Majumdar R and Kunčak V Safety verification of deep neural networks Computer Aided Verification 2017 Cham Springer 3-29
[7]
Dreossi T et al. Dillig I, Tasiran S, et al. VerifAI: a toolkit for the formal design and analysis of artificial intelligence-based systems Computer Aided Verification 2019 Cham Springer 432-442
[8]
Wu M, Wicker M, Ruan W, Huang X, and Kwiatkowska M A game-based approximate verification of deep neural networks with provable guarantees Theor. Comput. Sci. 2020 807 298-329
[9]
Liu C et al. Algorithms for verifying deep neural networks Found. Trends® Optim. 2021 4 3–4 244-404
[10]
Seshia SA, Sadigh D, and Sastry SS Toward verified artificial intelligence Commun. ACM 2022 65 7 46-55
[11]
Huang C, Hu Z, Huang X, and Pei K Farkaš I, Masulli P, Otte S, and Wermter S Statistical certification of acceptable robustness for neural networks Artificial Neural Networks and Machine Learning – ICANN 2021 2021 Cham Springer 79-90
[12]
Zhang T, Ruan W, and Fieldsend JE Amini MR, Canu S, Fischer A, Guns T, Kralj Novak P, and Tsoumakas G Proa: a probabilistic robustness assessment against functional perturbations Joint European Conference on Machine Learning and Knowledge Discovery in Databases 2022 Heidelberg Springer 154-170
[13]
Shafaei S, Kugele S, Osman MH, and Knoll A Gallina B, Skavhaug A, Schoitsch E, and Bitsch F Uncertainty in machine learning: a safety perspective on autonomous driving Computer Safety, Reliability, and Security 2018 Cham Springer 458-464
[14]
Gawlikowski, J., et al.: A survey of uncertainty in deep neural networks. arXiv preprint arXiv:2107.03342 (2021)
[15]
Hüllermeier E and Waegeman W Aleatoric and epistemic uncertainty in machine learning: an introduction to concepts and methods Mach. Learn. 2021 110 457-506
[16]
Gruber, C., Schenk, P.O., Schierholz, M., Kreuter, F., Kauermann, G.: Sources of uncertainty in machine learning - a statisticians’ view. arXiv:2305.16703 (2023)
[17]
Cheng, C.-H., Nührenberg, G., Yasuoka, H.: Runtime monitoring neuron activation patterns. In: Design, Automation & Test in Europe Conference & Exhibition (DATE), vol. 2019, pp. 300–303. IEEE (2019)
[18]
Henzinger, T.A., Lukina, A., Schilling, C.: Outside the box: abstraction-based monitoring of neural networks. In: ECAI 2020, pp. 2433–2440. IOS Press (2020)
[19]
Cheng, C.-H.: Provably-robust runtime monitoring of neuron activation patterns. In: Design, Automation & Test in Europe Conference & Exhibition (DATE), vol. 2021, pp. 1310–1313. IEEE (2021)
[20]
Lukina A, Schilling C, and Henzinger TA Feng L and Fisman D Into the unknown: active monitoring of neural networks Runtime Verification 2021 Cham Springer 42-61
[21]
Cheng C-H, Wu C, Seferis E, and Bensalem S Bouajjani A, Holik L, and Wu Z Prioritizing corners in OoD detectors via symbolic string manipulation International Symposium on Automated Technology for Verification and Analysis 2022 Heidelberg Springer 397-413
[22]
Fremont, D.J., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: a language for scenario specification and scene generation. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 63–78 (2019)
[23]
Zhong S et al. Machine learning: new ideas and tools in environmental science and engineering Environ. Sci. Technol. 2021 55 19 12741-12754
[24]
Brunton, S.L., Kutz, J.N.: Data-driven Science and Engineering: Machine Learning, Dynamical Systems, and Control. Cambridge University Press, Cambridge (2019)
[25]
Zelaya, C.V.G.: Towards explaining the effects of data preprocessing on machine learning. In: IEEE 35th International Conference on Data Engineering (ICDE), vol. 2019, pp. 2086–2090. IEEE (2019)
[26]
Roh Y, Heo G, and Whang SE A survey on data collection for machine learning: a big data-AI integration perspective IEEE Trans. Knowl. Data Eng. 2019 33 4 1328-1347
[27]
Bensalem, S., et al.: Formal specification for learning-enabled autonomous systems. In: FoMLAS2022 (2022)
[28]
Musa JD Operational profiles in software-reliability engineering IEEE Softw. 1993 10 2 14-32
[29]
Fukunaga K Introduction to Statistical Pattern Recognition 2013 Amsterdam Elsevier
[30]
Nakkiran, P., Kaplun, G., Bansal, Y., Yang, T., Barak, B., Sutskever, I.: Deep double descent: where bigger models and more data hurt. In: International Conference on Learning Representations (2020)
[31]
Li J, Liu J, Yang P, Chen L, Huang X, and Zhang L Chang B-YE Analyzing deep neural networks with symbolic propagation: towards higher precision and faster verification Static Analysis 2019 Cham Springer 296-319
[32]
Li, R., et al.: Prodeep: a platform for robustness verification of deep neural networks. In: Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2020, pp. 1630–1634. ACM, New York (2020)
[33]
Yang P et al. Enhancing robustness verification for deep neural networks via symbolic propagation Form. Asp. Comput. 2021 33 3 407-435
[34]
Ruan, W., Huang, X., Kwiatkowska, M.: Reachability analysis of deep neural networks with provable guarantees. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI-18, pp. 2651–2659 (2018)
[35]
Ruan, W., Wu, M., Sun, Y., Huang, X., Kroening, D., Kwiatkowska, M.: Global robustness evaluation of deep neural networks with provable guarantees for the hamming distance. In: Proceedings of the 28th International Joint Conference on Artificial Intelligence, IJCAI-19, pp. 5944–5952 (2019)
[36]
Xu, P., Ruan, W., Huang, X.: Quantifying safety risks of deep neural networks. In: Complex & Intelligent Systems (2022)
[37]
Belkin M, Hsu D, Ma S, and Mandal S Reconciling modern machine-learning practice and the classical bias-variance trade-off Proc. Natl. Acad. Sci. 2019 116 32 15849-15854
[38]
Huang, X., et al.: A survey of safety and trustworthiness of large language models through the lens of verification and validation. arXiv:2305.11391 (2023)
[39]
Littlewood B and Rushby J Reasoning about the reliability of diverse two-channel systems in which one channel is “possibly perfect” IEEE Trans. Softw. Eng. 2012 38 5 1178-1194
[40]
Rushby, J.: Software verification and system assurance. In: 7th International Conference on Software Engineering and Formal Methods, pp. 3–10. IEEE, Hanoi (2009)
[41]
Zhao X, Littlewood B, Povyakalo A, Strigini L, and Wright D Modeling the probability of failure on demand (pfd) of a 1-out-of-2 system in which one channel is “quasi-perfect” Reliabil. Eng. Syst. Safety 2017 158 230-245
[42]
Huang, W., Zhao, X., Jin, G., Huang, X.: Safari: versatile and efficient evaluations for robustness of interpretability. In: International Conference on Computer Vision (ICCV 2023) (2023)
[43]
Dutle, A., et al.: Pressburger, from requirements to autonomous flight: an overview of the monitoring ICAROUS project. In: Proceedings of 2nd Workshop on Formal Methods for Autonomous Systems, vol. 329 of EPTCS, pp. 23–30 (2020)
[44]
Balakrishnan, A., et al.: Specifying and evaluating quality metrics for vision-based perception systems. In: Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 1433–1438 (2019).
[45]
Balakrishnan A, Deshmukh J, Hoxha B, Yamaguchi T, and Fainekos G Feng L and Fisman D PerceMon: online monitoring for perception systems Runtime Verification 2021 Cham Springer 297-308
[46]
Dong Y et al. Reliability assessment and safety arguments for machine learning components in system assurance ACM Trans. Embedded Comput. Syst. 2023 22 3 1-48
[47]
Huang X, Ruan W, Tang Q, and Zhao X Riesco A and Zhang M Bridging formal methods and machine learning with global optimisation Formal Methods and Software Engineering 2022 Cham Springer 1-19
[48]
Zhao X et al. Casimiro A, Ortmeier F, Bitsch F, Ferreira P, et al. A safety framework for critical systems utilising deep neural networks Computer Safety, Reliability, and Security 2020 Cham Springer 244-259
[49]
Katz G, Barrett C, Dill DL, Julian K, and Kochenderfer MJ Majumdar R and Kunčak V Reluplex: an efficient SMT solver for verifying deep neural networks Computer Aided Verification 2017 Cham Springer 97-117
[50]
Ehlers R D’Souza D and Narayan Kumar K Formal verification of piece-wise linear feed-forward neural networks Automated Technology for Verification and Analysis 2017 Cham Springer 269-286
[51]
Narodytska, N.: Formal analysis of deep binarized neural networks. In: IJCAI, pp. 5692–5696 (2018)
[52]
Narodytska, N., Kasiviswanathan, S., Ryzhyk, L., Sagiv, M., Walsh, T.: Verifying properties of binarized deep neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 32 (2018)
[53]
Cheng C-H, Nührenberg G, Huang C-H, and Ruess H Piskac R and Rümmer P Verification of binarized neural networks via inter-neuron factoring Verified Software. Theories, Tools, and Experiments 2018 Cham Springer 279-290
[54]
Cheng C-H, Nührenberg G, and Ruess H D’Souza D and Narayan Kumar K Maximum resilience of artificial neural networks Automated Technology for Verification and Analysis 2017 Cham Springer 251-268
[55]
Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351 (2017)
[56]
Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: Ai2: safety and robustness certification of neural networks with abstract interpretation. In: IEEE Symposium on Security and Privacy (SP), vol. 2018, pp. 3–18. IEEE (2018)
[57]
Mirman, M., Gehr, T., Vechev, M.: Differentiable abstract interpretation for provably robust neural networks. In: International Conference on Machine Learning, pp. 3575–3583 (2018)
[58]
Wong, E., Kolter, Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: International Conference on Machine Learning, pp. 5283–5292 (2018)
[59]
Dvijotham, K., Stanforth, R., Gowal, S., Mann, T.A., Kohli, P.: A dual approach to scalable verification of deep networks. In: UAI, vol. 1, p. 3 (2018)
[60]
Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: 27th USENIX Security Symposium (USENIX Security 2018), pp. 1599–1614 (2018)
[61]
Peck, J., Roels, J., Goossens, B., Saeys, Y.: Lower bounds on the robustness to adversarial perturbations. Adv. Neural Inf. Process. Syst. 30 (2017)
[62]
Neumaier A and Shcherbina O Safe bounds in linear and mixed-integer linear programming Math. Program. 2004 99 283-296
[63]
Ruan, W., Huang, X., Kwiatkowska, M.: Reachability analysis of deep neural networks with provable guarantees. arXiv preprint arXiv:1805.02242 (2018)
[64]
Weng, T.-W., et al.: Evaluating the robustness of neural networks: an extreme value theory approach. In: ICLR 2018 (2018)
[65]
Webb, S., Rainforth, T., Teh, Y.W., Kumar, M.P.: A statistical approach to assessing neural network robustness. In: International Conference on Learning Representations (2018)
[66]
Wang, B., Webb, S., Rainforth, T.: Statistically robust neural network classification. In: Uncertainty in Artificial Intelligence, pp. 1735–1745. PMLR (2021)
[67]
Zhao, X., et al.: Assessing the reliability of deep learning classifiers through robustness evaluation and operational profiles. In: Workshop on AI Safety at IJCAI-21 (2021)
[68]
Pei, K., Cao, Y., Yang, J., Jana, S.: Deepxplore: automated whitebox testing of deep learning systems. In: proceedings of the 26th Symposium on Operating Systems Principles, pp. 1–18 (2017)
[69]
Ma, L., et al.: DeepGauge: comprehensive and multi-granularity testing criteria for gauging the robustness of deep learning systems. In: 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE) (2018)
[70]
Sun, Y., Wu, M., Ruan, W., Huang, X., Kwiatkowska, M., Kroening, D.: Deepconcolic: testing and debugging deep neural networks. In: ICSE 2019 (2019)
[71]
Du, X., Xie, X., Li, Y., Ma, L., Liu, Y., Zhao, J.: Deepstellar: model-based quantitative analysis of stateful deep learning systems. In: Proceedings of the 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 477–487 (2019)
[72]
Huang W et al. Coverage-guided testing for recurrent neural networks IEEE Trans. Reliab. 2021 71 3 1191-1206
[73]
Berend, D.: Distribution awareness for AI system testing. In: 2021 IEEE/ACM 43rd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), pp. 96–98. IEEE (2021)
[74]
Dola, S., Dwyer, M.B., Soffa, M.L.: Distribution-aware testing of neural networks using generative models. In: 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE), pp. 226–237. IEEE (2021)
[75]
Byun, T., Vijayakumar, A., Rayadurgam, S., Cofer, D.: Manifold-based test generation for image classifiers. In: IEEE International Conference on Artificial Intelligence Testing (AITest), vol. 2020, pp. 15–22. IEEE (2020)
[76]
Toledo, F., Shriver, D., Elbaum, S., Dwyer, M.B.: Distribution models for falsification and verification of dnns. In: 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 317–329. IEEE (2021)
[77]
Huang, W., Zhao, X., Banks, A., Cox, V., Huang, X.: Hierarchical distribution-aware testing of deep learning. arXiv preprint arXiv:2205.08589 (2022)
Index Terms
- What, Indeed, is an Achievable Provable Guarantee for Learning-Enabled Safety-Critical Systems
Index terms have been assigned to the content through auto-classification.
Recommendations
Integrated safety analysis of software-controlled critical systems
Software for safety-critical systems must deal with the hazards identified by safety analysis in order to make the system safe, risk-free and fail-safe. Certain faults in critical systems can result in catastrophic consequences such as death, injury or ...
How do practitioners perceive assurance cases in safety-critical software systems?
CHASE '18: Proceedings of the 11th International Workshop on Cooperative and Human Aspects of Software EngineeringSafety-critical software systems are those whose failure or malfunction could result in casualty and/or serious financial loss. In such systems, safety assurance cases (SACs) are an emerging approach that adopts a proactive strategy to produce ...
Modeling of Safety-Critical Systems Using Petri Nets
Safety plays a crucial role in the development of complex computer systems in the relevant areas like railway transport, process industry, power plants, etc. In the design phase of safety-critical systems, various methods are used to make the system ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 14 December 2023
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 16 Nov 2024
Other Metrics
Citations
Cited By
View all- Aichernig BHavelund K(2023)AI-Assisted Programming with Test-Based RefinementBridging the Gap Between AI and Reality10.1007/978-3-031-73741-1_24(385-411)Online publication date: 23-Oct-2023
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in