Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles

TL;DR

SEVIN introduces a scalable, explainable verification framework for image-based neural network controllers in autonomous vehicles, using VAEs to reduce complexity and improve safety assurance.

Contribution

The paper presents SEVIN, a novel framework that combines VAEs with formal verification to enable scalable, interpretable safety analysis of high-dimensional image-based controllers.

Findings

Efficient verification of neural controllers with reduced computational cost.

Enhanced interpretability through explainable latent space analysis.

Robustness verification under environmental perturbations.

Abstract

Existing formal verification methods for image-based neural network controllers in autonomous vehicles often struggle with high-dimensional inputs, computational inefficiency, and a lack of explainability. These challenges make it difficult to ensure safety and reliability, as processing high-dimensional image data is computationally intensive and neural networks are typically treated as black boxes. To address these issues, we propose SEVIN (Scalable and Explainable Verification of Image-Based Neural Network Controllers), a framework that leverages a Variational Autoencoders (VAE) to encode high-dimensional images into a lower-dimensional, explainable latent space. By annotating latent variables with corresponding control actions, we generate convex polytopes that serve as structured input spaces for verification, significantly reducing computational complexity and enhancing scalability. Integrating the VAE's decoder with the neural network controller allows for formal and robustness verification using these explainable polytopes. Our approach also incorporates robustness verification under real-world perturbations by augmenting the dataset and retraining the VAE to capture environmental variations. Experimental results demonstrate that SEVIN achieves efficient and scalable verification while providing explainable insights into controller behavior, bridging the gap between formal verification techniques and practical applications in safety-critical systems.