Exact forward and backward reachability of deep neural networks with ReLU activation. Associated with the papers:
- Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components (conference version)
- Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems (journal version)
- Julia 1.8.2
- See Project.toml
- For the Taxinet example I use MPT3 (version 3.2.1) with MATLAB R2020a. See the ReadMe for the Taxinet example for more details.
Clone the repository in the desired location:
git clone https://github.com/StanfordMSL/Neural-Network-Reach
In the Neural-Network-Reach directory activate the project:
julia # launch julia REPL
julia> ] # switch to package manager
(@v1.8) pkg> activate .
(Neural-Network-Reach) pkg> instantiate
This creates a Julia environment for the package and sets up all necessary packages.
-
Install
pipandvirtualenvif you don't have them already. -
Clone the repository and navigate to the folder in a terminal.
-
Run
virtualenv venvto make a new virtual environment for the project in the repo folder (the./venv/folder is git ignored so it won't push those files to the repo). -
Activate the virtual environment with:
source venv/bin/activate. -
Install the requirements with:
pip install -r requirements.txt. -
If you've installed new packages and want to add them to the
requirements.txtjust do:pip freeze > requirements.txt.
In pendulum.jl the following should be specified:
copies: How many times the dynamics network should be concatenated.- keyword arguments of
compute_reach(): Specify whether to compute forward and/or backward reachable sets and/or solve a verification problem. Then run the file:
julia> include("pendulum.jl")
In acas.jl the following should be specified:
acas_net(a,b): Argumentsa,bspecify which ACAS network to analyze.property: Current implementation supports"acas property 3"and"acas property 4".- keyword arguments of
compute_reach(): Specify whether to compute forward and/or backward reachable sets and/or solve a verification problem. Then run the file:
julia> include("acas.jl")
In random.jl the following should be specified:
in_d, out_d, hdim, layers: Arguments are input dimension, output dimension, hidden layer dimension, and number of layers.- keyword arguments of
compute_reach(): Specify whether to compute forward and/or backward reachable sets and/or solve a verification problem. Then run the file:
julia> include("random.jl")
In vanderpol_roa.jl the following should be specified:
steps: A list of the number of steps to compute for the BRS.
Then run the file:
julia> include("vanderpol_roa.jl")