Formal Verification of Neural ODE for Safety Evaluation in Autonomous Vehicles

Abstract

Higher autonomy is an increasingly common goal in the design of transportation systems for the cities of the future. Recently, part of this autonomy in both rail and maritime transport has come from the field of artificial intelligence and machine learning, particularly for perception tasks (detection and recognition of rail signals, other vessels, or other elements in the vehicle environment) using neural networks. Although AI-based approaches have gained significant popularity in many application fields due to their good performance, their unpredictability and lack of formal guarantees regarding their desired behavior present a major issue for the deployment of such safety-critical systems in urban areas. The goal of my PhD thesis is to design new formal methods to analyze and ensure the safety of such AI-based perception modules in autonomous vehicles. More specifically, my PhD topic aims to formally evaluate the safety of a recently introduced class of continuous AI models which are neural ODE. Neural ODE have already been used successfully for image recognition tasks, showing higher performance compared to classical neural networks, but current work in the literature primarily focuses on their training performance, while they have been barely studied in terms of safety and formal guarantees. The main research directions that will be investigated during my PhD include: • R.D 1: Establishing formal relations between discrete and continuous neural models, and using them to deduce the safety of one model based on the safety verification of the other. • R.D 2: Analysis of the mathematical properties satisfied by the new continuous models (continuity, monotonicity, contraction, stability, etc.). • R.D 3: Exploiting these mathematical properties to study and/or enforce the overall behavior of the neural ODE with respect to various features: stability, stabilization, reachability analysis, safety, formal verification. • Verification and testing of theoretical findings on autonomous underwater vehicles (AUVs) during a 6 month mobility at the Department of Marine Technology, NTNU.