This repository contains code to reproduce the neural feedback loop analysis experiment (Section XI.B) from our paper on convex hull reachability analysis (T. Lew, R. Bonalli, M. Pavone, "Convex Hulls of Reachable Sets", 2024).

This code is a branch of the fork at https://github.com/StanfordASL/nn_robustness_analysis of https://github.com/mit-acl/nn_robustness_analysis with minor modifications. This branch only supports the experiments of the paper and changes may break previous functionalities (for those, please revert to the RandUP branch). This code supports (a) 2d integrator system, (b) continuous-time reachability problem with uncertain initial state under disturbances, (c) ReachLP, RandUP, and Algorithm 1 (see pmpUP.py and Dynamics.py), (d) ReLU activations are automatically replaced with SoftPlus activations (see crown_ibp/crown_ibp/bound_layers.py). We refer to the paper for further details.

To reproduce results, run:

python -m nn_closed_loop.experiments_with_disturbances

For installation instructions, see the previous instructions below.

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.

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

• 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.

• 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

git clone --recursive <this_repo>

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!

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

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

• LCSS/ACC '21: README
• ICRA '21: README
• Journal: README

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},
    }

• 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