-
src/
: source code -
benchmark/
: benchmarks for experiment -
results/
: experimental results -
env.yaml
: required packages
- Anaconda or Miniconda
- Gurobi: Gurobi requires a license (a free academic license is available).
-
Make sure you have
Anaconda
/Miniconda
andGurobi
properly installed. -
Remove pre-installed environment
conda deactivate
conda env remove --name veristable
- Install required packages
conda env create -f env.yaml
- Activate
conda
environment
conda activate veristable
- Minimal command
python3 main.py --net ONNX_PATH --spec VNNLIB_PATH
- More options
python3 main.py --net ONNX_PATH --spec VNNLIB_PATH
[--beam_candidate BEAM_CANDIDATE] [--stabilize_candidate STABILIZE_CANDIDATE]
[--timeout TIMEOUT] [--device {cpu,cuda}]
[--result_file RESULT_FILE] [--export_cex]
[--disable_restart] [--disable_stabilize]
[--verbosity {0,1,2}] [--test]
Use -h
or --help
to see options that can be passed into VeriStable.
--net
: load pretrained ONNX model from this specified path.--spec
: path to VNNLIB specification file.--beam_candidate
: DPLL(T) search parallelism factor (n
)--stabilize_candidate
: stabilization parallelism factor (k
)--timeout
: timeout in seconds--device
: device to use (eithercpu
orcuda
).--verbosity
: logging options (0: NOTSET, 1: INFO, 2: DEBUG).--result_file
: file to save execution results.--export_cex
: enable writing counter-example toresult_file
.--disable_restart
: disable RESTART heuristic.--disable_stabilize
: disable STABILIZE.--test
: test on small example with special settings.
- Unit test
python3 test.py
- Examples showing VeriStable verifies properties (i.e., UNSAT results):
python3 main.py --net "example/mnistfc-medium-net-554.onnx" --spec "example/test.vnnlib"
# unsat,29.7011
python3 main.py --net "example/cifar10_2_255_simplified.onnx" --spec "example/cifar10_spec_idx_4_eps_0.00784_n1.vnnlib"
# unsat,20.0496
python3 main.py --net "example/ACASXU_run2a_1_1_batch_2000.onnx" --spec "example/prop_6.vnnlib"
# unsat,4.3972
- Examples showing VeriStable disproves properties (i.e., SAT results):
python3 main.py --net "example/ACASXU_run2a_1_9_batch_2000.onnx" --spec "example/prop_7.vnnlib"
# sat,4.2924
python3 main.py --net "example/mnist-net_256x2.onnx" --spec "example/prop_1_0.05.vnnlib"
# sat,1.4306