Mark Müller

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...

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...

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=ca42b4afd1ff8cb92ebde5303fcce0db26357b49 SCRIPTS_DIR=vnncomp_scripts ``` Edit: ERAN should...

@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...

While everything @huanzhang12 said is true the ERAN install script was based on the vanilla python environment and as this might be updated between when I tested things and when...

@stanleybak I agree with @pat676 comments that proving robustness against all other classes seems to be a practically more relevant use-case and allows tools that can reuse intermediate results to...

@stanleybak I see this does indeed depend on whether we view the specification as the to be verified property (prove it holds for all permissible inputs) or as a description...

I would like to propose the following benchmark: 1) A ReLU FFN with 8 hidden layers of 200 neurons each for MNIST, that was normally trained with eps=0.015. 36 samples...

@stanleybak Thank you for organizing the competition and drafting the competition rules! I have a few suggestions/requests for clarification: 1.) **Runtime caps**: In the current draft it seems like the...

@stanleybak Thank you for taking up the suggestions I made. Regarding the choice of samples as a block vs fully random: I suggested using blocks of samples (perhaps randomly chose...