How can we run ACAS benchmarks in Neurify?

[ericksonalves]

I have tried to run ACAS benchmarks from ReluVal in Neurify code, but it closes unexpectedly.

[ChristopherBrix]

I'm not the author of Neurify, but I've been working on bugfixes and improvements for the last few months. So far, I always focused on MNIST, so I'm not sure what's the problem with ACAS. Could you run it with valgrind and post any error messages you get? Also, please monitor the memory consumption using htop to make sure it's not hitting any limits there. In the best case, this bug is related to something I already fixed for MNIST, so I can point you to the relevant changes.

However, @tcwangshiqi-columbia may be able to give more concrete help.

[ericksonalves]

Hi @ChristopherBrix ,

Thank you for the update. I will try to do that and let you know the results.

[shchae7]

Hi @ericksonalves , I'm also trying to run the ACAS Xu from ReluVal using Neurify, but having some difficulties. (I'm trying to modify the codes in general dir)

from general/network_test.c line 107 ~

else if(PROPERTY==1){
        /*
         * Customize your own property you want to verify
         * For instance, you can check whether the first ouput is
         * always the smallest or the second output is always
         * less than 0.01
         * For each property, you need to change (1) the dataset
         * that you want to load in nnet.c; (2) the check_function
         * and check_function1 in split.c.
         */
    }

it looks like to fit the scripts provided in the ReluVal repo, we have to add in the properties manually. But I'm a bit lost on the correlation btw the image_length, image_start, INF variable that we have to initialize, and what happens in the network_test.c of ReluVal.

Has there been any progress and if so could you share us the results?