Tool submission

[stanleybak]

The tool testing and submission instructions are in this document.

Please post your tool information according to the instructions in this topic.

[stanleybak]

This is the entry for the nnenum tool. The tool is available using git:

TOOL_NAME=nnenum
REPO=https://github.com/stanleybak/nnenum.git 
COMMIT=c93a39cb568f58a26015bd151acafab34d2d4929
SCRIPTS_DIR=vnncomp_scripts

[mnmueller]

Regarding the tool (and benchmark) submission deadline. I would like to propose to either strictly enforce both or give all participants one week from the last update to any benchmark to submit their tool (i.e., move that deadline) such that all other participants can check that their tools behaves as expected on all other benchmarks and potentially fix any problems coming up.

[stanleybak]

I think your second option may be more realistic. Maybe we'll have a cutoff for scored benchmarks... if people submit something late and we still want to do them, them they won't be part of the scoring. How does that sound?

[mnmueller]

I have no problem with either suggestion. While it would be great to be able to score all benchmarks, moving the deadline will obviously leave you (and the rest of the organizing team) with a tighter schedule, so I think this decision should be yours.
If we go with excluding some benchmarks from the scoring, it would still be great to be able to test the final (example) benchmarks/networks before we have to submit our tools.

[pat676]

@stanleybak, we intend to compete with a toolkit that hasn't been published yet; how should we proceed with this? We can share it via a Dropbox folder if that's okay with you?

We also have a dependency on the Xpress solver, they have free academic licenses or we could provide the license file (this is all described in our readme). If we are to provide the license file, we need a host-id from the AWS instance; this host-id changes every time the instance is stopped.

[Neelanjana314]

@stanleybak Should we have one result file for each instance run(i.e one onnx-vnnlib pair)? Or its a single result (.txt) file containing all the instances run?

Also, as per my understanding there will be 3 categories: mnist, cifar10 and acasxu. In that case, if I want to skip a particular benchmark under any these categories, how should I mention that? Or the Categories will be the benchmark names?

[Wei-TianHao]

This is the entry for the NeuralVerification.jl tool. The tool is available using git: Passed docker test.

TOOL_NAME=NeuralVerification.jl
REPO=https://github.com/intelligent-control-lab/NeuralVerification.jl.git
COMMIT=4e612602ba4b34b42416742d85476d9b0dcdcb51
SCRIPTS_DIR=vnncomp_scripts

[pat676]

@stanleybak, we have emailed you instructions on how to obtain the VeriNet toolkit. Please let us know if you need a different submission format.

[stanleybak]

@pat676 got it. We'll let you know if there are issues with the licensing.

@Neelanjana314 one result for each instance run. The run_instance.sh script gets passed in a single onnx path and a single vnnlib path, your tool should run on that single instance and then output the result. Our competition scripts will aggregate results.

[alessandrodepalma]

This is the submission for the oval framework:

TOOL_NAME=oval
REPO=https://github.com/oval-group/oval-bab.git 
COMMIT=0f39b4d685927c56f9e2c12307cc3d2b19be8bd6
SCRIPTS_DIR=vnncomp_scripts

[mnmueller]

This is the submission for the ERAN framework:
A gurobi license has to be acquired manually as detailed in the readme.

TOOL_NAME=ERAN
REPO=https://github.com/mnmueller/eran_vnncomp2021.git
COMMIT=<updated later in the topic>ca42b4afd1ff8cb92ebde5303fcce0db26357b49
SCRIPTS_DIR=vnncomp_scripts

Edit: ERAN should be run on a GPU instance

[stanleybak]

@mnmueller great thanks. Were you able to test if / how to get Gurobi working on AWS?

[mnmueller]

@stanleybak Yes. If you follow the README.md or uncomment the following block in install_tool_user.sh and copy a license key into the "###" block everything should work correctly.

#cd bin
#./grbgetkey #################### < ../../
#cd ../../../

[dlshriver]

The submission for DNNF:

TOOL_NAME=DNNF
REPO=https://github.com/dlshriver/DNNF.git 
COMMIT=e2dafcc0017bdd555a777e8f6ae96d0af5813bfb
SCRIPTS_DIR=scripts/vnncomp

The README for the tool submission is here: https://github.com/dlshriver/DNNF/blob/e2dafcc0017bdd555a777e8f6ae96d0af5813bfb/scripts/vnncomp/README.md

[ChristopherBrix]

For Debona:

TOOL_NAME=Debona
REPO=https://github.com/ChristopherBrix/Debona
COMMIT=792575d18bb5f83cb8699dda6b9097dc41438e3d
SCRIPTS_DIR=Debona

https://github.com/ChristopherBrix/Debona

Thank you for organizing this competition!