  While ensuring stability for linear systems is well understood, it remains a
major challenge for nonlinear systems. A general approach in such cases is to
compute a combination of a Lyapunov function and an associated control policy.
However, finding Lyapunov functions for general nonlinear systems is a
challenging task. To address this challenge, several methods have been proposed
that represent Lyapunov functions using neural networks. However, such
approaches either focus on continuous-time systems, or highly restricted
classes of nonlinear dynamics. We propose the first approach for learning
neural Lyapunov control in a broad class of discrete-time systems. Three key
ingredients enable us to effectively learn provably stable control policies.
The first is a novel mixed-integer linear programming approach for verifying
the discrete-time Lyapunov stability conditions, leveraging the particular
structure of these conditions. The second is a novel approach for computing
verified sublevel sets. The third is a heuristic gradient-based method for
quickly finding counterexamples to significantly speed up Lyapunov function
learning. Our experiments on four standard benchmarks demonstrate that our
approach significantly outperforms state-of-the-art baselines. For example, on
the path tracking benchmark, we outperform recent neural Lyapunov control
baselines by an order of magnitude in both running time and the size of the
region of attraction, and on two of the four benchmarks (cartpole and PVTOL),
ours is the first automated approach to return a provably stable controller.
Our code is available at: https://github.com/jlwu002/nlc_discrete.
