From e880a3ff44536fa06eae8de9e05c9417804ad9bb Mon Sep 17 00:00:00 2001 From: Diego Manzanas Date: Fri, 29 Mar 2024 16:43:58 -0500 Subject: [PATCH 1/3] Added some comments and instructions for vnncomp --- .../Submission/VNN_COMP2023/README.md | 23 +++ .../VNN_COMP2023/convert_scoring_networks.m | 63 +++---- .../VNN_COMP2023/run_vnncomp2023_instance.m | 168 ++++++++++-------- .../VNN_COMP2023/test_some_instances.m | 5 +- 4 files changed, 152 insertions(+), 107 deletions(-) diff --git a/code/nnv/examples/Submission/VNN_COMP2023/README.md b/code/nnv/examples/Submission/VNN_COMP2023/README.md index 0cb9c6faa1..cf2717ac3b 100644 --- a/code/nnv/examples/Submission/VNN_COMP2023/README.md +++ b/code/nnv/examples/Submission/VNN_COMP2023/README.md @@ -15,3 +15,26 @@ 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. + + +3) \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2023/convert_scoring_networks.m b/code/nnv/examples/Submission/VNN_COMP2023/convert_scoring_networks.m index 54d03d219e..165159d751 100644 --- a/code/nnv/examples/Submission/VNN_COMP2023/convert_scoring_networks.m +++ b/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 diff --git a/code/nnv/examples/Submission/VNN_COMP2023/run_vnncomp2023_instance.m b/code/nnv/examples/Submission/VNN_COMP2023/run_vnncomp2023_instance.m index 3e0cb8ab8f..f9ab7593b8 100644 --- a/code/nnv/examples/Submission/VNN_COMP2023/run_vnncomp2023_instance.m +++ b/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 diff --git a/code/nnv/examples/Submission/VNN_COMP2023/test_some_instances.m b/code/nnv/examples/Submission/VNN_COMP2023/test_some_instances.m index 8ffba64f4d..e54b5bebf1 100644 --- a/code/nnv/examples/Submission/VNN_COMP2023/test_some_instances.m +++ b/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"); From 247ecfc697879b7f5808f238c99a86093e6e26e9 Mon Sep 17 00:00:00 2001 From: Diego Manzanas Lopez Date: Fri, 29 Mar 2024 16:46:42 -0500 Subject: [PATCH 2/3] Update README.md --- code/nnv/examples/Submission/VNN_COMP2023/README.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/code/nnv/examples/Submission/VNN_COMP2023/README.md b/code/nnv/examples/Submission/VNN_COMP2023/README.md index cf2717ac3b..d3a2824698 100644 --- a/code/nnv/examples/Submission/VNN_COMP2023/README.md +++ b/code/nnv/examples/Submission/VNN_COMP2023/README.md @@ -36,5 +36,3 @@ TODO: 3) Change line 4 in 'test_some_instances.m' to the folder where you downloaded the benchmarks. - -3) \ No newline at end of file From c6d8d5ce3f369ef21a6e75e8846ff18b2ff68de5 Mon Sep 17 00:00:00 2001 From: Diego Manzanas Lopez Date: Fri, 29 Mar 2024 16:48:19 -0500 Subject: [PATCH 3/3] Update README.md --- code/nnv/examples/Submission/VNN_COMP2023/README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/code/nnv/examples/Submission/VNN_COMP2023/README.md b/code/nnv/examples/Submission/VNN_COMP2023/README.md index d3a2824698..e55f9df1e6 100644 --- a/code/nnv/examples/Submission/VNN_COMP2023/README.md +++ b/code/nnv/examples/Submission/VNN_COMP2023/README.md @@ -34,5 +34,6 @@ TODO: 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. +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.