Safety-critical autonomous systems must satisfy hard state constraints under tight computational and sensing budgets, yet learning-based controllers are often far more complex than safe operation requires. To formalize this gap, we study how many distinct control signals are needed to render a compact set forward invariant under sampled-data control, connecting the question to the information-theoretic notion of invariance entropy. We propose a vector-quantized autoencoder that jointly learns a state-space partition and a finite control codebook, and develop an iterative forward certification algorithm that uses Lipschitz-based reachable-set enclosures and sum-of-squares programming. On a 12-dimensional nonlinear quadrotor model, the learned controller achieves a 157× reduction in codebook size over a uniform grid baseline while preserving invariance, and we empirically characterize the minimum sensing resolution compatible with safe operation.
Figures & tables
Fig. 1: VQ-AE controller architecture. The quadrotor estimates its state x^(t)∈R12 from images of an ArUco marker. The encoder Eθ maps x^(t) to a latent vector z , quantized to the nearest codebook entry i=argmink∥z−ek∥22 , inducing a partition {Ai}i=1M of Q . A 2D projection of the partition is shown; the full 12-dimensional partition contains additional regions. Arrows display the controlled vector field within each region, directing trajectories inward to maintain invariance of Q . The decoder Dϕ maps index i to an open-loop control applied over [tk,tk+Ts) .
Fig. 2: Codebook size ∣VTs∣ and closed-loop invariance vs. codebook pressure λpr . Invariance holds at 100% down to ∣VTs∣=14 codes, then collapses. Green checkmarks indicate IFC certification success; all controllers at or beyond the collapse point are unverified.
Method
∣VTs∣
CL Inv. (%)
VQ-AE (ours, pruned)
26
99.979
VQ-AE (ours, unpruned)
171
99.989
VQ-AE partition + OL LQR
171
0.000
Uniform grid + NN
4096
99.975
Uniform grid + CL LQR
2.2M
76.870
TABLE I: Comparison of codebook size and closed-loop invariance rate across baselines, evaluated over 105 trials for 10 s.
Fig. 3: Outputs at different resolutions (indicated above). Closed-loop invariance and terminal safety over 10 s versus image resolution. Invariance remains above 99% down to ∼65 px, then degrades with lower resolution.
Safety-critical control of autonomous systems requires formal safety certificates, such as controlled invariant sets, that must be computed online as conditions change. Although standard synthesis algorithms scale poorly with state dimension, monotone dynamical systems with lower-closed safety specifications allow for accelerated computation of controlled invariant sets. In particular, lazy fixed-point algorithms exploit monotonicity and track only the antichain basis of the set. However, membership tests and redundancy checks against an evolving basis remain major bottlenecks. We introduce a threshold-function reformulation in which a lower-closed set on a d-dimensional grid is represented by its column heights along a designated axis. This reformulates the greatest-fixed-point iteration as independent one-dimensional binary searches, one per grid column, yielding an embarrassingly parallel iteration with asymptotically lower computational complexity than the lazy fixed-point algorithm. Experiments synthesize invariant sets on 3D grids with 10^9 cells in under 50 ms and 10^14 cells in under two minutes. We further demonstrate online re-synthesis in a safety-informed model predictive controller example.
Yasin Sonmez, Mahmoud Khaled, Majid Zamani +1
University of California, Berkeley, USA · Ludwig-Maximilian University, Germany · University of Colorado Boulder, USA
We establish sufficient conditions for robust positive invariance under state- and input-dependent disturbances with anisotropic covariance structure. The proposed ansatz maps a fixed ellipsoidal template through a GP-derived positive-definite matrix field, subsuming scalar homothetic scaling while retaining finite graph-based verification. The resulting LMI conditions couple the learned field to Schur-stable dynamics; an isotropic fallback with inflation factor r=1/(1−γcl) proves admissibility. During each learning epoch the field is frozen, so online tube evaluation is one GP covariance query and a small matrix square root, with no online set iteration or LMI solve. Quadrotor simulations show a 195× reduction in 3D velocity-tube volume and a 2.1×105 reduction in the joint 7D velocity-control subspace relative to a non-adaptive homothetic baseline. This extended version adds full proofs, a separated offline/online complexity analysis, and controller-sweep, contraction, and projection-area studies.
We propose a framework for training neural network controllers with certified robust forward invariant polytopes. First, we parameterize a family of lifted control systems in a higher dimensional space, where the original neural controlled system evolves on an invariant subspace of each lifted system. We use interval analysis and neural network verifiers to further construct a family of lifted embedding systems, carefully capturing the knowledge of this invariant subspace. If the vector field of any lifted embedding system satisfies a sign constraint at a single point, then a certain convex polytope of the original system is robustly forward invariant. Treating the neural network controller and the lifted system parameters as variables, we propose an algorithm to train controllers with certified forward invariant polytopes in the closed-loop control system. Through two examples, we demonstrate how the simplicity of the sign constraint allows our approach to scale with system dimension to over 50 states, and outperform state-of-the-art Lyapunov-based sampling approaches in runtime.
Akash Harapanahalli, Samuel Coogan
School of Electrical and Computer Engineering, Georgia Institute of Technology