PaperlayerView exact revision on arXiv

Source-linked AI summary

Lyapunov-stable neural-network control

Hongkai Dai, Benoit Landry, Lujie Yang, Marco Pavone, Russ Tedrake

arXiv:2109.14152v1cs.ROeess.SY

TL;DR

Neural-network controllers often lack theoretical stability guarantees despite their success in robotics. The paper synthesizes a neural-network controller with a neural-network Lyapunov function, verifies stability using MIPs, and demonstrates the approach on pendulums and quadrotors, where it can outperform a baseline LQR controller.

  • Problem

    Neural-network controllers generally lack theoretical guarantees such as Lyapunov stability, limiting their support for safety-critical robotics applications.

  • Method

    The method jointly synthesizes a neural-network controller and Lyapunov function, using MIP verification to certify conditions or generate counterexamples for improvement.

  • Results

    The approach successfully synthesizes Lyapunov-stable controllers for inverted pendulums and 2D and 3D quadrotors, outperforming a baseline LQR controller in the reported demonstrations.

  • Takeaways & Limitations

    The framework combines neural-network control with formal Lyapunov certification and computes an inner approximation of the closed-loop region of attraction.

Abstract

from arXiv · show

Deep learning has had a far reaching impact in robotics. Specifically, deep reinforcement learning algorithms have been highly effective in synthesizing neural-network controllers for a wide range of tasks. However, despite this empirical success, these controllers still lack theoretical guarantees on their performance, such as Lyapunov stability (i.e., all trajectories of the closed-loop system are guaranteed to converge to a goal state under the control policy). This is in stark contrast to traditional model-based controller design, where principled approaches (like LQR) can synthesize stable controllers with provable guarantees. To address this gap, we propose a generic method to synthesize a Lyapunov-stable neural-network controller, together with a neural-network Lyapunov function to simultaneously certify its stability. Our approach formulates the Lyapunov condition verification as a mixed-integer linear program (MIP). Our MIP verifier either certifies the Lyapunov condition, or generates counter examples that can help improve the candidate controller and the Lyapunov function. We also present an optimization program to compute an inner approximation of the region of attraction for the closed-loop system. We apply our approach to robots including an inverted pendulum, a 2D and a 3D quadrotor, and showcase that our neural-network controller outperforms a baseline LQR controller. The code is open sourced at \url{https://github.com/StanfordASL/neural-network-lyapunov}.

I. INTRODUCTION

Neural-network controllers have strong empirical success in robotics but generally lack theoretical stability guarantees. The paper addresses this gap by synthesizing neural-network controllers and Lyapunov functions, verifying their conditions with MIPs, and evaluating them on robotic systems.

  • Neural-network control policies trained with reinforcement learning generally lack theoretical performance guarantees needed for many safety-critical applications.
  • Lyapunov stability guarantees convergence to an equilibrium for every initial state within a region of attraction.
  • Unlike linear or polynomial approaches, the paper synthesizes both a stable neural-network controller and a neural-network Lyapunov function for systems with neural-network dynamics.
  • The approach verifies Lyapunov conditions with mixed-integer programs that can certify them or produce maximally violating counterexamples.
  • Counterexamples are used either to expand the training set with violation losses or to optimize the maximal violation directly through a min-max procedure.
  • The paper models discrete-time neural-network dynamics around an equilibrium and imposes a decreasing Lyapunov condition on a compact sub-level set to establish exponential convergence.

III. BACKGROUND ON RELU AND MIP

The paper uses mixed-integer linear constraints to represent leaky-ReLU networks because their piecewise-affine structure can be encoded exactly. This enables global MIP verification of neural-network properties over bounded inputs.

  • Leaky-ReLU networks are piecewise-affine, so their input-output relationships can be encoded with linear constraints and binary variables for activation regions.
  • A fully connected network applies affine transformations followed by leaky-ReLU activations across its layers.
  • Replacing each leaky-ReLU unit with big-M constraints fully captures the network's input-output relationship as mixed-integer linear constraints.
  • The verification procedure assumes bounded neural-network inputs because the analysis concerns states near equilibrium and bounded system inputs.
  • Neuron bounds can be computed using interval arithmetic, linear programming, or mixed-integer linear programming.
  • Off-the-shelf solvers can solve the resulting mixed-integer programs to global optimality using branch-and-cut.

IV. APPROACH

The approach jointly parameterizes a neural-network controller and Lyapunov function, then verifies their conditions over a bounded region using mixed-integer programs. It uses a full-rank 1-norm term to promote local positivity and extracts counterexamples when verification fails.

  • Lyapunov function construction: The method searches for a neural-network Lyapunov function φV and a full column-rank matrix R, adding |R(x_t−x*)|_1 to promote positivity around equilibrium.The 1-norm is strictly positive except at x*, while sufficiently large R guarantees local positivity.
  • Controller construction: The controller is a clamped neural network, π(x_t)=clamp(φπ(x_t)−φπ(x*)+u*,u_min,u_max), and it applies u* at equilibrium.Clamping is performed elementwise within the input limits [u_min,u_max].
  • Scope: The approach applies only to systems stabilizable by regular controllers, excluding systems such as a unicycle that require non-regular controllers.The stated regularity examples include locally Lipschitz bounded controllers.
  • MIP verification: The verifier formulates Lyapunov-condition checks as optimization problems over a bounded polytope around the equilibrium, with piecewise-affine objectives suitable for MIP solving.The positivity and decrease conditions are checked through separate objectives.
  • MIP verification: Zero optimal violation values certify the candidate Lyapunov condition, whereas positive values produce counterexamples that falsify the candidate.Maximizing violation yields the worst counterexample, and branch-and-cut can provide additional counterexamples.

B. Trainer

The trainer improves the controller and Lyapunov function jointly after MIP verification identifies violations. Its parameters include the neural-network parameters and the free variables defining the full-rank matrix R.

  • Trainer: Counterexamples from the MIP verifier are used to reduce Lyapunov-condition violations while optimizing the controller and Lyapunov function simultaneously.The searched parameters θ include both network parameters and the variables defining R.

1) Approach 1, growing training set with counter examples:

The first training approach grows sampled-state training sets with MIP-generated counterexamples and minimizes a surrogate violation loss by batched gradient descent. Because the loss is evaluated only on sampled states, this approach can overfit and leave large violations elsewhere.

  • Growing training set: The training sets grow after each MIP solve by appending generated counterexamples, with separate sets for positivity and decrease violations.The two sets are denoted X1 and X2.
  • Surrogate loss: The surrogate loss measures Lyapunov-condition violations on sampled states using vector norms such as the 1-norm, ∞-norm, and 4-norm.The 1-norm measures mean violation, the ∞-norm maximal violation, and the 4-norm smoothly approximates the ∞-norm.
  • Optimization: Batched gradient descent minimizes the surrogate loss over the controller and Lyapunov-function parameters.Algorithm 1 summarizes this iterative procedure.
  • Limitation: Because the loss is computed only on sampled states, gradient descent may overfit the training set and create large violations away from those states.The paper motivates an alternative approach that avoids constructing training sets.

2) Approach 2, minimize the violation via min-max program:

The min-max approach directly minimizes the worst Lyapunov-condition violation, using MIP solutions and gradients with respect to controller and Lyapunov-function parameters.

  • The method minimizes Lyapunov-condition violation through a min-max problem rather than only a surrogate loss on a training set.
  • At each iteration, MIP solvers find the maximal violation, after which gradient descent updates the controller and Lyapunov-function parameters.
  • The inner MIP is simplified by fixing optimal binary variables and retaining active linear constraints.
  • The resulting optimal objective is differentiated by back-propagating a closed-form expression, provided the active constraints and binary solution remain unchanged under perturbation.

C. Computing region of attraction

The region of attraction is approximated by the largest Lyapunov-function sub-level set contained within the verified region where the function is positive definite and strictly decreasing.

  • The inner approximation S is the largest sub-level set V(x_t) ≤ ρ contained in the verified region B.
  • The verified region B is not necessarily invariant, whereas Lyapunov-function sub-level sets are guaranteed to be invariant.
  • The boundary-based optimization is formulated with mixed-integer linear constraints because the Lyapunov function is piecewise affine.
  • The computed inner approximation can be small because the Lyapunov function is fixed while only its sub-level set is searched.

V. RESULTS

The approach synthesizes stabilizing neural-network controllers and Lyapunov functions for an inverted pendulum and quadrotors, with simulations showing convergence beyond some verified regions.

  • The approach synthesizes stable controllers and Lyapunov functions for an inverted pendulum, a 2D quadrotor, and a 3D quadrotor.
  • A. Inverted pendulum: For the inverted pendulum, the synthesized controller is evaluated on both neural-network-approximated and original Lagrangian dynamics.
  • A. Inverted pendulum: The pendulum controller swings up and stabilizes the system despite approximation error in the learned dynamics.
  • A. Inverted pendulum: Simulated pendulum trajectories converge to equilibrium even when initialized outside the verified region of attraction and verified box region.
  • A. Inverted pendulum: Both training algorithms converge within 3 hours for the larger pendulum box 0 ≤ θ ≤ 2π, −5 ≤ ˙θ ≤ 5.

B. 2D quadrotor

For the 2D quadrotor, the neural-network controller stabilizes more sampled states than LQR, while the 3D experiment exposes learned-dynamics discrepancies and differing training scalability.

  • B. 2D quadrotor: More of 10,000 sampled 2D-quadrotor states are stabilized by the neural-network controller than by LQR under Lagrangian dynamics.
  • B. 2D quadrotor: The neural-network controller stabilizes a strict superset of the states stabilized by LQR, partly because it accounts for input limits.
  • B. 2D quadrotor: Both training algorithms find a stabilizing controller for the 2D quadrotor, taking 20 minutes on the small box and 1 day on the larger box.
  • C. 3D quadrotor: The 3D quadrotor controller stabilizes the system, but its learned dynamics have MSE around 10^-4 versus about 10^-6 in other examples.
  • C. 3D quadrotor: On the 3D quadrotor, Algorithm 1 does not converge whereas Algorithm 2 finds a solution, with the authors attributing this to possible training-set overfitting.

VI. CONCLUSION AND FUTURE WORK

The paper demonstrates MIP-based synthesis and certification of neural-network controllers and Lyapunov functions, while identifying scalability and continuous-time dynamics as future challenges.

  • The MIP verifier certifies Lyapunov stability or generates counterexamples for improving the candidate controller and Lyapunov function.
  • Two Algorithm 1 runs on the 2D quadrotor timed out after 6 hours, while only three 3D quadrotor runs were included because they were time-consuming.
  • The approach computes an inner approximation of the closed-loop system’s region of attraction.
  • MIP solving limits scalability because binary variables scale with network neurons and worst-case solution complexity is exponential.
  • The formulation currently applies to discrete-time systems, with continuous-time extension left for future work.
  • The framework can be extended to synthesize barrier functions for certifying that robots remain within safe regions.

VII. APPENDIX

The appendix explains how clamp and ReLU representations are converted into mixed-integer linear constraints for the verifier.

  • Each task uses separate feedforward neural networks for forward dynamics, control policy, and Lyapunov function, all with leaky ReLU activations.
  • Elementwise bounds l ≤ x ≤ u are converted into a mixed-integer linear constraint.
  • The derivation assumes l < 0 and u > 0, while cases with l ≥ 0 or u ≤ 0 are trivial.
  • The clamp function is represented piecewise according to whether x lies below, within, or above its bounds.
  • The clamp representation is rewritten using the ReLU function.
  • Because ReLU functions can be converted to mixed-integer linear constraints, the resulting formulation is an MIP.

C. Necessity of condition (9)

The appendix establishes a scaled Lyapunov-function condition and illustrates why a quadratic function from linearized dynamics may increase under nonlinear quadrotor dynamics.

  • The lemma states that a piecewise-affine Lyapunov function can satisfy a lower bound involving ϵ|R(x − x∗)|1 after suitable scaling.
  • The proof constructs the scaling through directional piecewise-affine functions and the smallest ratio between the candidate Lyapunov function and the required lower bound.
  • The proof concludes the scaled function satisfies the bound ϵ|R(x − x∗)|1 along the direction from x∗ to x.
  • For a 3D quadrotor, the LQR Lyapunov function xT Sx can increase under actual nonlinear dynamics even though it would decrease for linear dynamics.
  • Algorithm convergence is declared when the relevant MIP optimal costs are on the order of 10^-6 because of solver numerical tolerance.
Loading 2109.14152v1…