nfl-veripy 0.0.1a4

A small example package

Updates

• 2023-04-19: Major cleanup and re-branding of repo, released PyPi package for easier usability!
• 2023-04-13: Add new jax-based propagators, including some from DRIP paper. Cleaned up implementation of BReach-LP and HyBReach-LP from OJCSYS paper.
• 2022-06-20: Add new backprojection code from BReach-LP paper. More info here
• 2022-05-09: Add new N-Step ClosedLoopPropagator. Rather than recursively computing reachable sets (suffers from the wrapping effect), we see improved performance by solving an LP directly for the reachable set N steps in the future. You can experiment with this using the CROWNNStep flag in nfl_veripy/example.py.
• 2022-05-09: Add new MILP-based ClosedLoopPropagator, using OVERT. Note that this component requires a Julia installation, and we pass data between Python and Julia using a lightweight local HTTP server. More info here.

About

nfl_veripy: Closed-Loop Analysis (NNs in feedback loops) -- includes Reach-LP and BReach-LP

Handles problems such as:

• Given a set of possible initial states, a trained NN controller, and a known dynamics model, compute outer bounds on the set of possible future states (forward reachable sets).
• Given a set of terminal states, a trained NN controller, and a known dynamics model, compute inner/outer bounds on the set of possible initial states that will/won't lead to the terminal state set (backprojection sets).

For more info, please see this README and this README.

Setup

If you just want to run the code, you can simply install our package via pip:

pip install "jax_verify @ git+https://gitlab.com/mit-acl/ford_ugvs/jax_verify.git" \
    "crown_ibp @ git+https://gitlab.com/mit-acl/ford_ugvs/crown_ibp.git" \
    nfl_veripy

Aside: We acknowledge that the above method for installing jax_verify and crown_ibp (dependencies of nfl_veripy) in the above way is a little unconventional. It would be better to simply include these as dependencies of nfl_veripy and let pip find those packages, but (a) those packages are not available (or are too outdated) on PyPI, and (b) it is not allowed to include dependencies with direct URLs when releasing a package on PyPI. If there's a better way of doing this we would love to hear about it!

Simple Examples

Compute forward reachable sets for a closed-loop system with a pre-trained NN control policy:

python -m nfl_veripy.example --config example_configs/icra21/fig3_reach_lp.yaml

Compute backward reachable sets for a closed-loop system with a pre-trained NN control policy:

python -m nfl_veripy.example --config example_configs/ojcsys23/di_breach.yaml

Jupyter Notebooks

Please see the jupyter_notebooks folder for an interactive version of the above examples.

Replicate plots from the papers:

• LCSS/ACC '21: README
• ICRA '21: README
• IEEE Access '21: README
• CDC '22: README
• ACC '23 (to appear): Coming soon!
• OJCSYS '23 (to appear): Coming soon!
• LCSS '23 (to appear): Coming soon!

If you find this code useful, please consider citing our work:

• Everett, M. (2021, December). Neural network verification in control. In 2021 60th IEEE Conference on Decision and Control (CDC) (pp. 6326-6340). IEEE.
• Everett, M., Habibi, G., & How, J. P. (2020). Robustness analysis of neural networks via efficient partitioning with applications in control systems. IEEE Control Systems Letters, 5(6), 2114-2119.
• Everett, M., Habibi, G., Sun, C., & How, J. P. (2021). Reachability analysis of neural feedback loops. IEEE Access, 9, 163938-163953.
• Everett, M., Habibi, G., & How, J. P. (2021, May). Efficient reachability analysis of closed-loop systems with neural network controllers. In 2021 IEEE International Conference on Robotics and Automation (ICRA) (pp. 4384-4390). IEEE.
• Rober, N., Everett, M., & How, J. P. (2022, December). Backward reachability analysis for neural feedback loops. In 2022 IEEE 61st Conference on Decision and Control (CDC) (pp. 2897-2904). IEEE.
• Rober, N., Everett, M., Zhang, S., & How, J. P. (2022). A Hybrid Partitioning Strategy for Backward Reachability of Neural Feedback Loops. arXiv preprint arXiv:2210.07918.
• Rober, N., Katz, S. M., Sidrane, C., Yel, E., Everett, M., Kochenderfer, M. J., & How, J. P. (2023). Backward reachability analysis of neural feedback loops: Techniques for linear and nonlinear systems. IEEE Open Journal of Control Systems.
• Everett, M., Bunel, R., & Omidshafiei, S. (2023). Drip: Domain refinement iteration with polytopes for backward reachability analysis of neural feedback loops. IEEE Control Systems Letters.

Acknowledgements

This research is supported in part by Ford Motor Company.

We build on excellent open-source repositories from the neural network analysis community. These repositories are imported as Git submodules or re-implemented in Python here, with some changes to reflect the slightly different problem statements:

• auto_LIRPA
• crown_ibp
• robust_nn
• nnv
• jax_verify

TODOS:

• add rtdocs (auto-fill code snippets from test files)
• add installation instructions & tests for julia code

Developer Setup

If you want to work directly with the source code, here is how we set up our development environments.

Get the code

git clone --recursive <this_repo>

Install

You might need to install these dependencies on Linux (for cvxpy's SCS solver and to generate reasonably sized animation files) (did not need to on OSX):

sudo apt-get install libblas-dev liblapack-dev gifsicle

Create a virtualenv for this repo:

python -m virtualenv venv
source venv/bin/activate

Install the various python packages in this repo in editable mode (-e):

python -m pip install -e third_party/crown_ibp third_party/jax_verify third_party/auto_LiRPA .

You're good to go!

packaging info

cd nfl_veripy
python -m build
python -m twine upload --repository testpypi dist/nfl_veripy-0.0.1a0*

python -m pip install "jax_verify @ git+https://gitlab.com/mit-acl/ford_ugvs/jax_verify.git" "crown_ibp @ git+https://gitlab.com/mit-acl/ford_ugvs/crown_ibp.git"
python -m pip install --extra-index-url https://test.pypi.org/simple/ nfl-veripy==0.0.1.a3