Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Installation script with instructions #248

Merged
merged 3 commits into from
Nov 26, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 26 additions & 10 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,22 @@ _Previous_
* Earliest version: https://doi.org/10.24433/CO.1314285.v1

# Installation:

1. Clone or download the NNV toolbox from (https://github.com/verivital/nnv)

Note: to operate correctly, nnv depends on other tools (CORA, NNMT, HyST, onnx2nnv), which are included as git submodules. As such, you must clone recursively, e.g., with the following:
```
git clone --recursive https://github.com/verivital/nnv.git
```

2. If running in Ubuntu, install MATLAB and proceed to run the provided installation script (then, skip to step 6).

```
chmod +x install_ubuntu.sh
./install_ubuntu.sh
```

1. Install MATLAB (2022b or newer) with at least the following toolboxes:
3. For MacOS and Windows, please install MATLAB (2023a or newer) with at least the following toolboxes:
* Computer Vision
* Control Systems
* Deep Learning
Expand All @@ -31,23 +45,17 @@ _Previous_
* Symbolic Math
* System Identification

2. Install the following support package
4. Install the following support package
[Deep Learning Toolbox Converter for ONNX Model Format](https://www.mathworks.com/matlabcentral/fileexchange/67296-deep-learning-toolbox-converter-for-onnx-model-format)

Note: Support packages can be installed in MATLAB's HOME tab > Add-Ons > Get Add-ons, search for the support package using the Add-on Explorer and click on the Install button.

3. Clone or download the NNV toolbox from (https://github.com/verivital/nnv)

Note: to operate correctly, nnv depends on other tools (CORA, NNMT, HyST, onnx2nnv), which are included as git submodules. As such, you must clone recursively, e.g., with the following:
```
git clone --recursive https://github.com/verivital/nnv.git
```

4. Open MATLAB, then go to the directory where NNV exists on your machine, then run the `install.m` script located at /nnv/
5. Open MATLAB, then go to the directory where NNV exists on your machine, then run the `install.m` script located at /nnv/

Note: if you restart Matlab, rerun either install.m or startup_nnv.m, which will add the necessary dependencies to the path; you alternatively can run `savepath` after installation to avoid this step after restarting Matlab, but this may require administrative privileges

5. Optional installation packages
6. Optional installation packages

a. To run verification for convolutional neural networks (CNNs) on VGG16/VGG19, additional support packages must be installed:

Expand Down Expand Up @@ -140,6 +148,14 @@ The methods implemented in NNV are based upon or used in the following papers:

* Diego Manzanas Lopez, Sung Woo Choi, Hoang-Dung Tran, Taylor T. Johnson, "NNV 2.0: The Neural Network Verification Tool". In: Enea, C., Lal, A. (eds) Computer Aided Verification. CAV 2023. Lecture Notes in Computer Science, vol 13965. Springer, Cham. [https://doi.org/10.1007/978-3-031-37703-7_19]

* Anne M Tumlin, Diego Manzanas Lopez, Preston Robinette, Yuying Zhao, Tyler Derr, and Taylor T Johnson. "FairNNV: The Neural Network Verification Tool For Certifying Fairness. In Proceedings of the 5th ACM International Conference on AI in Finance (ICAIF '24)". Association for Computing Machinery, New York, NY, USA, 36–44. [https://doi.org/10.1145/3677052.3698677]

* Taylor T. Johnson, Diego Manzanas Lopez and Hoang-Dung. Tran, "Tutorial: Safe, Secure, and Trustworthy Artificial Intelligence (AI) via Formal Verification of Neural Networks and Autonomous Cyber-Physical Systems (CPS) with NNV," 2024 54th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume (DSN-S), Brisbane, Australia, 2024, pp. 65-66, [https://doi.org/10.1109/DSN-S60304.2024.00027]

* Preston K. Robinette, Diego Manzanas Lopez, Serena Serbinowska, Kevin Leach, and Taylor T Johnson. "Case Study: Neural Network Malware Detection Verification for Feature and Image Datasets". In Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE) (FormaliSE '24). Association for Computing Machinery, New York, NY, USA, 127–137. [https://doi.org/10.1145/3644033.3644372]

* Hoang-Dung Tran, Diego Manzanas Lopez, and Taylor Johnson. "Tutorial: Neural Network and Autonomous Cyber-Physical Systems Formal Verification for Trustworthy AI and Safe Autonomy". In Proceedings of the International Conference on Embedded Software (EMSOFT '23). Association for Computing Machinery, New York, NY, USA, 1–2. [https://doi.org/10.1145/3607890.3608454]

* Neelanjana Pal, Diego Manzanas Lopez, Taylor T Johnson, "Robustness Verification of Deep Neural Networks using Star-Based Reachability Analysis with Variable-Length Time Series Input", to be presented at FMICS 2023. [https://arxiv.org/pdf/2307.13907.pdf]

* Mykhailo Ivashchenko, Sung Woo Choi, Luan Viet Nguyen, Hoang-Dung Tran, "Verifying Binary Neural Networks on Continuous Input Space using Star Reachability," 2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), Melbourne, Australia, 2023, pp. 7-17, [https://doi.org/10.1109/FormaliSE58978.2023.00009]
Expand Down
3 changes: 3 additions & 0 deletions code/nnv/startup_nnv.m
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
fprintf('\nAdding dependencies to Matlab path...\n');

if ~exist("tbxmanager.m","file") % not added to the path
addpath("tbxmanager");
end
tbxmanager restorepath

fprintf('\nAdding NNV to Matlab path...\n');
Expand Down
2 changes: 1 addition & 1 deletion code/nnv/tests/io/test_io.m
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@

%% Test 3: Load onnx model
if ~is_github_actions() % importers (support packages) are not installed in MATLAB actions
net_onnx = importONNXNetwork('mobilenetv2-1.0.onnx');
net_onnx = importNetworkFromONNX('mobilenetv2-1.0.onnx');
% net = matlab2nnv(net_onnx);
% This should get error:
% nnet.cnn.layer.GroupedConvolution2DLayer unsupported
Expand Down
24 changes: 24 additions & 0 deletions install_ubuntu.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
#!/bin/bash

# VARS
MATLAB_RELEASE=2024b # latest
EXISTING_MATLAB_LOCATION=$(dirname $(dirname $(readlink -f $(which matlab))))
# (assume no products are installed yet)
ADDITIONAL_PRODUCTS="Computer_Vision_Toolbox Control_System_Toolbox Deep_Learning_Toolbox Image_Processing_Toolbox Optimization_Toolbox Parallel_Computing_Toolbox Statistics_and_Machine_Learning_Toolbox Symbolic_Math_Toolbox System_Identification_Toolbox Deep_Learning_Toolbox_Converter_for_ONNX_Model_Format Deep_Learning_Toolbox_Converter_for_TensorFlow_Models"
CURR_DIR=$(pwd)


# MATLAB INSTALLATION
wget -q https://www.mathworks.com/mpm/glnxa64/mpm \
&& chmod +x mpm \
&& ./mpm install \
--destination=${EXISTING_MATLAB_LOCATION} \
--release=r${MATLAB_RELEASE} \
--products ${ADDITIONAL_PRODUCTS}

# -------------------------------------------------------------------------
# NNV INSTALLATION
matlab -nodisplay -r "cd ${CURR_DIR}; cd code/nnv/; install; exit()"


# DONE
Loading