PaperlayerView exact revision on arXiv

Source-linked AI summary

Learning neural controllers for nonlinear systems from data

Zhongjie Hu, Zhi-Wei Liu, Chen Wang

arXiv:2608.29303v1eess.SY

TL;DR

The paper asks how to design provably stable neural controllers for unknown nonlinear systems despite finite data, input limits, and identification perturbations. It identifies dynamics from offline data, jointly synthesizes neural control and Lyapunov functions, and combines hard saturation with SMT and local analysis. The reported examples obtain formal asymptotic-stability certificates, including under data perturbations.

  • Problem

    Designing neural controllers for unknown nonlinear systems requires stability guarantees despite finite data, continuous-domain requirements, and nonconvex neural stability conditions.

  • Method

    An indirect data-driven framework identifies dynamics from offline data, jointly synthesizes neural controllers and Lyapunov functions, enforces inputs by hard saturation, and certifies stability with SMT plus local analysis.

  • Results

    The numerical evaluations formally certify asymptotic stability over the full normalized domain, including under identification-data perturbations.

  • Takeaways & Limitations

    The framework provides a data-driven route to neural feedback control with provable stability, actuator-limit enforcement, and robustness to data-consistent model uncertainty.

  • Takeaways & Limitations

    Formal certification requires restricting verification to a bounded domain because global verification with transcendental dynamics and activations is undecidable.

Abstract

from arXiv · show

This article addresses the problem of designing neural feedback controllers for unknown nonlinear systems. We propose an indirect data-driven framework that uses offline data to identify the system dynamics, upon which a neural feedback controller and a neural Lyapunov function are jointly synthesized. Input constraints are enforced by integrating a hard-saturation structure into the controller architecture. Robust synthesis conditions are derived to account for data perturbations during identification. Formal stability is certified by combining SMT verification with local Lyapunov analysis near the equilibrium. Numerical examples validate the effectiveness of the proposed framework.

I. INTRODUCTION

The paper targets neural control of unknown nonlinear systems while addressing limited controller expressivity, continuous stability certification, and nonconvex neural stability conditions. It proposes an indirect data-driven framework that identifies dynamics from offline data, then jointly synthesizes and formally verifies neural controllers and Lyapunov functions.

  • Fixed-structure controllers and Lyapunov functions can limit expressivity and create a bottleneck for closed-loop performance.
  • Neural networks enlarge the controller and Lyapunov-function search spaces through their ability to approximate continuous functions.
  • Finite training data, continuous-domain stability requirements, and nonconvex neural stability conditions make rigorous guarantees difficult.
  • The framework identifies unknown dynamics from offline data before jointly synthesizing and formally verifying neural feedback controllers and neural Lyapunov functions.It assumes the vector field can be represented as a matrix multiplying known basis functions and requires data richness through a full-row-rank data matrix.
  • State normalization, bias elimination, pre-training, counterexample search, local Lyapunov analysis, hard saturation, and robust synthesis address numerical, verification, input, and data-perturbation concerns.The verification domain is split between an outer SMT-certified region and an inner region handled analytically near equilibrium.

B. Neural controller design

The paper jointly designs neural feedback controllers and neural Lyapunov functions for data-driven stabilization of unknown nonlinear systems. Formal guarantees are obtained through Lyapunov conditions, while the approach avoids structural limitations of several existing methods.

  • Neural controller and Lyapunov design: Neural networks parameterize both the feedback controller and Lyapunov function, enabling joint synthesis for asymptotic stabilization.The controller and Lyapunov function are required to vanish at the origin.
  • Neural controller and Lyapunov design: Theorem 1 certifies asymptotic stability when the neural controller and Lyapunov function satisfy the stated conditions over a set containing the origin.Any contained sublevel set of the Lyapunov function provides an estimate of the region of attraction.
  • Comparison with existing methods: The proposed neural controller directly accounts for the full nonlinear dynamics and therefore bypasses the linear stabilizability requirements shared by two comparison methods.Those methods use augmented formulations whose feasibility can be difficult because of structural zero blocks.
  • Comparison with existing methods: Formal verification with transcendental dynamics requires interval-based SMT solvers on a bounded domain, because global verification is mathematically undecidable for the included nonlinearities.Compact-domain restriction is essential for obtaining formal stability certificates.
  • Comparison with existing methods: The Taylor-expansion comparison avoids requiring a prior function library but restricts controllers and Lyapunov functions to linear or fixed-degree polynomial templates.Its truncated remainder grows unbounded with state norm, confining theoretical guarantees to a local region.

IV. NEURAL CONTROLLER SYNTHESIS AND SMT-BASED LYAPUNOV VERIFICATION

The synthesis pipeline identifies and normalizes the system representation, trains neural controller and Lyapunov networks, and formally verifies stability over the domain. State normalization preserves stability equivalence while improving numerical conditioning, and hard architectural constraints enforce equilibrium properties exactly.

  • Synthesis and verification pipeline: The framework minimizes a sample-based stability loss while combining SMT solvers with local stability analysis for formal certification.Training uses dynamic counterexample-guided data augmentation rather than only a static offline dataset.
  • Dynamic data generation and state normalization: State normalization is presented as necessary for effective training because disparate physical scales can cause ill-conditioning and vanishing gradients outside the tanh activation range.The paper therefore treats normalization as more than empirical preprocessing.
  • Dynamic data generation and state normalization: State normalization maps the bounded physical domain onto the unit hypercube [−1, 1]^n for neural-network training.The transformation scales each state coordinate by its corresponding bound.
  • Dynamic data generation and state normalization: The normalized model is identified from data matrices satisfying Z1 = MΦ0, with M recovered using the right inverse of Φ0.The normalized function library is constructed through a nonsingular diagonal transformation.
  • Dynamic data generation and state normalization: Stability of the normalized system is equivalent to stability of the original physical dynamics under the nonsingular coordinate transformation z = Sx.The transformation bijectively maps the original domain to the normalized domain and preserves the equilibrium.
  • Synthesis and verification pipeline: The synthesis objective designs normalized networks and recovers the physical controller and Lyapunov function through ϕ(x) = ψ(Sx) and V(x) = Vz(Sx).This transfers stability conditions established on the normalized domain back to the original domain.
  • Network architecture and pre-training: Hard bias elimination guarantees ψ(0) = 0 and Vz(0) = 0 by construction, independently of network weights and biases.Lyapunov pre-training toward a canonical quadratic function provides a well-conditioned initialization for joint optimization.

Loss Function Design and Optimization:

The framework jointly synthesizes a neural controller and Lyapunov function by penalizing violations of positive- and negative-definiteness conditions. Margin and penalty-weight choices balance convergence, optimization, and numerical tractability.

  • Loss Function Design and Optimization:: The metric Ω(z) := z⊤z converts Lyapunov stability conditions into explicit penalty terms in the loss architecture.
  • Loss Function Design and Optimization:: Positive-definiteness of Vz(z) and negative-definiteness of its time derivative are enforced through separate penalty terms.The penalties are evaluated over the normalized domain excluding the origin.
  • Loss Function Design and Optimization:: The loss function jointly synthesizes the neural controller ψ(z) and neural Lyapunov function Vz(z).The overall objective combines penalties for Lyapunov-condition violations.
  • Loss Function Design and Optimization:: The margin ε trades off closed-loop decay rate, transient performance, optimization tractability, and SMT numerical robustness.Large ε can induce high-gain actions, gradient explosion, and divergence; small ε can slow convergence and strain solver precision.
  • Loss Function Design and Optimization:: The penalty-weight ratio γ1/γ2 must account for normalization-induced gradient scaling so neither loss component dominates optimization.Small state-scaling bounds can amplify the derivative penalty and require a higher γ1/γ2 ratio.

B. Counterexample Generation

Counterexample generation replaces average-sample training with targeted searches for states violating Lyapunov conditions. PGD, GAN, and PSO generate such states, which are added to the training set while controller and Lyapunov parameters remain fixed during search.

  • B. Counterexample Generation: Counterexamples are states in Xz \ {0} that violate at least one Lyapunov stability condition.The violation set is defined as the union of the regions where the conditions fail.
  • B. Counterexample Generation: The framework targets worst-case violations instead of relying only on empirical risk minimization over randomly drawn samples.This aligns training with the deterministic, domain-wide stability guarantee sought by verification.
  • B. Counterexample Generation: PGD recursively follows violation-loss gradients and projects candidate states back onto Xz at each step.The search uses a step size κ over a horizon of p steps.
  • B. Counterexample Generation: GAN maps Gaussian inputs directly to candidate counterexamples and maximizes the deterministic loss Ltotal instead of using an empirical discriminator.
  • B. Counterexample Generation: PSO searches for worst-case states without derivatives, avoiding gradient vanishing or explosion from saturating activations and non-smooth penalties.
  • B. Counterexample Generation: Generated counterexamples from PGD, GAN, or PSO are appended to D for subsequent training of Vz and ψ.The search phase keeps both network parameter sets fixed while uncovering counterexamples.

C. Stability Formal Verification

Formal certification combines counterexample-guided training and interval-based SMT verification outside a small neighborhood of the equilibrium with local Lyapunov analysis inside it. In the Lorenz example, the procedure verifies the domain-wide stability conditions and shows convergence of tested closed-loop trajectories to the origin.

  • C. Stability Formal Verification: SMT verification addresses the gap between finite-sample neural training and continuous Lyapunov guarantees over the domain.Successful verification certifies the Lyapunov conditions across XSMT.
  • C. Stability Formal Verification: The origin is excluded from SMT verification because conservative interval enclosures become computationally bottlenecked near the equilibrium.The verified region is changed to XSMT := Xz \ Bσ(0), with the remaining neighborhood handled locally.
  • C. Stability Formal Verification: Local certification uses a quadratic Lyapunov function Vloc(z) := z⊤Pz and checks negativity of its derivative near the origin.The matrix P is obtained through an SDP after the closed-loop Jacobian is verified to be Hurwitz.
  • C. Stability Formal Verification: The synthesis loop alternates targeted sampling, counterexample augmentation, neural optimization, SMT verification, and local stability checks until acceptance conditions are met.Failed SMT checks return falsifying intervals for further training, while accepted candidates proceed to Jacobian and threshold tests.
  • C. Stability Formal Verification: The dynamically expanded dataset combines initial samples, heuristic counterexamples, and formal SMT counterexamples.Hybrid sampling also concentrates points near the boundary of the excluded local ball.
  • C. Stability Formal Verification: In the Lorenz example, dReal formally verifies the Lyapunov conditions over XSMT, while the local Jacobian has maximum eigenvalue real part −2.6667 and σthreshold = 2.2526.The reported threshold satisfies σ < σthreshold, completing the stability argument over the full domain.
  • C. Stability Formal Verification: Closed-loop trajectories from four tested initial states converge to the origin, unlike the open-loop trajectories that remain chaotic.

V. INPUT CONSTRAINTS

The framework enforces admissible inputs through hard saturation and normalization, then synthesizes controllers and Lyapunov functions in transformed coordinates. Numerical examples certify stability and show convergence while respecting input bounds.

  • Input constraint formulation: Input admissibility is defined by lower and upper bounds on each control component.The admissible set is U := {u ∈ R^m | −u_i,min ≤ u_i ≤ u_i,max}.
  • Numerical validation: For the Lorenz example, closed-loop trajectories from four initial states converge to the origin, unlike the persistently chaotic open-loop trajectories.The comparison is shown using 3D phase portraits.
  • Hard saturation and normalization: The hard-saturation architecture avoids adding input constraints to SMT verification or diverting optimization toward penalty terms.The paper identifies both alternatives as computationally burdensome or distracting to Lyapunov-condition optimization.
  • Hard saturation and normalization: A tanh layer confines normalized controls to [−1,1]^m, while linear scaling guarantees recovery of physical inputs in U.The scaling matrix uses b_u,i := min(u_i,min, u_i,max).
  • Normalized synthesis: Input normalization preserves stability equivalence between transformed and physical systems, enabling synthesis in normalized coordinates.The physical controller and Lyapunov function are recovered as ϕ(x) = S_u ψ̄(Sx) and V(x) = V_z(Sx).
  • Numerical validation: For magnetic levitation, the synthesized controller formally certifies stability and drives the iron ball toward its desired height while keeping control input within U.The example uses normalized shifted coordinates and a bounded control architecture.
  • Numerical validation: The estimated region of attraction is obtained from sublevel sets of V_z contained in the set where its derivative is negative.The reported projection compares H, a Lyapunov sublevel set with c = 2.3660, and the target domain.

VI. ROBUSTNESS TO DISTURBANCES

The disturbance-robustness extension treats offline identification as the only stage directly exposed to physical measurement disturbances. Subsequent synthesis and verification operate numerically and deterministically.

  • Scope of disturbances: Offline data acquisition is the sole stage interfacing with the physical plant, so identification data may be affected by environmental disturbances.Controller synthesis and verification occur afterward within a deterministic numerical framework.

A. Robust Stability Conditions under Data Perturbations

The paper models corrupted derivative measurements as bounded additive uncertainty and requires Lyapunov conditions to hold for every system matrix consistent with the data. Under these conditions, asymptotic stability is guaranteed.

  • Perturbation model: State-derivative measurements are modeled with additive perturbations d(t_i), inducing an unknown perturbation matrix D_0 in the data relation.The perturbations enter the sampled dynamics at each acquisition time.
  • Perturbation model: The uncertainty set D_0D_0^⊤ ⪯ ΔΔ^⊤ accommodates pointwise norm bounds, energy constraints, and stochastic disturbances.The bound formalizes prior knowledge about data perturbations.
  • Robust guarantee: Robust synthesis requires the Lyapunov stability conditions to hold across the entire set of system matrices compatible with corrupted data.The true system matrix is represented using the unknown perturbation matrix.
  • Robust guarantee: Under the stated assumptions, existence of neural controller and Lyapunov networks satisfying the robust conditions makes the origin asymptotically stable.The guarantee applies on a set X containing the origin.
  • Feasibility condition: Feasibility depends on making the nominal closed-loop Lyapunov decrease dominate the perturbation and regressor-dependent terms.The paper notes that controllability of the nominal system is fundamental to achieving this balance.

B. Robust Loss Design and Joint Synthesis

The robust loss explicitly encodes perturbation-aware stability conditions and jointly optimizes controller, Lyapunov, and positivity parameters. Exponential reparameterization enforces positivity during training.

  • Robust loss: The nominal loss term is modified into a robust penalty that explicitly enforces the perturbation-aware stability condition.The normalized perturbation is scaled as D_z,0 = S D_0 with bound Δ_z = SΔ.
  • Joint synthesis: The parameter α is optimized jointly with the controller and Lyapunov networks rather than selected offline.This makes α part of the synthesis decision variables.
  • Joint synthesis: The reparameterization α = e^θ_α guarantees α > 0 while allowing unconstrained gradient-based optimization.The learned value becomes a deterministic constant after convergence.
  • Joint synthesis: The convergence margin ε can also be trained jointly, but regularization is required to prevent the trivial solution ε → 0^+.The regularizer maximizes ε while maintaining the Lyapunov inequalities.

C. Robust Local Stability Certification

The framework certifies robust local asymptotic stability by combining an SDP-based local Lyapunov analysis with SMT verification over the remaining domain. In the inverted-pendulum example, this procedure certifies stability despite identification-data perturbations and estimates a region of attraction.

  • Robust local certification: The local analysis searches for P ≻ 0 and positive scalars through an SDP to establish Lyapunov decrease robustly across perturbation matrices.If the SDP is infeasible, the candidate controller is rejected and the networks are re-synthesized.
  • Robust local certification: The local Lyapunov derivative is guaranteed negative throughout Bσ(0)\{0} for every data-consistent dynamics model.This local guarantee is combined with SMT verification over XSMT to cover the full normalized domain Xz.
  • Inverted-pendulum evaluation: The identified-data setting uses 50 uniformly sampled state-control pairs, perturbed measurements, and neural controller and Lyapunov networks with one 50-neuron tanh hidden layer.The experiment targets the domain defined by b1 = 3.14 and b2 = 2.0 and uses σ = 0.05 for the SMT exclusion ball.
  • Inverted-pendulum evaluation: In the inverted-pendulum example, dReal certifies the robust Lyapunov conditions universally over XSMT, while α* = 0.0152 and σthreshold = 2.5523 satisfy the local stability condition.Because σ < σthreshold, the synthesized controller is formally guaranteed to stabilize the upright equilibrium under data perturbations.
  • Inverted-pendulum evaluation: The verified decrease region contains sub-level sets of the learned Lyapunov function that provide region-of-attraction estimates, with the displayed green set larger than any such sub-level set inside X.Figure 4 specifies the displayed sub-level set using c = 3.4224.
  • Robustness with data size: Robust certification remains possible up to T = 1000 samples, although increasing T raises uncertainty-bound conservatism and decreases σthreshold.The observed trend is attributed to the increase of Kg,D with T.

VII. CONCLUSION

The paper presents a data-driven framework that identifies unknown nonlinear dynamics from offline data, then jointly synthesizes and formally verifies neural controllers and neural Lyapunov functions. It enforces actuator limits by construction and extends the synthesis to stability guarantees across data-consistent models under identification perturbations.

  • The framework jointly synthesizes and formally verifies neural feedback controllers and neural Lyapunov functions for unknown nonlinear systems.
  • It follows an indirect control paradigm in which offline data first identify the system model before controller and Lyapunov-function synthesis.
  • A hard-saturation architecture enforces physical actuator limits by construction.
  • The robust extension ensures stability across all models consistent with identification data perturbations.
  • The authors identify computational complexity in high-dimensional systems and output-feedback control as directions for future research.
Loading 2608.29303v1…