update nnneum

.gitignore

@@ -13,3 +13,6 @@ __pycache__
 *branch_str.txt
 *.mypy_cache
 .coverage
+examples/acasxu/out.txt
+examples/acasxu/results/*
+out.txt

.travis.yml

@@ -0,0 +1,17 @@
+
+# configuration file for continuous integration testing using travis-ci.com
+
+dist:
+ - jammy
+
+python: 3.8
+
+services:
+  - docker
+
+script:
+# build Docker container
+- docker build -t nnenum .
+
+# run tests
+- docker run nnenum

Dockerfile

@@ -6,7 +6,7 @@
 # To get a shell after building the image:
 # docker run -ir nnenum_image bash
 
-FROM tensorflow/tensorflow:2.2.0
+FROM python:3.10
 
 COPY ./requirements.txt /work/requirements.txt
 
@@ -17,9 +17,12 @@ WORKDIR /work
 RUN pip3 install -r requirements.txt
 
 # set environment variables
-ENV PYTHONPATH=$PYTHONPATH:/work/nnenum
+ENV PYTHONPATH=$PYTHONPATH:/work/src
 ENV OPENBLAS_NUM_THREADS=1
 ENV OMP_NUM_THREADS=1
 
 # copy remaining files to docker
-COPY . /work
+COPY . /work
+
+# cmd, run one of each benchmark
+CMD cd /work && ./run_tests.sh

README.md

@@ -1,17 +1,47 @@
+[![Build Status](https://travis-ci.com/stanleybak/nnenum.svg?branch=master)](https://app.travis-ci.com/github/stanleybak/nnenum)
+
 # nnenum - The Neural Network Enumeration Tool
-**nnenum** (pronounced *en-en-en-um*) is a high-performance neural network verification tool. Multiple levels of abstraction are used to quickly verify ReLU networks without sacrificing completeness. Analysis combines three types of zonotopes with star set (triangle) overapproximations, and uses [efficient parallelized ReLU case splitting](http://stanleybak.com/papers/bak2020cav.pdf). The verification tree search can be augmented with adversarial example generation using multiple attacks from the [foolbox library](https://github.com/bethgelab/foolbox) to quickly find property violations. The tool is written in Python 3, uses GLPK for LP solving and directly accepts [ONNX](https://github.com/onnx/onnx) network files as input. The [ImageStar trick](https://arxiv.org/abs/2004.05511) allows sets to be quickly propagated through all layers supported by the [ONNX runtime](https://github.com/microsoft/onnxruntime), such as convolutional layers with arbitrary parameters.
+**nnenum** (pronounced *en-en-en-um*) is a high-performance neural network verification tool. Multiple levels of abstraction are used to quickly verify ReLU networks without sacrificing completeness. Analysis combines three types of zonotopes with star set (triangle) overapproximations, and uses [efficient parallelized ReLU case splitting](http://stanleybak.com/papers/bak2020cav.pdf). The tool is written in Python 3, uses GLPK for LP solving and directly accepts [ONNX](https://github.com/onnx/onnx) network files and `vnnlib` specifications as input. The [ImageStar trick](https://arxiv.org/abs/2004.05511) allows sets to be quickly propagated through all layers supported by the [ONNX runtime](https://github.com/microsoft/onnxruntime), such as convolutional layers with arbitrary parameters.
 
 The tool is written by Stanley Bak ([homepage](http://stanleybak.com), [twitter](https://twitter.com/StanleyBak)).
 
 ### Getting Started
-The `Dockerfile` shows how to install all the dependencies (mostly python packages) and set up the environment. Although the tool loads neural networks directly from ONNX files, the properties and initial sets and verification settings must be defined in python scripts.
+The `Dockerfile` shows how to install all the dependencies (mostly python packages) and set up the environment. The tool loads neural networks directly from ONNX files and properties to check from `vnnlib` files.
+For example, try running:
 
-The best way to get started is to look at some of the examples. For example, in the `examples/acasxu` directory you can try to verify property 9 of network 3-3 of the [well-studied ACAS Xu neural network verification benchmarks](https://arxiv.org/abs/1702.01135) by running the command: 
+```
+python3 -m nnenum.nnenum examples/acasxu/data/ACASXU_run2a_3_3_batch_2000.onnx examples/acasxu/data/prop_9.vnnlib
+```
 
-```python3 acasxu_single.py 3 3 9```
+You can see a few more examples in `run_tests.sh`.
 
 ### VNN 2020 Neural Network Verification Competition (VNN-COMP) Version
-The nnenum tool performed well in VNN-COMP 2020, being the only tool to verify all the ACAS-Xu benchmarks (each in under 10 seconds), as well as one of the best on the MNIST and CIFAR-10 benchmarks. The version used for the competition as well as model files and scripts to run the compeition benchmarks are in the `vnn2020` branch.
+The nnenum tool performed well in VNN-COMP 2020, being the only tool to verify all the ACAS-Xu benchmarks (each in under 10 seconds). The version used for the competition as well as model files and scripts to run the compeition benchmarks are in the `vnn2020` branch.
 
 ### CAV 2020 Paper Version
 The CAV 2020 paper ["Improved Geometric Path Enumeration for Verifying ReLU Neural Networks"](http://stanleybak.com/papers/bak2020cav.pdf) by S. Bak, H.D Tran, K. Hobbs and T. T. Johnson corresponds to optimizations integrated into the exact analysis mode of nnenum, which also benefits overapproximative analysis. The paper version and repeatability evaluation package instructions are available [here](http://stanleybak.com/papers/bak2020cav_repeatability.zip).
+
+### Citing nnenum ###
+The following citations can be used for nnenum:
+
+```
+@inproceedings{bak2021nfm,
+  title={nnenum: Verification of ReLU Neural Networks with Optimized Abstraction Refinement},
+  author={Bak, Stanley},
+  booktitle={NASA Formal Methods Symposium},
+  pages={19--36},
+  year={2021},
+  organization={Springer}
+}
+```
+
+```
+@inproceedings{bak2020cav,
+  title={Improved Geometric Path Enumeration for Verifying ReLU Neural Networks},
+  author={Bak, Stanley and Tran, Hoang-Dung and Hobbs, Kerianne and Johnson, Taylor T.},
+  booktitle={Proceedings of the 32nd International Conference on Computer Aided Verification},
+  year={2020},
+  organization={Springer}
+}
+```
+

examples/acasxu/README.md

@@ -1,5 +1,5 @@
 These are the well-studied ACAXU benchmarks from "Reluplex: An efficient SMT solver for verifying deep neural networks" by Katz, Guy, et al., CAV 2017.
 
-To run a specific bencmark, such as network 3-3 with property 9, execute 'python3 acasxu_single.py 3 3 9'
+To run a specific bencmark, such as network 3-3 with property 9, execute 'python3 -m nnenum.nnenum data/ACASXU_run2a_3_3_batch_2000.onnx data/prop_9.vnnlib'
 
 To run all the benchmarks, run acasxu_all.py (results summary file is placed in results folder).

examples/acasxu/acasxu_all.py

@@ -4,32 +4,25 @@
 Stanley Bak, 2020
 '''
 
-import os
 import sys
 import time
 from pathlib import Path
+import subprocess
 
 from termcolor import cprint
 
-from nnenum.settings import Settings
-from acasxu_single import verify_acasxu
-
 def main():
     'main entry point'
 
     start = time.time()
 
-    Settings.TIMING_STATS = False
-    Settings.PARALLEL_ROOT_LP = False
-    Settings.SPLIT_IF_IDLE = False
-    Settings.PRINT_OVERAPPROX_OUTPUT = False
-
     full_filename = 'results/full_acasxu.dat'
     hard_filename = 'results/hard_acasxu.dat'
+    timeout = 600.0
 
     if len(sys.argv) > 1:
-        Settings.TIMEOUT = 60 * float(sys.argv[1])
-        print(f"Running measurements with timeout = {Settings.TIMEOUT} secs")
+        timeout = 60.0 * float(sys.argv[1])
+        print(f"Running measurements with timeout = {timeout} secs")
 
     instances = []
 
@@ -69,39 +62,7 @@ def main():
 
                 cprint(f"\nRunning net {a_prev}-{tau} with spec {spec}", "grey", "on_green")
 
-                if spec == "7":
-                    # ego / 10 processes is beter for deep counterexamples in prop 7
-                    Settings.BRANCH_MODE = Settings.BRANCH_EGO
-                    Settings.NUM_PROCESSES = 10
-
-                    # property 7 is nondeterministic due to work sharing among processes... use median of 10 runs
-                    pretimeout = Settings.TIMEOUT
-                    Settings.TIMEOUT = min(5, pretimeout) # smaller timeout to make it go faster
-                    runs = 10
-                    print(f"\nTrying median of {runs} quick runs")
-                    results = []
-
-                    for i in range(runs):
-                        print(f"\nTrial {i+1}/{runs}:")
-                        res_str, secs = verify_acasxu(net_pair, spec)
-                        results.append((secs, res_str))
-
-                    results.sort()
-                    print(f"results: {results}")
-                    secs, res_str = results[runs // 2] # median
-
-                    print(f"Median: {secs}, {res_str}")
-
-                    Settings.TIMEOUT = pretimeout
-
-                    if res_str == "timeout":
-                        # median was timeout; run full
-                        res_str, secs = verify_acasxu(net_pair, spec)
-                else:
-                    Settings.BRANCH_MODE = Settings.BRANCH_OVERAPPROX
-                    Settings.NUM_PROCESSES = len(os.sched_getaffinity(0))
-
-                    res_str, secs = verify_acasxu(net_pair, spec)
+                res_str, secs = verify_acasxu(net_pair, spec, timeout)
 
                 s = f"{a_prev}_{tau}\t{spec}\t{res_str}\t{secs}"
                 f.write(s + "\n")
@@ -116,5 +77,29 @@ def main():
 
     print(f"Completed all measurements in {round(mins, 2)} minutes")
 
+def verify_acasxu(net_pair, spec, timeout):
+    'returns res_str, secs'
+
+    prev, tau = net_pair
+
+    onnx_path = f'./data/ACASXU_run2a_{prev}_{tau}_batch_2000.onnx'
+    spec_path = f'./data/prop_{spec}.vnnlib'
+
+    args = [sys.executable, '-m', 'nnenum.nnenum', onnx_path, spec_path, f'{timeout}', 'out.txt']
+
+    start = time.perf_counter()
+
+    result = subprocess.run(args, check=False)
+
+    if result.returncode == 0:
+        with open('out.txt', 'r') as f:
+            res_str = f.readline()
+    else:
+        res_str = 'error_exit_code_{result.returncode}'
+
+    diff = time.perf_counter() - start
+
+    return res_str, diff
+
 if __name__ == '__main__':
     main()