Tutorial: Neural Network and Autonomous Cyber-Physical Systems Formal Verification for Trustworthy AI and Safe Autonomy
Pages 1 - 2
Abstract
This interactive tutorial describes state-of-the-art methods for formally verifying neural networks and their usage within safety-critical cyber-physical systems (CPS). The inclusion of deep learning models in safety-critical applications requires to formally analyze the behavior of the system, including reasoning about the individual components (e.g., controller robustness), and their interactions and effects in the system as a whole. This tutorial begins with a lecture on this emerging research area, followed by demos of these methods implemented in software tools, specifically the Neural Network Verification (NNV) tool. Examples include systems from aerospace, automotive, and beyond.
References
[1]
Christopher Brix, Mark Niklas Müller, Stanley Bak, Taylor T. Johnson, and Changliu Liu. 2023. First Three Years of the International Verification of Neural Networks Competition (VNN-COMP). arXiv:2301.05815 [cs.LG]
[2]
Arthur Clavière, Laura Altieri Sambartolomé, Eric Asselin, Christophe Garion, and Claire Pagetti. 2022. Verification of Machine Learning Based Cyber-Physical Systems: A Comparative Study. In 25th ACM International Conference on Hybrid Systems: Computation and Control (Milan, Italy) (HSCC '22). Association for Computing Machinery, New York, NY, USA, Article 22, 16 pages.
[3]
Michael Ivashchenko, Sungwoo Choi, Viet-Luan Nguyen, and Hoang-Dung Tran. 2023. Verifying Binary Neural Networks on Continuous Input Space using Star Reachability. In International Conference on Formal Methods in Software Engineering. ACM.
[4]
Diego Manzanas Lopez, Matthias Althoff, Luis Benet, Xin Chen, Jiameng Fan, Marcelo Forets, Chao Huang, Taylor T Johnson, Tobias Ladner, Wenchao Li, Christian Schilling, and Qi Zhu. 2022. ARCH-COMP22 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants. In Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22) (EPiC Series in Computing, Vol. 90), Goran Frehse, Matthias Althoff, Erwin Schoitsch, and Jeremie Guiochet (Eds.). EasyChair, 142--184.
[5]
Diego Manzanas Lopez, Sung Woo Choi, Hoang-Dung Tran, and Taylor T. Johnson. 2023. NNV 2.0: The Neural Network Verification Tool. In 35th International Conference on Computer-Aided Verification (CAV).
[6]
Diego Manzanas Lopez, Sung Woo Choi, Hoang-Dung Tran, and Taylor T. Johnson. 2023. NNV 2.0: The Neural Network Verification Tool, (CodeOcean Capsule). https://doi.org/10.24433/CO.0803700.v1
[7]
Diego Manzanas Lopez, Taylor T. Johnson, Stanley Bak, Hoang-Dung Tran, and Kerianne Hobbs. 2022. Evaluation of Neural Network Verification Methods for Air to Air Collision Avoidance. AIAA Journal of Air Transportation (JAT) (Oct. 2022).
[8]
Diego Manzanas Lopez, Patrick Musau, Nathaniel Hamilton, Hoang-Dung Tran, and Taylor T. Johnson. 2020. Case Study: Safety Verification of an Unmanned Underwater Vehicle. In Workshop on Assured Autonomous Systems (WAAS). IEEE.
[9]
Diego Manzanas Lopez, Patrick Musau, Nathaniel Hamilton, and Taylor Johnson. 2022. Reachability Analysis of a General Class of Neural Ordinary Differential Equation. In Proceedings of the 20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2022), Co-Located with CONCUR, FMICS, and QEST as part of CONFEST 2022. Warsaw, Poland.
[10]
Mark Niklas Müller, Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. 2022. The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results.
[11]
ONNX. [n. d.]. Open Neural Network Exchange (ONNX). https://onnx.ai/
[12]
Hoang-Dung Tran, Feiyang Cei, Diego Manzanas Lopez, Taylor T. Johnson, and Xenofon Koutsoukos. 2019. Safety Verification of Cyber-Physical Systems with Reinforcement Learning Control. In ACM SIGBED International Conference on Embedded Software (EMSOFT'19). ACM.
[13]
Hoang Dung Tran, SungWoo Choi, Tomoya Yamaguchi, Bardh Hoxha, and Danil Prokhorov. 2023. Verification of Recurrent Neural Networks using Star Reachability. In The 26th ACM International Conference on Hybrid Systems: Computation and Control (HSCC).
[14]
Hoang-Dung Tran, Patrick Musau, Diego Manzanas Lopez, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson. 2019. Parallelizable Reachability Analysis Algorithms for Feed-forward Neural Networks. In Proceedings of the 7th International Workshop on Formal Methods in Software Engineering (FormaliSE'19) (Montreal, Quebec, Canada) (FormaliSE '19). IEEE Press, Piscataway, NJ, USA, 31--40.
[15]
Hoang-Dung Tran, Patrick Musau, Diego Manzanas Lopez, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T. Johnson. 2019. Star-Based Reachability Analsysis for Deep Neural Networks. In 23rd International Symposisum on Formal Methods (FM'19). Springer International Publishing.
[16]
Hoang-Dung Tran, Neelanjana Pal, Diego Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T Johnson. 2021. Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter. Formal Aspects of Computing 33, 4 (2021), 519--545.
[17]
Hoang-Dung Tran, Neelanjana Pal, Patrick Musau, Diego Manzanas Lopez, Nathaniel Hamilton, Xiaodong Yang, Stanley Bak, and Taylor T Johnson. 2021. Robustness verification of semantic segmentation neural networks using relaxed reachability. In International Conference on Computer Aided Verification. Springer, 263--286.
[18]
Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T. Johnson. 2020. NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems. In 32nd International Conference on Computer-Aided Verification (CAV).
Index Terms
- Tutorial: Neural Network and Autonomous Cyber-Physical Systems Formal Verification for Trustworthy AI and Safe Autonomy
Index terms have been assigned to the content through auto-classification.
Recommendations
Towards Formal Verification of Neural Networks in Cyber-Physical Systems
NASA Formal MethodsAbstractMachine Learning approaches have been successfully used for the creation of high-performance control components of cyber-physical systems, where the control dynamics result from the combination of many subsystems. However, these approaches may ...
Practical Use of Formal Verification for Safety Critical Cyber-Physical Systems: A Case Study
CPSNA '14: Proceedings of the 2014 IEEE International Conference on Cyber-Physical Systems, Networks, and ApplicationsCyber-Physical Systems (CPS) linking computing to physical systems are often used to monitor and controlsafety-critical processes, i.e. processes that bear the potential to cause significant damage or loss in the case of failures. While safety-critical ...
Cyber/Physical Co-verification for Developing Reliable Cyber-physical Systems
COMPSAC '13: Proceedings of the 2013 IEEE 37th Annual Computer Software and Applications ConferenceCyber-Physical Systems (CPS) tightly integrate cyber and physical components and transcend discrete and continuous domains. It is greatly desired that the physical components being controlled and the software implementation of control algorithms can be ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2023
28 pages
ISBN:9798400702914
DOI:10.1145/3607890
- Chair:
- Xiaobo Sharon Hu,
- Co-chair:
- Alessandro Biondi,
- Program Chair:
- Claire Pagetti
Copyright © 2023 ACM.
Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of the United States government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 19 January 2024
Check for updates
Qualifiers
- Tutorial
Funding Sources
- National Science Foundation
- NSF Nebraska EPSCoR
- DARPA
- Air Force Office of Scientific Research
Conference
Acceptance Rates
Overall Acceptance Rate 60 of 203 submissions, 30%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 75Total Downloads
- Downloads (Last 12 months)75
- Downloads (Last 6 weeks)4
Reflects downloads up to 22 Nov 2024
Other Metrics
Citations
Cited By
View allView Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in