# Verification of Unknown Dynamical Systems via Autoencoder Latent Space

arXiv: https://arxiv.org/abs/2512.13593 · HTML: https://mlsanity.com/paper/2512.13593/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 33 references that are in the map.
- First posted on arXiv 15 Dec 2025.

## Builds on (most cited first, 14 of 14)

- [Learning Latent Dynamics for Planning from Pixels](https://mlsanity.com/paper/1811.04551/) (2018)
- [Deep Kernel Learning](https://mlsanity.com/paper/1511.02222/) (2015)
- [Input Convex Neural Networks](https://mlsanity.com/paper/1609.07152/) (2016)
- [Embed to Control: A Locally Linear Latent Dynamics Model for Control from Raw Images](https://mlsanity.com/paper/1506.07365/) (2015)
- [Generalizing Safety Beyond Collision-Avoidance via Latent-Space Reachability Analysis](https://mlsanity.com/paper/2502.00935/) (2025)
- [A Simple and Efficient Sampling-based Algorithm for General Reachability Analysis](https://mlsanity.com/paper/2112.05745/) (2021)
- [Efficiency through Uncertainty: Scalable Formal Synthesis for Stochastic Hybrid Systems](https://mlsanity.com/paper/1901.01576/) (2019)
- [PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks](https://mlsanity.com/paper/2408.09262/) (2024)
- [Error Bounds For Gaussian Process Regression Under Bounded Support Noise With Applications To Safety Certification](https://mlsanity.com/paper/2408.09033/) (2024)
- [Latent Representations for Control Design with Provable Stability and Safety Guarantees](https://mlsanity.com/paper/2505.23210/) (2025)
- [Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression](https://mlsanity.com/paper/2201.00655/) (2021)
- [Promises of Deep Kernel Learning for Control Synthesis](https://mlsanity.com/paper/2309.06569/) (2023)
- [tt MORALS: Analysis of High-Dimensional Robot Controllers via Topological Tools in a Latent Space](https://mlsanity.com/paper/2310.03246/) (2023)
- [Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates (Extended Version)](https://mlsanity.com/paper/2506.16971/) (2025)

## Built on by (most cited first, 1 of 1)

- [Latent Safety Filters: When a Lossy Encoder Admits a Transferable Certificate](https://mlsanity.com/paper/2610.04297/) (2026)

## Abstract (arXiv)

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.