ReachNN* is a reachability analysis approach based on Bernstein polynomials that can verify neural-network controlled systems (NNCSs) with a more general form of activation functions. We further explore how the specific property, like Lipschitz constant, of the network influences the verification result and propose a new Verification-aware Knowledge Distillation method to distill a new neural network controller that is more verification-friendly and retain the knowledge from the orignal neural network controller.
ReachNN* is a GPU implementation of the originally proposed ReachNN tool and integrate the function of Verification-aware Knowledge Distillation. Experiment results across a set of benchmarks show 7x to 422x efficiency improvement in terms of runtime
ReachNN* can be tested in Virtual Machine, please download it and import the .ova file using Oracle VM Virtual Box.
We have tested our code with RAM size 3072 MB. The tool is stored in folder ~/ReachNNStar.
In the home directory, credentials.txt includes information about user name and password. readme.pdf contains the instruction to test our tool. howto_vbox_shared_folder.txt is the instruction about file sharing between the virtual machine and your desktop. ~/ReachNNStar/checksum_result.txt is for the integrity check.
We note that since VM does not support GPU usage and has limited RAM memory, the runtime result could be different from what we report.
Please skip this step if you are using our tool in the provided VM.
Ubuntu 18.04, Python 3.6
- Install dependencies through apt-get install
sudo apt-get install m4 libgmp3-dev libmpfr-dev libmpfr-doc libgsl-dev gsl-bin bison flex gnuplot-x11 libglpk-dev gcc-8 g++-8 libopenmpi-dev
- Install python libraries
sudo apt-get install python3-pip
sudo pip3 install -U virtualenv
virtualenv --system-site-packages -p python3 ~/venv
source ~/venv/bin/activate
pip install pip --upgrade
pip install -r requirements.txt # Run this command under the repository's root directory
./compile.sh # under the root directory ./ReachNNStar/
Our tool does not include the installation of Sherlock and Verisig for comparison. For the comparison with Verisig and Sherlock results, please refer to the results in ReachNN[1].
Figure 1: Reachability analysis results: Red lines represent boundaries of the obstacles and form the avoid set. Green rectangle represents the target region. Blue rectangle represents the computed flowpipes.
Table 1: Comparison with ReachNN
We provide a example usage to illustrate how to define a NNCS and run verification with ReachNN. Details are included in ReachNNStar_Usage.pdf.
NOTE: All the capitalized word is the input argument and has no suffix.
Please activate the python virtualenv before running any examples.
source ~/venv/bin/activate
We assume the following commands are running under ReachNNStar/ directory.
For example #1 to #5, the program will require at least 3GB RAM to run.
For example #6, the program will require at least 8GB RAM to run.
cd ReachNN
# example 1 to 5
./run_exp.sh
# example 6
# note that this program requires at least 8 GB RAM memory to run.
./run_tora.sh
The verification results will return to ReachNNStar/ReachNN/outputs/SYSTEM.txt.
The computed flowpipes will be plotted to ReachNNStar/ReachNN/outputs/image/SYSTEM.eps after the program is finished.
Please refer to the template in run_exp.sh
The neural network description file is in ReachNNStar/ReachNN/Bernstein_Polynomial_Approximation/nn/
The cpp file that model the system are in ReachNNStar/ReachNN/Bernstein_Polynomial_Approximation/systems/
# SYSTEM is the example's cpp filename and network filename; ERROR_BOUND depends on the system's sensitivity
./example.sh SYSTEM ERROR_BOUND
All results will be stored in ReachNNStar/ReachNN/outputs/
Check the result of SYSTEM
# verification result
vim SYSTEM.txt
# plotted flowpipes
gnuplot SYSTEM.plt
Check the figures in outputs/images/
In this section, the new network will be trained given the original network in example #1, #2 and #6. Then, the new networks are fed to the reachability analysis module to obtain the new verification results.
For example #1 and #2, the program will require at least 3GB RAM to run.
For example #6, the program will require at least 8GB RAM to run.
cd VF_Retraining
# example 1 and 2
./run_distillation_limited_memory.sh
# example 1, 2 and 6
./run_distillation.sh
Please check the result in ReachNNStar/ReachNN/outputs/SYSTEM_retrained.txt and ReachNNStar/ReachNN/outputs/images/SYSTEM_retrained.eps.
The one without the "retrained" suffix is the result of the original network.
cd VF_Retraining
# put the original network NETWORK_FILENAME in folder nn/
cp NETWORK_FILENAME nn/
# run KD to distill a new network
./example.sh NETWORK_FILENAME NETWORK_FILENAME_RETRAINED ACTIVATION L_TARGET REGRESSION_ERROR_BOUND SCALAR OFFSET
The NETWORK_NEW_FILENAME will be shown in folder nn_retrained/.
After distillation, to rerun the reachability analysis on the new NN, execute the following commands:
# put the new network into reachability analysis module
cp nn_retrained/NETWORK_FILENAME_RETRAINED ../ReachNN/Bernstein_Polynomial_Approximation/nn/
# create a new system file to redo reachability analysis
cd ../ReachNN/Bernstein_Polynomial_Approximation/systems
cp NETWORK_FILENAME.cpp NETWORK_FILENAME_RETRAINED.cpp
vim NETWORK_FILENAME_RETRAINED.cpp # change the network name to NETWORK_FILENAME_RETRAINED in the cpp file and change the output file name to NETWORK_FILENAME_RETRAINED too.
cd ../../
./example.sh NETWORK_FILENAME_RETRAINED ERROR_BOUND
All results will be stored in ReachNNStar/ReachNN/Bernstein_Polynomial_Approximation/outputs/
Check the result with NETWORK_FILENAME_RETRAINED
# verification result
vim NETWORK_FILENAME_RETRAINED.txt
# plotted flowpipes
gnuplot NETWORK_FILENAME_RETRAINED.plt
Check the figures in outputs/images/
cd VF_retraining
# If there is less than 8 GB memory, please run the following command
./example_usage_limited_memory.sh
# If there is at least 8GB memory, please run the following command
./example_usage.sh
The results will be reported in ReachNNStar/ReachNN//outputs/ with filename nn_1_relu_tanh_origin.txt and nn_1_relu_tanh_retrained.txt. The plotted flowpipes are shown in ReachNNStar/ReachNN/outputs/images/ with filename nn_1_relu_tanh_origin.eps and nn_1_relu_tanh_retrained.eps.
Jiameng Fan, Chao Huang, Wenchao Li, Xin Chen, Qi Zhu
[1] C.Huang, J.Fan, W.Li, X.Chen, and Q.Zhu. ReachNN: Reachability Analysis of Neural-Network Controlled Systems. ACM Transactions on Embedded Computing Systems (TECS), 18:1–22, October 2019.
[2] J.Fan, C.Huang, W.Li, X.Chen, and Q.Zhu. Towards Verification-Aware Knowledge Distillation for Neural-Network Controlled Systems. International Conference on Computer Aided Design (ICCAD), November 2019.
[3] J.Fan, C.Huang, X.Chen, W.Li, and Q.Zhu. ReachNN*: A Tool for Reachability Analysis ofNeural-Network Controlled Systems. The 18th International Symposium on Automated Technology for Verification and Analysis (ATVA), October 2020 (to appear).
To fix this problem, try to reinstall m4 first
sudo apt-get install --reinstall m4