Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles
Aditya Parameshwaran, Yue Wang
TL;DR
The paper tackles the scalability and interpretability gap in formal verification of image-based neural network controllers for autonomous vehicles by introducing SEVIN, which maps high-dimensional images to a structured latent space via a Gaussian Mixture-VAE and partitions this space into convex polytopes labeled by control actions. The decoder of the VAE is integrated with the controller to form a combined network $\mathcal{H}(\mathbf{z}) = F(D(\mathbf{z}))$, enabling formal verification over low-dimensional polytopes with symbolic specifications (VNN-LIB) and using tools like $\alpha$-$\beta$-CROWN; the framework also extends to robustness verification through augmented latent spaces learned from perturbed data. Key contributions include a concrete construction of latent-space convex polytopes, a theoretical equivalence between latent-space and input-space verification (Theorem 1), and an end-to-end pipeline that supports both vanilla and robustness verification. Experiments in a driving environment show SEVIN achieving efficient verification (often under 1 second) and providing interpretable insights into controller behavior, with robustness improvements demonstrated via augmented data. Overall, SEVIN advances practical safety guarantees for image-based AV controllers by combining probabilistic latent representations, geometric input-space partitioning, and symbolic specifications to bridge formal methods and real-world applications.
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.