tcwangshiqi-columbia / reluval Goto Github PK

If I change check_max_constant in split.c to use a threshold of -0.02 instead of 0.5011, I get a segfault during verification.

I am trying to test a neural network that has different sized hidden layers, but I am getting a segfault. After some debugging, it looks like the indices used for the weight matrices in backward_prop are wrong. See here. We can see that, along with line 1002, i and j will loop until the maxLayerSize, but if the weight matrices have smaller dimensions, then we'll have a segFault at line 1004. So this doesn't seem to be any issue for the example networks where the weight matrices are all maxLayerSize by maxLayerSize, but for non-uniform hidden layer networks, it causes a problem. I am having trouble fixing this issue on my own and would appreciate some help.

i don't understand what the "target" means in nnet.c.

when I make, I find Compilation Error. but I don't change the code.
/usr/bin/ld: split.o:(.bss+0x0): multiple definition of lock'; network_test.o:(.bss+0x0): first defined here
collect2: error: ld returned 1 exit status
make: *** [makefile:15: network_test] Error 1`

In nnet.c

if (PROPERTY==16) {
        float upper[] = {62000,-0.7,-3.141592+0.005,200,1200};
        float lower[] = {12000,-3.141592,-3.141592,100,0};
        memcpy(u, upper, sizeof(float)*inputSize);
        memcpy(l, lower, sizeof(float)*inputSize);
    }

    if (PROPERTY==26) {
        float upper[] = {62000,3.141592,-3.141592+0.005,200,1200};
        float lower[] = {12000,0.7,-3.141592,100,0};
        memcpy(u, upper, sizeof(float)*inputSize);
        memcpy(l, lower, sizeof(float)*inputSize);
    }

The upper and lower bounds of the 4th input variable (v_own) are specified 100 <= v_own <= 200, but in the Reluplex paper it's 100 <= v_own <= 1200.
Is this an intended change or a typo?