<<<<<<< HEAD
The files here are to reproduce the examples in the ADHS 2018 paper, "Learning and Verification of Feedback Control Systems using Feedforward Neural Networks." The implementation here uses "sherlock" as a fundamental primitive to solve the reachability problem over Neural Networks.
Sherlock is an output range analysis tool for deep neural networks. The current version can handle only feedforward neural networks, with ReLU activation units.
The only library that is needed is the MILP solver Gurobi. It's free for academic purposes and can be downloaded from here : http://www.gurobi.com/resources/getting-started/mip-basics
Please modify the file Makefile.locale to help us find Gurobi.
For a Mac with the latest gurobi8.00 installed your likely settings will be:
HOST_ARCH=mac64 GUROBI_PATH=/Library/gurobi800
For a linux box, your settins will be:
ARCH=linux64 # if you are using a linux box GUROBI_PATH=/opt/gurobi800
You should feel free to modify these two variables. The Makefile will look for Gurobi headers under
$(GUROBI_PATH)/$ (HOST_ARCH)/include
and libraries under
$(GUROBI_PATH)/$ (HOST_ARCH)/include
Once these are set, you should type
make
It should create all the different executables for each of the examples. Which you should be able to run with the right option. You can chose what option you want by just running it first as :
./run_file_1
The code here implements verification guided training scheme for neural network plant models. The verification scheme uses SHERLOCK to implement range propagation idea, and Tensorflow to train the Neural Network.
2012c5a5da6554e9f0128d96040ba85cc82151e3