nnv-rs

Fast reachability analysis and sampling for deep neural networks

Based loosely on the matlab toolbox of a similar name largely developed by Dr. Hoang-Dung Tran. I'm developing this software for my dissertation and I'm happy to support other work using it. If you're using this package or working on similar problems, please let me know by email at equint at cse dot unl dot <educational ending> (sorry, trying to thwart automated mailers).

Build Python package

1. Install Rust with curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh and re-launch your shell.
2. Create a Python virtualenv and run pip install -r requirements.txt to install Python requirements.
3. Clone the following Rust projects ndarray-linalg, numpy, truncnorm-rs
4. Set the ndarray version in numpy to 15.2.0
5. Ensure CMake 3.15 or higher is installed as well as clang
6. Install OpenBlas (apt-get install libopenblas-dev on Ubuntu)
7. Switch to nightly Rust with rustup default nightly
8. Build and install the Rust-backed Python package with python ./setup.py install

Benchmarking

When benchmarking, if you want to generate a flamegraph, use the following syntax:

cargo bench --bench my_benchmark -- --profile-time 5

To do

1. Implement proper bounds checking with DeepPoly

• Figure out how to run DeepPoly from a star rather than input bounds

2. Implement constellation importance sampling
3. Implement neural network argmax

Troubleshooting

• Build gives linker error /usr/bin/ld: cannot find -lCbcSolver: cbc solver is a default dependency of the good_lp package we're using for linear programming. Fix on Ubuntu is to run sudo apt install coinor-libcbc-dev.
• If your issue isn't listed here, open an issue on GitHub and we'll see if we can fix/add it.

Acknowledgements

This work is not supported by anybody.