Verification of Unknown Dynamical Systems via Autoencoder Latent Space

Robert Reed; Luca Laurenti; Morteza Lahijanian

cs.LGDec 15, 2025

Verification of Unknown Dynamical Systems via Autoencoder Latent Space

Authors: Robert Reed, Luca Laurenti, Morteza Lahijanian

Organizations: Dept. of Aerospace Engineering University of Colorado Boulder Boulder, Colorado, USA · Delft University of Technology Delft, Netherlands · AI4I, Turin, Italy

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 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.

Figures & tables

Panel of Figure 1 — Figure 1: Results for “ 3D-Nonlinear-to-2D ” and “ 6D-to-2D ” case studies. (a) The 2D latent space of the 3D system with the goal shown outlined in green, the domain outlined in black, and verification results in (b). (c) Verification results for the “ 6D-to-2D ” case study without obstacles, and (d) with an obstacle. (d) Encoded sample trajectories: green satisfy and red violate $\varphi$ in the original space.

Panel of Figure 2 — Figure 2: Results for the “ 26D-to-2D ” case study. (a) The 2D latent space and regions. (b) Verification results with (encoded) sample trajectories from the original space that satisfy $\varphi$ in green and a violating trajectory in red. (c)-(d) Safe and Unsafe trajectories that begin in the same region $q$ from (b) shown in the original space of the system (LiDAR shown every 5 steps).

System	$\mathbf{t_{h_{e}}}$ (s)	$\mathbf{t_{\text{IGP}}}$ (s)	$\mathbf{t_{\text{Abs}}}$ (s)	$\mathbf{\%\textrm{Vol}(Q_{yes})}$
$3D$	$125.75\pm 2.66$	$36.45\pm 3.26$	$495.14\pm 150.09$	$99.999\pm 0.002$
$6D$	$434.34\pm 17.88$	$39.99\pm 5.93$	$1816.88\pm 731.02$	$100\pm 0$
$6D$ Obs	$434.34\pm 17.88$	$39.99\pm 5.93$	$4227.05\pm 4266.38$	$47.29\pm 11.25$
$26D$	$503.00\pm 7.32$	$63.32\pm 2.35$	$6238.99\pm 2137.75$	$48.15\pm 3.55$

Table 1: Timings for the encoder training (

t_{h_{e}}

), Inclusion GP training (

t_{\text{IGP}}

), abstraction generation (

t_{\text{Abs}}

), and the percent volume of space in the latent domain that is in

Q_{yes}

\textrm{Vol}(Q_{yes}

)).

Appendix figures & tables4 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 3: A flowchart of the method used in this paper.

Figure 4: Visualization: mapping regions to the latent space.

Figure 5: Visualization of Inclusion GP predictions. The initial latent variables $z^{*}$ is shown as a black dot (top-right), observed evolutions $z_{i}^{+}$ as red stars (multiple samples of $h_{e}(\mathcal{X}^{\prime}_{z^{*}})$ ), the predicted evolution for 10 $c^{*}$ values of the Inclusion GP with blue rectangles ( $\mu^{(j)}_{D}(z^{*},c^{*})\pm\sigma_{D}^{(j)}(z^{*},c^{*})\sqrt{B^{2}-d^{*}}$ ).

Test	$L_{1}$	$L_{2}$	$L_{3}$	Loss	Latent Domain Size ( $Z\subset$ ranges)
$1$	0	0	1	0.02935	$[0,1600]\times[0,800]$
$1$	0	0	1	0.02367	$[0,1000]\times[0,1400]$
$2$	1	0	1	0.05373	$[2,16]\times[0,27]$
$2$	1	0	1	0.05228	$[2,18]\times[0,27]$
$3$	1	1	1	0.19286	NA
$3$	1	1	1	0.24785	NA

Appendix

Table 2: Ablation study results when training on the 6D dataset with different loss terms weighted at 0. The first 5 columns identify the multiplier applied to

\alpha_{i}

(i.e. 0 means the loss term is ignored). We run two tests for each setup under different seeds.

Formal Verification

Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.

See all 339 papers

Understanding Latent-Dimension Scaling in Dynamical-System Learning through Spectral Reliability
Oct 8, 2026Itsushi Sakata, Yuta Miyauchi, Yoshinobu KawaharaLatent Dynamics Modeling Dynamical Systems
RIKEN Center for Advanced Intelligence Project, Tokyo, Japan. · Graduate School of Information Science and Technology, The University of Osaka, Suita, Osaka, Japan.
Accelerated surrogate dynamics for dynamical, stochastic system evolution
Sep 29, 2026Marco Jochum, Ioannis Kouroudis, Gohar Ali Siddiqui +3Neural Surrogate Modeling Dynamical Systems
Chair of Simulation of Nanosystems for Energy Conversion, Department of Electrical Engineering, TUM School of Computation, Information and Technology, Atomistic Modeling Center (AMC), Munich Data Science Institute (MDSI), Technical University of Munich, Hans-Piloty-Straße 1, 85748 Garching, Germany
Learning Permutation-invariant Macroscopic Dynamics
May 29, 2026Zhichao Han, Mengyi Chen, Qianxiao LiDynamical Systems Latent Dynamics Modeling
Institute for Functional Intelligent Materials, National University of Singapore · Department of Mathematics, National University of Singapore

Oct 8, 2026J/K move · Enter open · S save

Understanding Latent-Dimension Scaling in Dynamical-System Learning through Spectral Reliability

Itsushi Sakata, Yuta Miyauchi, Yoshinobu Kawahara

RIKEN Center for Advanced Intelligence Project, Tokyo, Japan. · Graduate School of Information Science and Technology, The University of Osaka, Suita, Osaka, Japan.

Latent Dynamics Modeling Dynamical Systems Koopman Operator Learning

Open paper AskPDF arXiv

In deep learning, approximation theory motivates increasing representation size. We ask whether this benefit extends to dynamics learning through autoregressive prediction. We analyze the learned time evolution through the eigenstructure of Koopman operators, using relative residuals to detect spurious eigenpairs arising even as one-step error falls. For bounded Koopman operators, we show that minimal residuals over learned dictionary spaces converge pointwise to their full-space counterparts as these spaces approximate the observable space in

L^2

. Our hypothesis is that Koopman spectral reliability helps explain how consistently rollout error decreases with increasing dimension. We compare two models of a shared Koopman autoencoder trained alternately for reconstruction and latent evolution, using latent-prediction loss (one-step prediction errors in latent coordinates) or spectral-residual loss (relative residuals of candidate eigenpairs). Across six chaotic systems, both models reduced median windowed rollout error from smallest to largest dimension. The spectral-residual model achieved lower medians than the latent-prediction model for all systems and dimensions, and its median fell by a larger factor in every system. Its median decreased monotonically with dimension in four systems, against one for latent prediction. Against four baseline families, its mean valid prediction times were nearly always longer. At the largest dimension under two-stage training, we compared eigenvalue positions with each learned dictionary's residual contours. Spectral-residual eigenvalues concentrated in low-residual regions, whereas latent-prediction eigenvalues also appeared in high-residual regions, consistent with the hypothesis.

Abstract

Formal Verification

Explore similar work

Understanding Latent-Dimension Scaling in Dynamical-System Learning through Spectral Reliability

Accelerated surrogate dynamics for dynamical, stochastic system evolution

Learning Permutation-invariant Macroscopic Dynamics