Formalise 2025

code/nnv/examples/Submission/FORMALISE2025/.env

@@ -0,0 +1,2 @@
+NNV_PATH='' # replace with '/path/to/nnv' 
+NPY_MATLAB_PATH='' # replace with '/path/to/npy-matlab/npy-matlab'

code/nnv/examples/Submission/FORMALISE2025/.gitignore

@@ -0,0 +1,14 @@
+.DS_Store
+
+# don't commit the data
+*data/ZoomIn*
+*data/ZoomOut*
+*data/GTSRB*
+*data/STMNIST*
+
+# matlab stuff
+*.asv
+*tbxmanager*
+
+# python stuff
+*__pycache__*

code/nnv/examples/Submission/FORMALISE2025/LICENSE.txt

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2024
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

code/nnv/examples/Submission/FORMALISE2025/README.md

@@ -0,0 +1,105 @@
+# (Artifact) Robustness Verification of Video Classification Neural Networks
+
+This artifact is used to reproduce the results in _Robustness Verification of Video Classification Neural Networks_.
+
+All results from _Robustness Verification of Video Classification Neural Networks_ were captured using an Apple M1 Max 10-core [email protected]×10 with 64GB of RAM. The times reported to run the smoke test and reproduce results are approximated based on this computer.
+
+# Requirements
+
+The following resources are required to run this artifact:
+
+- MATLAB 2024a with NNV and npy-matlab installed and added to the path.
+- conda environment with Python v3.11. Install rquirements from requirements.txt. Make sure to install the source files.
+
+# Installation
+
+1. Clone NNV and npy-matlab and install them ensuring that both have been added to the MATLAB path.
+
+```
+# Clone NNV and npy-matlab
+git clone --recursive https://github.com/verivital/nnv.git
+git clone https://github.com/kwikteam/npy-matlab.git
+```
+
+Follow the instructions under heading `# Installation:` on [NNV's README](https://github.com/verivital/nnv/blob/master/README.md). Note, if using a computer with an Apple silicon CPU, then it may be necessary to remove a line from NNV's `install.m` script. The following line
+
+```matlab
+tbxmanager install lcp hysdel cddmex clpmex glpkmex fourier sedumi;
+```
+
+can be removed/commented out.
+
+For `npy-matlab`, add and save the path to MATLAB. Again, instructions are available on [`npy-matlab`'s README](https://github.com/kwikteam/npy-matlab/blob/master/README.md).
+
+2. Download the following dataset files from here into the `FORMALISE2025/data` folder:
+
+-
+
+3. Create a conda environment with `Python v3.11` and install the requirements from `requirements.txt`. Additionally, install the source files to the environment. Both can be done by running the following commands from the root directory (`FORMALISE2025`):
+
+   ```bash
+   pip install -r requirements.txt
+
+   # before installing source files, make sure to navigate to this src directory, e.g.
+   cd /path/to/FORMALISE2025/src
+   pip install -e .
+   ```
+
+4. Modify the `verify.py` file to add the path to your NNV and npy-matlab directories (the repositories that were cloned earlier). For the `npy-matlab` repository, you'll want to reference the subfolder in the directory also called `npy-matlab`, e.g. `/some/path/to/npy-matlab/npy-matlab`.
+
+5.
+
+# Smoke Test Instructions (~30 minutes)
+
+Instructions to quickly test the software needed to reproduce the artifacts of the paper. If no issues arise during the smoke test, you can safely proceed to reproducing all artifacts as described in the below section.
+
+1. Open a terminal and navigate to the `FORMALISE2025` directory.
+2. Make sure the conda environment with the installed dependencies is activated.
+3. Run the following command to enable the smoke test script to be executed and then run it:
+
+```bash
+chmod +x run_smoketest.sh && ./run_smoketest.sh
+```
+
+4. The smoketest will verify a single sample from each of the different datasets and with the different verification algorithms. The results will be output to a `smoketest_outputs.txt` file. Assuming everything ran smoothly, you should see:
+
+```
+**********************************************
+              Smoke test complete.
+**********************************************
+```
+
+# Reproducing the Full Results
+
+Assuming the average runtime for the experiments remains as shown in the paper, then it will take approximately 9-10 days to reproduce the results. As such, there will also be an intermediary where we verify 1/10 samples verified in the full experiments. Those instructions will be in the next section. For now, we discuss how to reproduce the full results. The instructions will be the exact same for running the smoke test, only we use a different script.
+
+1. Open a terminal and navigate to the `FORMALISE2025` directory.
+2. Make sure the conda environment with the installed dependencies is activated.
+3. Run the following command to begin reproducing the artifacts:
+
+```bash
+chmod +x run_vvn.sh && ./run_vvn.sh
+```
+
+# Reproducing a Subset of the Results
+
+This set of instructions is for reproducing a subset of the results. In this case, we verify every tenth sample from what was done for the original verification. Generating the reachable output range plots remains the same.
+
+1. Open a terminal and navigate to the `FORMALISE2025` directory.
+2. Make sure the conda environment with the installed dependencies is activated.
+3. Run the following command to begin reproducing a subset of the artifacts:
+
+```bash
+chmod +x run_subset_vvn.sh && run_subset_vvn.sh
+```
+
+# Results
+
+| Artifact | Filepath                                                                  | Description                                                                                                                                                     |
+| -------- | ------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------- |
+| Table II | `results/table2.txt                                                       | A table of results (PSRV and average runtime) for all experiments.                                                                                              |
+| Fig. 7   | `results/reach_stmnist_plot.png` and `results/reach_bad_stmnist_plot.png` | Plots of the reachable output ranges on a sample of STMNIST with different epsilon values (one robust, the other non-robust).                                   |
+| Fig. 8   | `results/runtime_comp.png`                                                | A visualization of how average runtime changes for the Zoom In, Zoom Out, and GTSRB datasets as the number of frames and magnitude of the perturbation changes. |
+
+<!-- ### requirements.txt -->
+<!-- Numpy could not be upgraded from 1.26.4 to 2.0.0 because of some incompatability with onnxruntime. -->

code/nnv/examples/Submission/FORMALISE2025/data/about.txt

@@ -0,0 +1 @@
+The datasets are too large to be pushed to the repository. Please navigate to the release to find the dataset files and put them in this directory accordingly.

code/nnv/examples/Submission/FORMALISE2025/requirements.txt

@@ -0,0 +1,25 @@
+coloredlogs==15.0.1
+contourpy==1.2.1
+cycler==0.12.1
+eagerpy==0.30.0
+flatbuffers==24.3.25
+fonttools==4.53.0
+humanfriendly==10.0
+kiwisolver==1.4.5
+matlabengine==24.1.2
+matplotlib==3.9.0
+mpmath==1.3.0
+numpy==1.26.4
+onnxruntime==1.18.0
+packaging==24.1
+pillow==10.3.0
+protobuf==5.27.1
+pyparsing==3.1.2
+python-dateutil==2.9.0.post0
+python-dotenv==1.0.1
+requests==2.32.3
+scipy==1.14.1
+six==1.16.0
+sympy==1.12.1
+typing_extensions==4.12.2
+urllib3==2.2.3

code/nnv/examples/Submission/FORMALISE2025/run_smoketest.sh

@@ -0,0 +1,95 @@
+#!/bin/bash
+
+OUTPUT_FILE="smoketest_outputs.txt"
+
+# Clear the file if it exists
+> $OUTPUT_FILE
+
+echo "Starting smoke test..."
+echo "Starting smoke test..." >> $OUTPUT_FILE
+
+#######################
+### ZOOM IN RESULTS ### 
+#######################
+# Zoom In 4f, relax
+python src/vvn/verify.py zoom_in relax 1 4 1800 751 >> $OUTPUT_FILE 2>&1
+
+# Zoom In 8f, relax
+python src/vvn/verify.py zoom_in relax 1 8 1800 751 >> $OUTPUT_FILE 2>&1
+
+# Zoom In 16f, relax
+python src/vvn/verify.py zoom_in relax 1 16 1800 751 >> $OUTPUT_FILE 2>&1
+
+# Zoom In 4f, approx
+python src/vvn/verify.py zoom_in approx 1 4 1800 751 >> $OUTPUT_FILE 2>&1
+
+# Zoom In 8f, approx
+python src/vvn/verify.py zoom_in approx 1 8 1800 751 >> $OUTPUT_FILE 2>&1
+
+
+########################
+### ZOOM OUT RESULTS ### 
+########################
+# Zoom Out 4f, relax
+python src/vvn/verify.py zoom_out relax 1 4 1800 624 >> $OUTPUT_FILE 2>&1
+
+# Zoom Out 8f, relax
+python src/vvn/verify.py zoom_out relax 1 8 1800 624 >> $OUTPUT_FILE 2>&1
+
+# Zoom Out 16f, relax
+python src/vvn/verify.py zoom_out relax 1 16 1800 624 >> $OUTPUT_FILE 2>&1
+
+# Zoom Out 4f, approx
+python src/vvn/verify.py zoom_out approx 1 4 1800 624 >> $OUTPUT_FILE 2>&1
+
+# Zoom Out 8f, approx
+python src/vvn/verify.py zoom_out approx 1 8 1800 624 >> $OUTPUT_FILE 2>&1
+
+
+#######################
+#### GTSRB RESULTS ####
+#######################
+# GTSRB 4f, relax
+python src/vvn/verify.py gtsrb relax 1 4 1800 12597 >> $OUTPUT_FILE 2>&1
+
+# GTSRB 8f, relax
+python src/vvn/verify.py gtsrb relax 1 8 1800 12597 >> $OUTPUT_FILE 2>&1
+
+# GTSRB 16f, relax
+python src/vvn/verify.py gtsrb relax 1 16 1800 12597 >> $OUTPUT_FILE 2>&1
+
+# GTSRB 4f, approx
+python src/vvn/verify.py gtsrb approx 1 4 1800 12597 >> $OUTPUT_FILE 2>&1
+
+# GTSRB 8f, approx
+python src/vvn/verify.py gtsrb approx 1 8 1800 12597 >> $OUTPUT_FILE 2>&1
+
+# GTSRB 16f, approx
+python src/vvn/verify.py gtsrb approx 1 16 1800 12597 >> $OUTPUT_FILE 2>&1
+
+
+#######################
+### STMNIST RESULTS ### 
+#######################
+# STMNIST 16f, relax
+python src/vvn/verify.py stmnist relax 1 16 1800 311 >> $OUTPUT_FILE 2>&1
+
+# STMNIST 32f, relax
+python src/vvn/verify.py stmnist relax 1 32 1800 311 >> $OUTPUT_FILE 2>&1
+
+# STMNIST 64f, relax
+python src/vvn/verify.py stmnist relax 1 64 1800 311 >> $OUTPUT_FILE 2>&1
+
+# STMNIST 16f, approx
+python src/vvn/verify.py stmnist approx 1 16 1800 311 >> $OUTPUT_FILE 2>&1
+
+# STMNIST 32f, approx
+python src/vvn/verify.py stmnist approx 1 32 1800 311 >> $OUTPUT_FILE 2>&1
+
+# STMNIST 64f, approx
+python src/vvn/verify.py stmnist approx 1 64 1800 311 >> $OUTPUT_FILE 2>&1
+
+
+echo -e "\n\n**********************************************"
+echo "              Smoke test complete.         "
+echo -e "**********************************************\n\n"

code/nnv/examples/Submission/FORMALISE2025/run_subset_vvn.sh

@@ -0,0 +1,14 @@
+#!/bin/bash
+# TABLE II (GET ALL VERIFICATION RESULTS)
+python src/run.py subset # MNIST Video
+python src/run_gtsrb.py subset # GTSRB
+python src/run_stmnist.py subset # STMNIST
+python src/analysis/make_table2.py
+
+
+# FIGURE 8 (COMPARISON OF AVERAGE RUNTIME)
+python src/analysis/make_plots.py
+
+
+# FIGURE 7 (REACHABLE OUTPUT PLOTS)
+python src/generate_output_plots.py

code/nnv/examples/Submission/FORMALISE2025/run_vvn.sh

@@ -0,0 +1,14 @@
+#!/bin/bash
+# TABLE II (GET ALL VERIFICATION RESULTS)
+python src/run.py # MNIST Video
+python src/run_gtsrb.py # GTSRB
+python src/run_stmnist.py # STMNIST
+python src/analysis/make_table2.py
+
+
+# FIGURE 8 (COMPARISON OF AVERAGE RUNTIME)
+python src/analysis/make_plots.py
+
+
+# FIGURE 7 (REACHABLE OUTPUT PLOTS)
+python src/generate_output_plots.py