Data-driven Verification of Autonomous Systems: Reachability, Entropy, and Contracts

Data-driven Verification of Autonomous Systems: Reachability, Entropy, and Contracts

연구 분야: Artificial Intelligence

학회: HSCC '24: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control

Engineering safe and trustworthy autonomous systems demand formal methodologies that accommodate statistical models and assumptions. In the first part of this talk, I will present safety verification methods that use reachability analysis. This research explores a spectrum of model assumptions and the corresponding guarantees and utilities. The methods combine simulation data with sensitivity analysis. At one end, complete dynamical models offer strong guarantees, but their utility can be limited. Learning sensitivity from data comes with statistical guarantees, and the algorithms are applicable to real-world scenarios, and still confer the benefits of formal reasoning via composition and abstraction. This flexible approach informs our current work on the Verse framework which aims to make code-level analysis for autonomous multi-agent scenarios accessible to undergraduates in engineering design courses. In the second part, I will discuss a safety analysis method for learning-enabled autonomous systems using abstraction and substitutivity. The method derives the conditions when a hypothetical ideal observer can be substituted with a practical observer implemented by a machine learning model. This leads to the notion of a perception contract which approximates the machine learning model, and it can substitute a perfect observer while preserving the safety proof. I will discuss applications of this method in the analysis for vision-based lane keeping and automated landing systems.