Scenario-based Compositional Verification of Autonomous Systems with Neural Perception
This work addresses the verification problem for autonomous systems with deep neural network perception, which is critical for safety-critical applications like autonomous vehicles, though it appears incremental as it builds on existing verification methods with scenario-based modeling.
The authors tackled the challenge of formally verifying autonomous systems with neural perception by proposing a probabilistic verification framework that decomposes tasks into scenarios and builds compact abstractions for each, enabling efficient compositional verification. They demonstrated the approach on case studies involving airplane taxiway guidance and an F1Tenth autonomous car, achieving verification with bounded error probabilities.
Recent advances in deep learning have enabled the development of autonomous systems that use deep neural networks for perception. Formal verification of these systems is challenging due to the size and complexity of the perception DNNs as well as hard-to-quantify, changing environment conditions. To address these challenges, we propose a probabilistic verification framework for autonomous systems based on the following key concepts: (1) Scenario-based Modeling: We decompose the task (e.g., car navigation) into a composition of scenarios, each representing a different environment condition. (2) Probabilistic Abstractions: For each scenario, we build a compact abstraction of perception based on the DNN's performance on an offline dataset that represents the scenario's environment condition. (3) Symbolic Reasoning and Acceleration: The abstractions enable efficient compositional verification of the autonomous system via symbolic reasoning and a novel acceleration proof rule that bounds the error probability of the system under arbitrary variations of environment conditions. We illustrate our approach on two case studies: an experimental autonomous system that guides airplanes on taxiways using high-dimensional perception DNNs and a simulation model of an F1Tenth autonomous car using LiDAR observations.