Verification of Unknown Dynamical Systems via Autoencoder Latent Space

TL;DR

This paper introduces a formal verification method for high-dimensional dynamical systems using convex autoencoders and kernel-based learning to reduce dimensionality and ensure accurate behavior abstraction.

Contribution

It presents a novel approach combining convex autoencoders and kernel methods to verify high-dimensional systems in a reduced latent space with guarantees.

Findings

Successfully verified a 26D neural network controlled system

Achieved significant scalability improvements over traditional methods

Constructed finite abstractions containing true system behaviors

Abstract

Formal verification provides a powerful framework for proving that dynamical systems satisfy their specifications. However, these techniques face scalability challenges in high-dimensional settings, as they often 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 correctness of latent space 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 approach on multiple systems, including a 26D system controlled by a neural network, showing significant scalability improvements.