Scalable Formal Verification via Autoencoder Latent Space Abstraction
This work addresses the problem of scalable formal verification for high-dimensional systems, which is crucial for ensuring safety in complex AI-driven applications, though it builds incrementally on existing learning-based approaches.
The paper tackles the scalability challenge of formal verification for high-dimensional systems by using convex autoencoders and kernel-based dynamics learning in the latent space, guaranteeing correctness and demonstrating significant scalability improvements on systems like a 26D neural network-controlled system.
Finite Abstraction methods provide a powerful formal framework for proving that systems satisfy their specifications. However, these techniques face scalability challenges for high-dimensional systems, as they rely on state-space discretization which grows exponentially with dimension. Learning-based approaches to dimensionality reduction, utilizing neural networks and autoencoders, have shown great potential to alleviate this problem. However, ensuring the correctness of the resulting verification results remains an open question. In this work, we provide a formal approach to reduce the dimensionality of systems via convex autoencoders and learn the dynamics in the latent space through a kernel-based method. We then construct a finite abstraction from the learned model in the latent space and guarantee that the abstraction contains the true behaviors of the original system. We show that the verification results in the latent space can be mapped back to the original system. Finally, we demonstrate the effectiveness of our approach on multiple systems, including a 26D system controlled by a neural network, showing significant scalability improvements without loss of rigor.