Latent Representations for Control Design with Provable Stability and Safety Guarantees

TL;DR

This work develops a formal framework for using low-dimensional latent representations to design verifiable controllers with stability and safety guarantees for high-dimensional dynamical systems. By defining dynamic conjugacy measures between latent and original models, it enables transfer of Lyapunov and barrier guarantees from latent space back to the true system, while accounting for reconstruction errors. The approach yields concrete loss functions for latent dynamics learning and a systematic method to certify regions of attraction and safe sets in the original state space. The authors validate the theory on cartpole stabilization and two-vehicle collision avoidance, showing practical stability and forward invariance under quantifiable conjugacy bounds with forward completeness guarantees. The work advances the reliability of learning-based control in safety-critical settings by linking latent theory to rigorous guarantees on real systems.

Abstract

We initiate a formal study on the use of low-dimensional latent representations of dynamical systems for verifiable control synthesis. Our main goal is to enable the application of verification techniques -- such as Lyapunov or barrier functions -- that might otherwise be computationally prohibitive when applied directly to the full state representation. Towards this goal, we first provide dynamics-aware approximate conjugacy conditions which formalize the notion of reconstruction error necessary for systems analysis. We then utilize our conjugacy conditions to transfer the stability and invariance guarantees of a latent certificate function (e.g., a Lyapunov or barrier function) for a latent space controller back to the original system. Importantly, our analysis contains several important implications for learning latent spaces and dynamics, by highlighting the necessary geometric properties which need to be preserved by the latent space, in addition to providing concrete loss functions for dynamics reconstruction that are directly related to control design. We conclude by demonstrating the applicability of our theory to two case studies: (1) stabilization of a cartpole system, and (2) collision avoidance for a two vehicle system.

Figures (3)

• Figure 1: Left (Stability): A Lyapunov function $V$ in latent space $\mathbb{R}^{n_z}$ guarantees: (1) stability of the origin, and (2) forward invariance of sub-level sets of $V$ (shown in yellow). The Lyapunov function $V$ induces in the original space $\mathbb{R}^{n_x}$: (1) forward invariant sets (shown in yellow), and (2) an attractive set $\mathcal{V}_{L\gamma/\rho}$ that contains the origin (shown in blue). Right (Safety): The set $\mathcal{S}_x$ denotes a safe set in the original space $\mathbb{R}^{n_x}$ that induces a safe set $\mathcal{S}_z$ in the latent space $\mathbb{R}^{n_z}$ (shown in red); we have that $E^{-1}(\mathcal{S}_z)\subseteq \mathcal{S}_x$. A barrier function $h$ in latent space guarantees forward invariance of a set $\mathcal{C}_z^\gamma \subset \mathcal{S}_z$ (shown in yellow). The set $\mathcal{C}_z^\gamma$ induces a forward invariant and safe set $\mathcal{C}_x^\gamma$ in the original space, i.e., $\mathcal{C}_x^\gamma\subseteq \mathcal{S}_x$.
• Figure 2: Top left: Sub-level sets of $\overline{V}=V\circ E$ for the $(0,0,\theta, \dot{\theta})$-slice of the cartpole state space under LQR controller. Over-approximation of the attractive set, $\overline{V}(x)\leq L\gamma/(1-\rho)$, is compared to directly-computed bound on attractive set, $\max_{x\in \mathcal{D}_x}|R(x)|/(1-\rho)$. For $(1-\rho)=0.15$, bounding $|R(x)|$ with $L\gamma$ yields a reasonable over-approximation. Note the zero set $E^{-1}(0)$ in red; the system can move in this direction while keeping $\overline{V}$ constant. Top right: Same as top-left, but for $(x,0,\theta,0)$-slice. Included system trajectories demonstrate convergent behavior: these trajectories converge to the origin even once entering the zero set $E^{-1}(0)$. Bottom left: Trajectories $x_t$ projected into latent space, and level sets of $V$. Bottom right: System trajectories converge to the zero-level set of $\overline{V}=V\circ E$; dashed line corresponds to directly-computed bound on the minimal attractive level set, dotted line corresponds to over-approximation $L\gamma/(1-\rho)$.
• Figure 3: Numerical simulation of 2-car avoidance system. Trajectories and plots are color-coded to reflect time. Top: Latent space trajectory. The gray circle corresponds to $\{z\mid\phi_{\beta'}(z)<0\}$ and the cyan circle corresponds to $\mathcal{S}_z^c$. Middle: State space trajectory resulting from applying the latent-CBF filtered control to the 6D dynamics. Bottom: Control signal over time.

Theorems & Definitions (30)

• Definition 1: Conjugate Dynamics Error -- Continuous Time
• Definition 2: Conjugate Dynamics Error -- Discrete Time
• Definition 3: Continuous Time Lyapunov Function
• Lemma 1: Lyapunov Condition (Continuous Time)
• proof
• Remark 1: Significance of $\mathcal{D}_x$
• Theorem 1: Stability Guarantee (Continuous Time)
• proof
• Remark 2: Forward Completeness
• Remark 3: Relation to Almost Lyapunov Functions