This repo contains the code for the two papers

• Counter-example guided synthesis of neural network Lyapunov functions for piecewise linear systems
  Hongkai Dai, Benoit Landry, Marco Pavone and Russ Tedrake
  IEEE Conference on Decision and Control, 2020
  video
• Lyapunov-stable neural-network control
  Hongkai Dai, Benoit Landry, Lujie Yang, Marco Pavone and Russ Tedrake
  Robotics: Science and Systems, 2021
  video

We can synthesize neural-network controllers with Lyapunov stability guarantees. Namely for all the initial states within a certain region, the controller will drive the system from these initial states to converge to the goal state.

We use python 3 in this project. You could first install the packages in requirements.txt.

Please run

pip install -e .

to install the package together with the dependencies.

Please refer to https://support.gurobi.com/hc/en-us/articles/360044290292-How-do-I-install-Gurobi-for-Python- on setting up Gurobi. Note that by default Gurobi ships with a limited license that has size limits on the optimization problem. Please refer to https://support.gurobi.com/hc/en-us/articles/360051597492 on using your own academic or commential license.

You could run

$ python3 neural_network_lyapunov/test/train_toy_system_controller_demo.py --dimension=1

This will synthesize a stabilizing controller with a Lyapunov function for a toy 1D system (TODO: add some visualization at the end of the demo). You should see that the error printed on the screen decreases to almost 0. (The code is non-deterministic, so if it doesn't converge to 0 in the first trial, you can re-run the demo and hopefully it converges in the second trial).

We use flake8 to check if the python code follows PEP standard. Before submitting the PR, you could run

$ cd neural_network_lyapunov
$ flake8 ./

to check if there are any violations.

I am a strong believer of unit test. We strongly encourage to add tests to the functions in the PR.