NARv

NARv, short for Network Abstraction-Refinement for verification, is a neural network verification tool based on structure-oriented CEGAR (counterexample-guided abstraction refinement). The technique details can be found in [1] and it is inspired by [2].

Dependencies

Marabou (checked compatibility with commit 30b23b9)

• Build both Marabou and Maraboupy:

cd /path/to/marabou/folder
mkdir build && cd build
cmake .. -DBUILD_PYTHON=ON
cmake --build .

• Export maraboupy folder to Python path:

PYTHONPATH=PYTHONPATH:/path/to/marabou/folder

Getting Started

You can try an example in the tests/ folder:

sh test_example.sh

File Tree

|--core/ 
|--experiments/
|--planet/
|--tests/
|--narv.py
|--README.md

• Folder core/: the main code of NARv.
• Folder experiments/: the benchmarks and the experimental data for the TOSEM submission.
• Folder planet/: the code of the tool Planet from its repository.
• Folder tests/: some testing scripts for NARv.

References

1. Jiaxiang Liu, Yunhan Xing, Xiaomu Shi, Fu Song, Zhiwu Xu, Zhong Ming: Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks. CoRR abs/2207.00759 (2022)

2. Yizhak Yisrael Elboher, Justin Gottschlich, Guy Katz: An Abstraction-Based Framework for Neural Network Verification. CAV (1) 2020: 43-65