Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles
This addresses safety and reliability issues in autonomous vehicles by improving verification methods, though it is incremental as it builds on existing formal verification techniques.
The paper tackles the problem of verifying image-based neural network controllers for autonomous vehicles, which face challenges with high-dimensional inputs and lack of explainability, by proposing SEVIN, a framework that uses Variational Autoencoders to encode images into a lower-dimensional latent space for efficient and scalable verification while providing explainable insights.
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.