Add some instructions/comments for vnncomp 2024

code/nnv/examples/Submission/VNN_COMP2023/README.md

@@ -15,3 +15,25 @@ Provided for the competition. Handles error-handling and set up of MATLAB engine
 Provided for the competition. Executes `nnv` on the test instance.
 
 
+# Preparing for 2024 competition
+
+TODO:
+
+- Choose optimal reachability options for each benchmark.
+
+- Change to the new ONNX import function (will this work from command line so no need to convert models prior to competition?)
+
+- There were some possible errors with counterexamples based on last year report, take a look at this (some already fixed).
+
+- Test the python integration with newest MATLAB version. Can we simplify the code and reduce computation time using the matlab engine for python? (This did not work properly on 2023a)
+
+
+# Instructions to test locally (2023 benchmarks)
+
+1) Ensure NNV is installed and the corresponding toolboxes
+
+2) Go to https://github.com/ChristopherBrix/vnncomp2023_benchmarks, clone the repo and run (in your desired folder) ./setup.sh
+
+3) Change line 4 in `test_some_instances.m` to the folder where you downloaded the benchmarks.
+
+4) Run `test_some_instances.m`. Change the instances tested as desired from the vnncomp_benchmarks repo.

code/nnv/examples/Submission/VNN_COMP2023/convert_scoring_networks.m

@@ -1,12 +1,12 @@
 %% Run some verification instances from the competition
 
 % path to benchmarks
-% vnncomp_path = "/home/manzand/Documents/MATLAB/vnncomp2023_benchmarks/benchmarks/";
-vnncomp_path = "/home/dieman95/Documents/MATLAB/vnncomp2023_benchmarks/benchmarks/";
+vnncomp_path = "/home/manzand/Documents/MATLAB/vnncomp2023_benchmarks/benchmarks/";
+% vnncomp_path = "/home/dieman95/Documents/MATLAB/vnncomp2023_benchmarks/benchmarks/";
 
 % Go through some of the instances for every benchmark
 % It looks like unless the networks are fully fully supported, we get errors...
-% Same problem we ra into when running with no GUI ...
+% Same problem we ran into when running with no GUI ...
 % 
 % Error using matlab.internal.indentcodeLegacy
 %This feature is not supported because:
@@ -39,6 +39,9 @@
 %Error in run_vnncomp2023_instance>load_vnncomp_network (line 127)
 %        net = importONNXNetwork(onnx, "InputDataFormats", "BC", 'OutputDataFormats',"BC"); %reshape
 
+if ~isfolder("networks2023")
+    mkdir("networks2023")
+end
 
 
 %% acasxu
@@ -196,21 +199,21 @@
 
 %% test 
 
-disp("Running test examples...");
-
-test_path = vnncomp_path + "test/";
-
-onnxmodels = ["test_nano.onnx", "test_sat.onnx", "test_small.onnx", "test_tiny.onnx", "test_unsat.onnx"];
-
-for i = 1:length(onnxmodels)
-    if contains(onnxmodels(i), "sat")
-        onnxFile = test_path + onnxmodels(i);
-        net =  importONNXNetwork(onnxFile, "InputDataFormats", "BCSS");
-        name = char(onnxmodels(i));
-        name = name(1:end-5);
-        save(['networks2023/', name], "net", "-v7.3");
-    end
-end
+% disp("Running test examples...");
+% 
+% test_path = vnncomp_path + "test/";
+% 
+% onnxmodels = ["test_nano.onnx", "test_sat.onnx", "test_small.onnx", "test_tiny.onnx", "test_unsat.onnx"];
+% 
+% for i = 1:length(onnxmodels)
+%     if contains(onnxmodels(i), "sat")
+%         onnxFile = test_path + onnxmodels(i);
+%         net =  importONNXNetwork(onnxFile, "InputDataFormats", "BCSS");
+%         name = char(onnxmodels(i));
+%         name = name(1:end-5);
+%         save(['networks2023/', name], "net", "-v7.3");
+%     end
+% end
 
 
 %% yolo
@@ -237,51 +240,51 @@
     % collins_rul: onnx to nnvnet
     % collins_nets = load_collins_NNs;
     if contains(category, 'collins_rul')
-        net = importONNXNetwork(onnx);
+        net = importNetworkFromONNX(onnx);
 
     elseif contains(category, "nn4sys")
         % nn4sys: onnx to matlab:
-        net = importONNXNetowrk(onnx, "OutputDataFormats", "BC"); % lindex
+        net = importNetworkFromONNX(onnx, "OutputDataFormats", "BC"); % lindex
 
     elseif contains(category, "dist_shift")
         % dist_shift: onnx to matlab:
-        net = importONNXNetwork(onnx, "InputDataFormats", "BC", 'OutputDataFormats',"BC"); %reshape
+        net = importNetworkFromONNX(onnx, "InputDataFormats", "BC", 'OutputDataFormats',"BC"); %reshape
 
     elseif contains(category, "cgan")
         % cgan
-        net = importONNXNetwork(onnx,"InputDataFormats", "BC", 'OutputDataFormats',"BC"); %reshape
+        net = importNetworkFromONNX(onnx,"InputDataFormats", "BC", 'OutputDataFormats',"BC"); %reshape
 
     elseif contains(category, "vgg")
         % vgg16: onnx to matlab
-        net = importONNXNetwork(onnx); % flattenlayer
+        net = importNetworkFromONNX(onnx); % flattenlayer
 
     elseif contains(category, "tllverify")
         % tllverify: onnx to matlab
-        net = importONNXNetwork(onnx,"InputDataFormats", "BC", 'OutputDataFormats',"BC");
+        net = importNetworkFromONNX(onnx,"InputDataFormats", "BC", 'OutputDataFormats',"BC");
 
     elseif contains(category, "vit")
         % vit: onnx to matlab
-        net = importONNXNetwork(onnx, "TargetNetwork","dlnetwork" );
+        net = importNetworkFromONNX(onnx );
 
     elseif contains(category, "cctsdb_yolo")
         % cctsdb_yolo: onnx to matnet
-        net = importONNXNetwork(onnx, "TargetNetwork","dlnetwork" );
+        net = importNetworkFromONNX(onnx);
 
     elseif contains(category, "collins_yolo")
         % collins_yolo: onnx to matlab:
-        net = importONNXNetwork(onnx, "TargetNetwork","dlnetwork" );
+        net = importNetworkFromONNX(onnx);
 
     elseif contains(category, "yolo")
         % yolo: onnx to matlab
-        net = importONNXNetwork(onnx); % padlayer
+        net = importNetworkFromONNX(onnx); % padlayer
 
     elseif contains(category, "acasxu")
         % acasxu: onnx to nnv
-        net = importONNXNetwork(onnx, "InputDataFormats","BCSS");
+        net = importNetworkFromONNX(onnx, "InputDataFormats","BCSS");
 
     elseif contains(category, "ml4acopf")
         % ml4acopf: ?
-        net = importONNXNetwork(onnx, "InputDataFormats", "BC");
+        net = importNetworkFromONNX(onnx, "InputDataFormats", "BC");
 
     else % all other benchmarks
         % traffic: onnx to matlab: opset15 issues

code/nnv/examples/Submission/VNN_COMP2023/run_vnncomp2023_instance.m

@@ -3,6 +3,7 @@
 
 t = tic; % start timer
 status = 2; % unknown (to start with)
+locally = true; % change to false for submission
 
 % Process:
 %  1) Load components
@@ -14,15 +15,18 @@
 %% 1) Load components
 
 % Load networks
-% have to go to this path for the networks to load properly... lovely
-old_path = pwd;
-% cd /home/dieman95/Documents/MATLAB/nnv/code/nnv/examples/Submission/VNN_COMP2023/networks2023/;
-cd /home/ubuntu/toolkit/code/nnv/examples/Submission/VNN_COMP2023/networks2023/;
-
-[net, nnvnet, needReshape] = load_vnncomp_network(category, onnx);
+if locally
+    [net, nnvnet, needReshape] = load_vnncomp_network_local(category, onnx);
+else
+    % have to go to this path for the networks to load properly... lovely
+    % old_path = pwd;
+    % cd /home/dieman95/Documents/MATLAB/nnv/code/nnv/examples/Submission/VNN_COMP2023/networks2023/;
+    % cd /home/ubuntu/toolkit/code/nnv/examples/Submission/VNN_COMP2023/networks2023/;
+    [net, nnvnet, needReshape] = load_vnncomp_network(category, onnx);
+    % cd(old_path); % go back to where we ran the functions from
+end
 inputSize = net.Layers(1, 1).InputSize;
 
-cd(old_path); % go back to where we ran the functions from
 
 % Load property to verify
 property = load_vnnlib(vnnlib);
@@ -419,74 +423,88 @@
 
 end
 
-% Had to change this because importer fails using the command line...s
-% function [net,nnvnet] = load_vnncomp_network_local(category, onnx)
-% % load vnncomp 2023 benchmark NNs (subset support)
-% 
-%     % collins_rul: onnx to nnvnet
-%     % collins_nets = load_collins_NNs;
-%     if contains(category, 'collins_rul')
-%         net = importONNXNetwork(onnx);
-%         nnvnet = matlab2nnv(net);
-% 
-%     elseif contains(category, "nn4sys")
-%         % nn4sys: onnx to matlab:
-%         net = importONNXLayers(onnx, "OutputDataFormats", "BC"); % lindex
-%         nnvnet = matlab2nnv(net);
-%         
-%     elseif contains(category, "dist_shift")
-%         % dist_shift: onnx to matlab:
-%         net = importONNXNetwork(onnx, "InputDataFormats", "BC", 'OutputDataFormats',"BC"); %reshape
-%         nnvnet = "";
-%         
-%     elseif contains(category, "cgan")
-%         % cgan
-%         net = importONNXNetwork(onnx,"InputDataFormats", "BC", 'OutputDataFormats',"BC"); %reshape
-%         nnvnet = matlab2nnv(net);
-%         
-%     elseif contains(category, "vgg16")
-%         % vgg16: onnx to matlab
-%         net = importONNXNetwork('vgg16-7.onnx'); % flattenlayer
-%         %reshapedInput = python_reshape(input,net_vgg.Layers(1,1).InputSize); % what is the input? assume it's all the same?
-%         %nnvnet = matlab2nnv(net);
-%         nnvnet = "";
-%         
-%     elseif contains(category, "tllverify")
-%         % tllverify: onnx to matlab
-%         net = importONNXNetwork(onnx,"InputDataFormats", "BC", 'OutputDataFormats',"BC");
-%         nnvnet = matlab2nnv(net);
-%         
-%     elseif contains(category, "vit")
-%         % vit: onnx to matlab
-%         net = importONNXNetwork(onnx, "TargetNetwork","dlnetwork" );
-%         nnvnet = "";
-%         
-%     elseif contains(category, "cctsdb_yolo")
-%         % cctsdb_yolo: onnx to matnet
-%         net = importONNXNetwork(onnx, "TargetNetwork","dlnetwork" );
-%         nnvnet = "";
-%         
-%     elseif contains(category, "collins_yolo")
-%         % collins_yolo: onnx to matlab:
-%         net = importONNXNetwork(onnx, "TargetNetwork","dlnetwork" );
-%         nnvnet = "";
-% 
-%     elseif contains(category, "yolo")
-%         % yolo: onnx to matlab
-%         net = importONNXNetwork(onnx); % padlayer
-%         nnvnet = matlab2nnv(net);
-% 
-%     elseif contains(category, "acasxu")
-%         % acasxu: onnx to nnv
-%         net = importONNXNetwork(onnx, "InputDataFormats","BCSS");
-%         nnvnet = matlab2nnv(net);
-%         
-%     else % all other benchmarks
-%         % traffic: onnx to matlab: opset15 issues
-%         error("ONNX model not supported")
-%     end
-% 
-% end
+% Had to change this because importer fails using the command line...
+function [net,nnvnet,needReshape] = load_vnncomp_network_local(category, onnx)
+% load vnncomp 2023 benchmark NNs (subset support)
+
+    needReshape = 0; % default is to use MATLAB reshape, otherwise use the python reshape
+    % collins_rul: onnx to nnvnet
+    % collins_nets = load_collins_NNs;
+    if contains(category, 'collins_rul')
+        net = importONNXNetwork(onnx);
+        nnvnet = matlab2nnv(net);
+        if contains(onnx, 'full_window_40')
+            needReshape = 2;
+        else
+            needReshape = 1;
+        end
+
+    elseif contains(category, "nn4sys")
+        % nn4sys: onnx to matlab:
+        if contains(onnx, "lindex")
+            net = importONNXLayers(onnx, "OutputDataFormats", "BC"); % lindex
+            nnvnet = matlab2nnv(net);
+            % net = assembleNetwork(net.net);
+            % nnvnet = matlab2nnv(net);
+        else
+            error("We don't have those");
+        end
+
+    elseif contains(category, "dist_shift")
+        % dist_shift: onnx to matlab:
+        net = importONNXNetwork(onnx, "InputDataFormats", "BC", 'OutputDataFormats',"BC"); %reshape
+        nnvnet = "";
+
+    elseif contains(category, "cgan")
+        % cgan
+        net = importONNXNetwork(onnx,"InputDataFormats", "BC", 'OutputDataFormats',"BC"); %reshape
+        nnvnet = matlab2nnv(net);
+
+    elseif contains(category, "vgg16")
+        % vgg16: onnx to matlab
+        net = importONNXNetwork('vgg16-7.onnx'); % flattenlayer
+        %reshapedInput = python_reshape(input,net_vgg.Layers(1,1).InputSize); % what is the input? assume it's all the same?
+        %nnvnet = matlab2nnv(net);
+        nnvnet = "";
+        needReshape = 1;
+
+    elseif contains(category, "tllverify")
+        % tllverify: onnx to matlab
+        net = importONNXNetwork(onnx,"InputDataFormats", "BC", 'OutputDataFormats',"BC");
+        nnvnet = matlab2nnv(net);
+
+    elseif contains(category, "vit")
+        % vit: onnx to matlab
+        net = importONNXNetwork(onnx, "TargetNetwork","dlnetwork" );
+        nnvnet = "";
+        needReshape= 1;
+
+    elseif contains(category, "cctsdb_yolo")
+        % cctsdb_yolo: onnx to matnet
+        net = importONNXNetwork(onnx, "TargetNetwork","dlnetwork" );
+        nnvnet = "";
+
+    elseif contains(category, "collins_yolo")
+        % collins_yolo: onnx to matlab:
+        net = importONNXNetwork(onnx, "TargetNetwork","dlnetwork" );
+        nnvnet = "";
+
+    elseif contains(category, "yolo")
+        % yolo: onnx to matlab
+        net = importONNXNetwork(onnx); % padlayer
+        nnvnet = matlab2nnv(net);
+
+    elseif contains(category, "acasxu")
+        % acasxu: onnx to nnv
+        net = importONNXNetwork(onnx, "InputDataFormats","BCSS");
+        nnvnet = matlab2nnv(net);
+
+    else % all other benchmarks
+        % traffic: onnx to matlab: opset15 issues
+        error("ONNX model not supported")
+    end
+
+end
 
 function xRand = create_random_examples(net, lb, ub, nR, inputSize, needReshape)
     xB = Box(lb, ub); % lb, ub must be vectors

code/nnv/examples/Submission/VNN_COMP2023/test_some_instances.m

@@ -1,8 +1,8 @@
 %% Run some verification instances from the competition
 
 % path to benchmarks
-% vnncomp_path = "/home/manzand/Documents/MATLAB/vnncomp2023_benchmarks/benchmarks/";
-vnncomp_path = "/home/dieman95/Documents/MATLAB/vnncomp2023_benchmarks/benchmarks/";
+vnncomp_path = "/home/manzand/Documents/MATLAB/vnncomp2023_benchmarks/benchmarks/"; % change to whatever local path vnncomp benchmarks are stored
+% vnncomp_path = "/home/dieman95/Documents/MATLAB/vnncomp2023_benchmarks/benchmarks/";
 
 % Go through some of the instances for every benchmark
 % It looks like unless the networks are fully fully supported, we get errors...
@@ -62,6 +62,7 @@
 
 % Run verification for acas 
 for i=1:length(acas_instances)
+    disp(i);
     onnx = acas_path + acas_instances(i,1);
     vnnlib = acas_path + acas_instances(i,2);
     run_vnncomp2023_instance("acasxu",onnx,vnnlib,"acas_results_" + string(i)+".txt");