About

This repository contains code for the neural network controller experiment (Section 6.2) in our sampling-based reachability analysis paper (T. Lew, L. Janson, R. Bonalli, M. Pavone, "A Simple and Efficient Sampling-based Algorithm for General Reachability Analysis", 2021).

This code is based on the work of M. Everett et al, see https://github.com/mit-acl/nn_robustness_analysis which this code is forked from.

Differences with the original repository are as follows:

• Implementation of sampling-based reachability analysis algorithms:
  • RandUP (see also https://github.com/StanfordASL/RandUP and https://github.com/StanfordASL/UP)
  • The kernel-based method in (A. Thorpe et al, "Learning Approximate Forward Reachable Sets Using Separating Kernels", L4DC, 2021)
  • GoTube (S. Gruenbacher et al, "GoTube: Scalable stochastic verification of continuous-depth models", AAAI, 2022)
• Computation of the Hausdorff distance (in nn_closed_loop/nn_closed_loop/utils/utils.py)

To reproduce the results in Section 6.2, run:

python -m nn_closed_loop.experiments_randUP_runtime_HausdorffDist
python -m nn_closed_loop.experiments_randUP_reachableSets_plots

The installation of all dependencies is described below, please also see https://github.com/mit-acl/nn_robustness_analysis.

About nn_robustness_analysis (forked from mit-acl/nn_robustness_analysis)

This repository provides Python implementations for the robustness analysis tools in some of our recent papers. This research is supported by Ford Motor Company.

nn_partition

• Michael Everett, Golnaz Habibi, Jonathan P. How, "Robustness Analysis of Neural Networks via Efficient Partitioning with Applications in Control Systems", IEEE LCSS 2020 & ACC 2021.

We introduce the concepts of Analyzer, Propagator, and Partitioner in our LCSS/ACC '21 paper and implement several instances of each concept as a starting point. This modular view on NN robustness analysis essentially defines an API that decouples each component. This decoupling enables improvements in either Propagator or Partitioner algorithms to have a wide impact across many analysis/verification problems.

nn_closed_loop

• Michael Everett, Golnaz Habibi, Chuangchuang Sun, Jonathan P. How, "Reachability Analysis of Neural Feedback Loops", in review.
• Michael Everett, Golnaz Habibi, Jonathan P. How, "Efficient Reachability Analysis for Closed-Loop Systems with Neural Network Controllers", ICRA 2021.

Since NNs are rarely deployed in isolation, we developed a framework for analyzing closed-loop systems that employ NN control policies. The nn_closed_loop codebase follows a similar API as the nn_partition package, leveraging analogous ClosedLoopAnalyzer, ClosedLoopPropagator and ClosedLoopPartitioner concepts. The typical problem statement is: given a known initial state set (and a known dynamics model), compute bounds on the reachable sets for N steps into the future. These bounds provide a safety guarantee for autonomous systems employing NN controllers, as they guarantee that the system will never enter parts of the state space outside of the reachable set bounds.

Reach-LP-Partition	Reach-LP w/ Polytopes

---

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

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:

python -m pip install -e crown_ibp 
python -m pip install -e auto_LiRPA
python -m pip install -e robust_sdp
python -m pip install -e nn_partition
python -m pip install -e nn_closed_loop

You're good to go!

Simple Examples

Try running a simple example where the Analyzer computes bounds on the NN output (given bounds on the NN input):

python -m nn_partition.example \
	--partitioner GreedySimGuided \
	--propagator CROWN_LIRPA \
	--term_type time_budget \
	--term_val 2 \
	--interior_condition lower_bnds \
	--model random_weights \
	--activation relu \
	--show_input --show_output --show_plot

Or, compute reachable sets for a closed-loop system with a pre-trained NN control policy:

python -m nn_closed_loop.example \
	--partitioner None \
	--propagator CROWN \
	--system double_integrator \
	--state_feedback \
	--t_max 5 \
	--show_plot

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

python -m nn_closed_loop.example_backward \
	--partitioner None \
	--propagator CROWN \
	--system double_integrator \
	--state_feedback \
	--show_plot --boundaries polytope

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
• Journal: README

If you find this code useful, please consider citing:

For the partitioning-only code (LCSS/ACC '21):

@article{everett2020robustness,
  title={Robustness Analysis of Neural Networks via Efficient Partitioning with Applications in Control Systems},
  author={Everett, Michael and Habibi, Golnaz and How, Jonathan P},
  journal={IEEE Control Systems Letters},
  year={2021},
  publisher={IEEE},
  doi={10.1109/LCSYS.2020.3045323}
}

For the closed-loop system analysis code (ICRA '21):

@inproceedings{Everett21_ICRA,
    Author = {Michael Everett and Golnaz Habibi and Jonathan P. How},
    Booktitle = {IEEE International Conference on Robotics and Automation (ICRA)},
    Title = {Efficient Reachability Analysis for Closed-Loop Systems with Neural Network Controllers},
    Year = {2021},
    Url = {https://arxiv.org/pdf/2101.01815.pdf},
    }

and/or:

@article{Everett21_journal,
    Author = {Michael Everett and Golnaz Habibi and Chuangchuang Sun and Jonathan P. How},
    Title = {Reachability Analysis of Neural Feedback Loops},
    journal={IEEE Access},
    Year = {2021 (accepted)},
    Url = {https://arxiv.org/pdf/2101.01815.pdf},
    }

TODOS:

• ICRA Fig 3 as single script
• ICRA Fig 3b make pkl
• ICRA Fig 3c from pkl
• get animation working for ICRA

Someday soon...

• add rtdocs (auto-fill code snippets from test files)
• LCSS Fig 8
• Replicate LCSS Table 6b
• Replicate LCSS Table I
• ICRA Fig 4a make pkl
• ICRA Fig 4a from pkl
• ICRA Fig 4b as single script
• ICRA Fig 4b load correct model