search

verivital / nnv

Neural Network Verification Software Tool
http://www.verivital.com
111 stars 49 forks source link

Regression issue wrt CAV'23 repeatability and convolutional layer #205

Closed ttj closed 8 months ago

ttj commented 9 months ago

I was trying to rerun the CAV'23 repeatability scripts as set up in codeocean and done for the repeatability then, just given the many changes in the fall, and updated the codeocean capsule syncing to the current latest version head. Some results passed, but I got an error in the middle related to some convolutional layer changes. Can you please check and resolve as needed when you have a chance? It would be great if we add some tests as well... 

+ export PATH=/flowstar/flowstar-2.1.0/:/MATLAB/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
+ PATH=/flowstar/flowstar-2.1.0/:/MATLAB/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
+ pwd
+ cd /deps
/code
+ cd /deps/run_nnv_comparison
+ chmod +x run_tools.sh
+ ls /code
images
LICENSE
nnv
README.md
run
run_codeocean.m
+ echo 'STARTING COMPARISONS'
+ cd /root/
STARTING COMPARISONS
STARTING MATLAB
+ echo 'STARTING MATLAB'
+ matlab -nodisplay -r 'addpath(genpath('\''/deps'\'')); addpath(genpath('\''/code'\'')); startup_nnv; savepath; run_codeocean;'

                            < M A T L A B (R) >
                  Copyright 1984-2022 The MathWorks, Inc.
             R2022b Update 2 (9.13.0.2105380) 64-bit (glnxa64)
                              October 26, 2022

To get started, type doc.
For product information, visit www.mathworks.com.

Adding dependencies to Matlab path...
Toolbox "mpt:3.2.1:all" added to the Matlab path.
Toolbox "mptdoc:3.0.4:all" added to the Matlab path.
Toolbox "lcp:1.0.3:glnxa64" added to the Matlab path.
Toolbox "hysdel:2.0.6:glnxa64" added to the Matlab path.
Toolbox "cddmex:1.0.1:glnxa64" added to the Matlab path.
Toolbox "clpmex:1.0:glnxa64" added to the Matlab path.
Toolbox "glpkmex:1.0:glnxa64" added to the Matlab path.
Toolbox "fourier:1.0:glnxa64" added to the Matlab path.
Toolbox "sedumi:1.3:glnxa64" added to the Matlab path.
Toolbox "yalmip:R20210331:all" added to the Matlab path.

Adding NNV to Matlab path...
[Warning: Invalid file or directory '/code/engine/hyst/lib/Hyst.jar'.] 
[> In javaclasspath>local_validate_dynamic_path (line 271)
In javaclasspath>local_javapath (line 187)
In javaclasspath (line 124)
In javaaddpath (line 71)
In startup_nnv (line 22)] 
Running neural ODE experiments...
Running MNIST experiments...

Read MNIST image data...
Number of images in the dataset:  10000 ...

Read MNIST label data...
Number of labels in the dataset:  10000 ...

Robust images: 5
Unknown images: 0
Not robust images: 0
Total time = 351.3802

Robust images: 5
Unknown images: 0
Not robust images: 0
Total time = 50.2575
Running ACC example...
...compute symbolic Jacobian
...compute symbolic Hessians
dynamics dim 1
dynamics dim 2
dynamics dim 3
dynamics dim 4
dynamics dim 5
dynamics dim 6
dynamics dim 7
dynamics dim 8
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 5
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
Running FPA example...
...compute symbolic Jacobian
...compute symbolic Hessians
dynamics dim 1
dynamics dim 2
dynamics dim 3
dynamics dim 4
dynamics dim 5
Neural ODE experiments finished.
Running NNV vs MATLAB comparison experiments...
Running ACAS Xu experiments...
Starting parallel pool (parpool) using the 'local' profile ...
Connected to the parallel pool (number of workers: 8).
Starting parallel pool (parpool) using the 'local' profile ...
Connected to the parallel pool (number of workers: 8).
IdleTimeout has been reached.
Parallel pool using the 'Processes' profile is shutting down.
Starting parallel pool (parpool) using the 'local' profile ...
Connected to the parallel pool (number of workers: 8).
IdleTimeout has been reached.
Parallel pool using the 'Processes' profile is shutting down.
Starting parallel pool (parpool) using the 'local' profile ...
Connected to the parallel pool (number of workers: 8).
IdleTimeout has been reached.
Parallel pool using the 'Processes' profile is shutting down.
Parallel pool using the 'Processes' profile is shutting down.
Running OVAL21 experiments...
All networks are loaded in 4.3004 seconds
{Error using vl_nnconv
DATA and FILTERS do not have compatible formats.

Error in Conv2DLayer/reach_star_single_input (line 504)
            c = vl_nnconv(input.V(:,:,:,1), obj.Weights, obj.Bias, 'Stride', obj.Stride, 'Pad', obj.PaddingSize, 'Dilate', obj.DilationFactor);

Error in Conv2DLayer/reach_star_multipleInputs (line 602)
                    images(i) = obj.reach_star_single_input(in_images(i));

Error in Conv2DLayer/reach (line 689)
                images = obj.reach_star_multipleInputs(in_images, option);

Error in NN/reach_withConns (line 1228)
                        outSet = obj.Layers{source_indx}.reach(inSet, obj.reachMethod, obj.reachOption, obj.relaxFactor, obj.dis_opt, obj.lp_solver);

Error in NN/reach (line 245)
                outputSet = obj.reach_withConns(inputSet);

Error in verify_oval21_nnv (line 11)
    R = nn.reach(IS, reachOpt);

Error in verifyAll (line 28)
        [res(i,1), res(i,2)] = verify_oval21_nnv(net, propertyFile, reachOpt1);

Error in run_cav23 (line 33)
    verifyAll;

Error in run_codeocean (line 19)
run_cav23
}
mldiego commented 9 months ago

Addressed this error on #207.

Please let me know if you run it again and encounter any other errors on CodeOcean. I'll keep this open for now.

ttj commented 8 months ago

I (finally) updated the codeocean to the latest and have some new errors:

+ export PATH=/flowstar/flowstar-2.1.0/:/MATLAB/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
+ PATH=/flowstar/flowstar-2.1.0/:/MATLAB/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
+ pwd
+ cd /deps
/code
+ cd /deps/run_nnv_comparison
+ chmod +x run_tools.sh
+ ls /code
images
LICENSE
nnv
README.md
run
run_codeocean.m
+ echo 'STARTING COMPARISONS'
+ cd /root/
+ echo 'STARTING MATLAB'
STARTING COMPARISONS
STARTING MATLAB
+ matlab -nodisplay -r 'addpath(genpath('\''/deps'\'')); addpath(genpath('\''/code'\'')); startup_nnv; savepath; run_codeocean;'

                            < M A T L A B (R) >
                  Copyright 1984-2022 The MathWorks, Inc.
             R2022b Update 2 (9.13.0.2105380) 64-bit (glnxa64)
                              October 26, 2022

To get started, type doc.
For product information, visit www.mathworks.com.

Adding dependencies to Matlab path...
Toolbox "mpt:3.2.1:all" added to the Matlab path.
Toolbox "mptdoc:3.0.4:all" added to the Matlab path.
Toolbox "lcp:1.0.3:glnxa64" added to the Matlab path.
Toolbox "hysdel:2.0.6:glnxa64" added to the Matlab path.
Toolbox "cddmex:1.0.1:glnxa64" added to the Matlab path.
Toolbox "clpmex:1.0:glnxa64" added to the Matlab path.
Toolbox "glpkmex:1.0:glnxa64" added to the Matlab path.
Toolbox "fourier:1.0:glnxa64" added to the Matlab path.
Toolbox "sedumi:1.3:glnxa64" added to the Matlab path.
Toolbox "yalmip:R20210331:all" added to the Matlab path.

Adding NNV to Matlab path...
[Warning: Invalid file or directory '/code/engine/hyst/lib/Hyst.jar'.] 
[> In javaclasspath>local_validate_dynamic_path (line 271)
In javaclasspath>local_javapath (line 187)
In javaclasspath (line 124)
In javaaddpath (line 71)
In startup_nnv (line 22)] 
Running neural ODE experiments...
Running MNIST experiments...

Read MNIST image data...
Number of images in the dataset:  10000 ...

Read MNIST label data...
Number of labels in the dataset:  10000 ...

Robust images: 5
Unknown images: 0
Not robust images: 0
Total time = 507.6229

Robust images: 5
Unknown images: 0
Not robust images: 0
Total time = 56.5751
Running ACC example...
...compute symbolic Jacobian
...compute symbolic Hessians
dynamics dim 1
dynamics dim 2
dynamics dim 3
dynamics dim 4
dynamics dim 5
dynamics dim 6
dynamics dim 7
dynamics dim 8
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 5
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
Running FPA example...
...compute symbolic Jacobian
...compute symbolic Hessians
dynamics dim 1
dynamics dim 2
dynamics dim 3
dynamics dim 4
dynamics dim 5
Neural ODE experiments finished.
Running NNV vs MATLAB comparison experiments...
Running ACAS Xu experiments...
Starting parallel pool (parpool) using the 'local' profile ...
Connected to the parallel pool (number of workers: 8).
Parallel pool using the 'Processes' profile is shutting down.
Running OVAL21 experiments...
All networks are loaded in 4.3678 seconds
Running RL Benchmarks experiments...
All networks are loaded in 0.40113 seconds
Running TLLverify experiments...
NNV vs MATLAB comparison is finished.
Running Semantic Segmentation examples...
{Error using load
Unable to find file or directory 'data/M2NIST/m2nist_6484_test_images.mat'.

Error in example_dilated (line 9)
    images = load('data/M2NIST/m2nist_6484_test_images.mat');

Error in run_cav23 (line 57)
    example_dilated;

Error in run_codeocean (line 19)
run_cav23
}
mldiego commented 8 months ago

This error was fixed on pull request #210

ttj commented 7 months ago

Thanks! That resolved that issue and most ran successfully. One near the end failed as below, looks like in the RNN things

Also, I did have to update the cora submodule (so needed to rebuild the docker in codeocean), just for reference (by default it is cached, but rebuilt successfully today, so that is good).

Run environment setup complete, running code...

/code
+ export PATH=/flowstar/flowstar-2.1.0/:/MATLAB/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
+ PATH=/flowstar/flowstar-2.1.0/:/MATLAB/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
+ pwd
+ cd /deps
+ cd /deps/run_nnv_comparison
+ chmod +x run_tools.sh
+ ls /code
images
LICENSE
nnv
README.md
run
run_codeocean.m
+ echo 'STARTING COMPARISONS'
+ cd /root/
+ echo 'STARTING MATLAB'
STARTING COMPARISONS
STARTING MATLAB
+ matlab -nodisplay -r 'addpath(genpath('\''/deps'\'')); addpath(genpath('\''/code'\'')); startup_nnv; savepath; run_codeocean;'

                            < M A T L A B (R) >
                  Copyright 1984-2022 The MathWorks, Inc.
             R2022b Update 2 (9.13.0.2105380) 64-bit (glnxa64)
                              October 26, 2022

To get started, type doc.
For product information, visit www.mathworks.com.

Adding dependencies to Matlab path...
Toolbox "mpt:3.2.1:all" added to the Matlab path.
Toolbox "mptdoc:3.0.4:all" added to the Matlab path.
Toolbox "lcp:1.0.3:glnxa64" added to the Matlab path.
Toolbox "hysdel:2.0.6:glnxa64" added to the Matlab path.
Toolbox "cddmex:1.0.1:glnxa64" added to the Matlab path.
Toolbox "clpmex:1.0:glnxa64" added to the Matlab path.
Toolbox "glpkmex:1.0:glnxa64" added to the Matlab path.
Toolbox "fourier:1.0:glnxa64" added to the Matlab path.
Toolbox "sedumi:1.3:glnxa64" added to the Matlab path.
Toolbox "yalmip:R20230609:all" added to the Matlab path.

Adding NNV to Matlab path...
Warning: Invalid file or directory '/code/engine/hyst/lib/Hyst.jar'. 
> In javaclasspath>local_validate_dynamic_path (line 271)
In javaclasspath>local_javapath (line 187)
In javaclasspath (line 124)
In javaaddpath (line 71)
In startup_nnv (line 22) 
Running neural ODE experiments...
Running MNIST experiments...

Read MNIST image data...
Number of images in the dataset:  10000 ...

Read MNIST label data...
Number of labels in the dataset:  10000 ...

Robust images: 5
Unknown images: 0
Not robust images: 0
Total time = 298.0189

Robust images: 5
Unknown images: 0
Not robust images: 0
Total time = 43.1944
Running ACC example...
Computing multivariate derivatives for dynamic 'tanh_plant':
  .. compute symbolic Jacobian
  .. compute symbolic Jacobian (output)
  .. compute symbolic Hessians
     .. dynamics dim 1
     .. dynamics dim 2
     .. dynamics dim 3
     .. dynamics dim 4
     .. dynamics dim 5
     .. dynamics dim 6
     .. dynamics dim 7
     .. dynamics dim 8
Done.
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 2
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 3
split! ...number of parallel sets: 4
split! ...number of parallel sets: 4
split! ...number of parallel sets: 4
split! ...number of parallel sets: 4
split! ...number of parallel sets: 4
split! ...number of parallel sets: 5
split! ...number of parallel sets: 4
split! ...number of parallel sets: 4
split! ...number of parallel sets: 4
Running FPA example...
Computing multivariate derivatives for dynamic 'CTRNN_FPA':
  .. compute symbolic Jacobian
  .. compute symbolic Jacobian (output)
  .. compute symbolic Hessians
     .. dynamics dim 1
     .. dynamics dim 2
     .. dynamics dim 3
     .. dynamics dim 4
     .. dynamics dim 5
Done.
Neural ODE experiments finished.
Running NNV vs MATLAB comparison experiments...
Running ACAS Xu experiments...
Starting parallel pool (parpool) using the 'local' profile ...
Connected to the parallel pool (number of workers: 8).
Parallel pool using the 'Processes' profile is shutting down.
Running OVAL21 experiments...
All networks are loaded in 1.9608 seconds
Running RL Benchmarks experiments...
All networks are loaded in 0.38536 seconds
Running TLLverify experiments...
NNV vs MATLAB comparison is finished.
Running Semantic Segmentation examples...
Semantic Segmentation examples are finished.
Running RNNs experiments...
Running RNN N_2_0 analysis...
Error using FullyConnectedLayer/evaluate
Inconsistent input vector

Error in NN/evaluate_noConns (line 1090)
                y = obj.Layers{i}.evaluate(y);

Error in NN/evaluate (line 133)
                y = obj.evaluate_noConns(x);

Error in verify_N2_0 (line 56)
            y = net.evaluate(input_points);

Error in run_rnn_all (line 6)
    verify_N2_0;

Error in run_cav23 (line 68)
    run_rnn_all();

Error in run_codeocean (line 19)
run_cav23