diff --git a/code/nnv/engine/nn/layers/ElementwiseAffineLayer.m b/code/nnv/engine/nn/layers/ElementwiseAffineLayer.m index 4e83b8c82..ff0f43853 100644 --- a/code/nnv/engine/nn/layers/ElementwiseAffineLayer.m +++ b/code/nnv/engine/nn/layers/ElementwiseAffineLayer.m @@ -137,7 +137,7 @@ end % Offset (bias) if obj.DoOffset - image = image.affineMap(diag(ones(1,a.dim)), obj.Offset); % x + b + image = image.affineMap(diag(ones(1,image.dim)), obj.Offset); % x + b end end @@ -150,7 +150,15 @@ % @S: output ImageStar n = length(inputs); - S(n) = ImageStar; + + % Initialize output variables + if isa(inputs, "ImageStar") + S(n) = ImageStar; + else + S(n) = Star; + end + + % Begin computing reachability one set at a time if strcmp(option, 'parallel') parfor i=1:n S(i) = obj.reach_star_single_input(inputs(i)); diff --git a/code/nnv/engine/set/Star.m b/code/nnv/engine/set/Star.m index 1cf2d300b..19e09bf9c 100644 --- a/code/nnv/engine/set/Star.m +++ b/code/nnv/engine/set/Star.m @@ -535,8 +535,13 @@ if ~isempty(obj.state_lb) && ~isempty(obj.state_ub) B = Box(obj.state_lb, obj.state_ub); + else + if isa(obj.V, 'single') || isa(obj.C, 'single') || isa(obj.d, 'single') + obj = obj.changeVarsPrecision('double'); + end + lb = zeros(obj.dim, 1); ub = zeros(obj.dim, 1); diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/ACC/acc.mat b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/ACC/acc.mat new file mode 100644 index 000000000..09d5f1e3a Binary files /dev/null and b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/ACC/acc.mat differ diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/ACC/acc.pdf b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/ACC/acc.pdf new file mode 100644 index 000000000..29f007c8b Binary files /dev/null and b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/ACC/acc.pdf differ diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/ACC/reach.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/ACC/reach.m index 31bdaefb4..f7026b549 100644 --- a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/ACC/reach.m +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/ACC/reach.m @@ -4,7 +4,7 @@ % Load components net = load_NN_from_mat('controller_5_20.mat'); -reachStep = 0.02; +reachStep = 0.05; controlPeriod = 0.1; output_mat = [0 0 0 0 1 0;1 0 0 -1 0 0; 0 1 0 0 -1 0]; % feedback: relative distance, relative velocity and ego-car velocity plant = NonLinearODE(6,1,@dynamicsACC, reachStep, controlPeriod, output_mat); @@ -34,7 +34,6 @@ reachPRM.numCores = 1; reachPRM.reachMethod = 'approx-star'; [R,rT] = nncs.reach(reachPRM); -% disp("Time to compute ACC reach sets: " +string(rT)); % Save results if is_codeocean diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Airplane/reach.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Airplane/reach.m index 89f057b61..44be76ad5 100644 --- a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Airplane/reach.m +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/Airplane/reach.m @@ -14,19 +14,19 @@ % define the plant as specified by nnv plant = NonLinearODE(12,6,@dynamics, reachStep, controlPeriod, eye(12)); % Set plant reachability options - plant.set_taylorTerms(20) + plant.set_taylorTerms(2) plant.set_zonotopeOrder(10); %% Reachability analysis % Initial set (smaller partition to falsify property) - lb = [0; 0; 0; 0; 0.8; 0; 0; 0; 0; 0; 0; 0]; - ub = [0; 0; 0; 0; 0.81; 0; 0; 0; 0; 0; 0; 0]; + lb = [0; 0; 0; 1; 1; 1; 0.99; 0; 0; 0; 0; 0]; + ub = [0; 0; 0; 1; 1; 1; 1; 0; 0; 0; 0; 0]; init_set = Star(lb,ub); % Store all reachable sets reachAll = init_set; % Execute reachabilty analysis - num_steps = 8; + num_steps = 20; reachOptions.reachMethod = 'approx-star'; t = tic; for i=1:num_steps @@ -51,10 +51,10 @@ f2 = figure; rectangle('Position',[-1,-1,2,2],'FaceColor',[0 0.5 0 0.5],'EdgeColor','y', 'LineWidth',0.1) hold on; - Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,2,5,'b'); + Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,2,7,'b'); grid; xlabel('x_2'); - ylabel('x_5'); + ylabel('x_7'); f5 = figure; rectangle('Position',[-1,-1,2,2],'FaceColor',[0 0.5 0 0.5],'EdgeColor','y', 'LineWidth',0.1) @@ -66,10 +66,10 @@ % Save figure if is_codeocean - exportgraphics(f2,'/results/logs/airplane_2v5.pdf', 'ContentType', 'vector'); + exportgraphics(f2,'/results/logs/airplane_2v7.pdf', 'ContentType', 'vector'); exportgraphics(f5,'/results/logs/airplane_8v9.pdf', 'ContentType', 'vector'); else - exportgraphics(f2,'airplane_3v4.pdf','ContentType', 'vector'); + exportgraphics(f2,'airplane_2v7.pdf','ContentType', 'vector'); exportgraphics(f5,'airplane_8v9.pdf', 'ContentType', 'vector'); end diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/README.md b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/README.md new file mode 100755 index 000000000..6e877a56b --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/README.md @@ -0,0 +1,11 @@ +# Proposed ARCH Benchmark - CartPole + +This benchmark is proposed for the ARCH Friendly Competition 2024. + +## Benchmark + +We consider a pendulum (pole) mounted on a movable cart (= CartPole). The cart can be moved by a controller. The carts postition x1, its velocity x2, the angle of the pole x3 (with 0, 2*pi being the upright postion) and its angular velocity x4 define the state vector of the 4-dimensional system. The system starts in a middle postition of the cart, with the pendulum in the upright position. The controllers goal is to counteract slight deviations in the starting values and balance the pendulum in the middle of the track. + +## Specifications and Dynamics + +The system dynamics can be found in ```dynamics.m```. The safe states are defined as a stable upright position, which has to be reached after 8 seconds and has to be hold for at least 2 seconds. The controllers step size is 0.02 seconds. diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/dynamics.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/dynamics.m new file mode 100755 index 000000000..192a78fab --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/dynamics.m @@ -0,0 +1,12 @@ +function dx = dynamics(x, f) + +% Cartpole Swingup, 4 states x and the input f (action of the controller) +% The controller takes (x(1), x(2), x(3), x(4)) as input, its output can +% be used directly. + +dx(1,1) = x(2); +dx(2,1) = 2*f; +dx(3,1) = x(4); +dx(4,1) = (0.08*0.41*(9.8*sin(x(3))-2*f*cos(x(3)))-0.0021*x(4))/0.0105; + +end \ No newline at end of file diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/model.onnx b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/model.onnx new file mode 100755 index 000000000..c837ab82a Binary files /dev/null and b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/model.onnx differ diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/reach.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/reach.m new file mode 100644 index 000000000..f89c5c7fb --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/reach.m @@ -0,0 +1,66 @@ +% function t = reach() + + %% Reachability analysis of Cartpole Benchmark + + %% Load Components + + % Load the controller + net = importNetworkFromONNX('model.onnx', "InputDataFormats", "BC"); + net = matlab2nnv(net); + % Load plant + reachStep = 0.002; + controlPeriod = 0.02; + plant = NonLinearODE(4,1,@dynamics, reachStep, controlPeriod, eye(4)); + plant.set_tensorOrder(2); + + + %% Reachability analysis + + % Initial set + lb = [-0.1; -0.05; -0.1; -0.05]; + ub = [0.1; 0.05; 0.1; 0.05]; + InitialSet = Box(lb,ub); + init_sets = InitialSet.partition([1,2,3,4],[20,10,20,10]); + for k=1:length(init_sets) + init_set = init_sets(k); + init_set = init_set.toStar; + % Store all reachable sets + reachAll = init_set; + num_steps = 500; + reachOptions.reachMethod = 'approx-star'; + t = tic; + for i=1:num_steps + disp(i); + % Compute controller output set + input_set = net.reach(init_set,reachOptions); + % Compute plant reachable set + init_set = plant.stepReachStar(init_set, input_set,'lin'); + reachAll = [reachAll init_set]; + toc(t); + end + t = toc(t); + end + + %% Visualize results + plant.get_interval_sets; + + f = figure; + hold on; + % rectangle('Position',[0.5,1,1,1],'FaceColor',[1 0 0 0.5],'EdgeColor','r', 'LineWidth',0.1) + Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,1,2,'b'); + Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,3,4,'r'); + % Plot only falsifying trace +% plot(squeeze(sims(3,k,:)), squeeze(sims(1,k,:)), 'Color', [0 0 1 1]); + grid; + % xlabel('Time (s)'); + % ylabel('\theta'); + % xlim([0 0.6]) + % ylim([0.95 1.25]) + % Save figure + % if is_codeocean + % exportgraphics(f,'/results/logs/cartpole.pdf', 'ContentType', 'vector'); + % else + % exportgraphics(f,'cartpole.pdf','ContentType', 'vector'); + % end + +% end \ No newline at end of file diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/specifications.txt b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/specifications.txt new file mode 100755 index 000000000..6af3a8d86 --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/CartPole/specifications.txt @@ -0,0 +1,14 @@ +Initial states: + +x1 = [-0.1, 0.1] +x2 = [-0.05, 0.05] +x3 = [-0.1, 0.1] +x4 = [-0.05, 0.05] + +t = 10 seconds +control period 0.02 s + +Property: + +For t > 8.0 s +x1, x3, x4 should be in [-0.001, 0.001] diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/README.md b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/README.md new file mode 100644 index 000000000..ce2771209 --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/README.md @@ -0,0 +1,39 @@ + +# NAV Benchmark + +## Property: +The control goal is to navigate a robot to a goal region while avoiding an obstacle. +Time horizon: `t = 6s`. Control period: `0.2s`. + +Initial states: + + x1 = [2.9, 3.1] + x2 = [2.9, 3.1] + x3 = [0, 0] + x4 = [0, 0] + +Dynamic system: [dynamics.m](./dynamics.m) + +Goal region ( t=6 ): + + x1 = [-0.5, 0.5] + x2 = [-0.5, 0.5] + x3 = [-Inf, Inf] + x4 = [-Inf, Inf] + +Obstacle ( always ): + + x1 = [1, 2] + x2 = [1, 2] + x3 = [-Inf, Inf] + x4 = [-Inf, Inf] + +## Networks: + +We provide two networks: +- The first network is trained with standard (point-based) reinforcement learning: `nn-nav-point.onnx` +- The second network is trained set-based to improve its verifiable robustness by integrating reachability analysis into the training process: `nn-nav-set.onnx` + +Reference set-based training: https://arxiv.org/abs/2401.14961 + + diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/dynamics.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/dynamics.m new file mode 100644 index 000000000..632c28d9f --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/dynamics.m @@ -0,0 +1,11 @@ +function dx = dynamics(x,u) + +dx = [ + x(3)*cos(x(4)); + x(3)*sin(x(4)); + u(1); + u(2) +]; + +end + diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/nav-point.pdf b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/nav-point.pdf new file mode 100644 index 000000000..2021a5d17 Binary files /dev/null and b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/nav-point.pdf differ diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/nav-set.pdf b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/nav-set.pdf new file mode 100644 index 000000000..08969cde1 Binary files /dev/null and b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/nav-set.pdf differ diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/nav_point.mat b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/nav_point.mat new file mode 100644 index 000000000..2761f92f8 Binary files /dev/null and b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/nav_point.mat differ diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/nav_set.mat b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/nav_set.mat new file mode 100644 index 000000000..93fec9be3 Binary files /dev/null and b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/nav_set.mat differ diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-point.mat b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-point.mat new file mode 100644 index 000000000..04e1915a0 Binary files /dev/null and b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-point.mat differ diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-point.onnx b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-point.onnx new file mode 100644 index 000000000..3b4a1c4db Binary files /dev/null and b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-point.onnx differ diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-set.mat b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-set.mat new file mode 100644 index 000000000..281a9931c Binary files /dev/null and b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-set.mat differ diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-set.onnx b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-set.onnx new file mode 100644 index 000000000..7ca29df9d Binary files /dev/null and b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/networks/nn-nav-set.onnx differ diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_point.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_point.m new file mode 100644 index 000000000..725ec4c9c --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_point.m @@ -0,0 +1,121 @@ +% function rT = reach_point() + + %% Reachability analysis of NAV Benchmark + + %% Load Components + + % Load the controller + net = importNetworkFromONNX('networks/nn-nav-point.onnx', "InputDataFormats", "BC"); + net = matlab2nnv(net); + % net.InputSize = 4; + + % Load plant + reachStep = 0.02; + controlPeriod = 0.2; + plant = NonLinearODE(4, 2, @dynamics, reachStep, controlPeriod, eye(4)); + plant.set_tensorOrder(2); + + % Create NNCS + % nncs = NonlinearNNCS(net,plant); + + %% Reachability analysis + + % Initial set + lb = [2.999; 2.999; 0; 0]; + ub = [3.0; 3.0; 0; 0]; + init_set = Star(lb,ub); + + % Store all reachable sets + reachAll = init_set; + + % Reachability options + num_steps = 25; + reachOptions.reachMethod = 'approx-star'; + + % Reachabilty analysis + % reachPRM.ref_input = input_ref; + % reachPRM.numSteps = 30; + % reachPRM.init_set = init_set; + % reachPRM.numCores = 1; + % reachPRM.reachMethod = 'approx-star'; + % [R,rT] = nncs.reach(reachPRM); + % Got an error from mpt when using Gurobi... + % Checking GUROBI license ... Did not find an environment variable GRB_LICENSE_FILE with GUROBI license. + % + % Error using optimset (line 177) + % Invalid default value for property 'modules' in class 'mptopt': + % No default options available for the function 'linprog'. + % + % Error in mpt_solvers_options (line 601) + % options.linprog = optimset('linprog'); + % + % Error in mpt_subModules (line 28) + % options.(modules_list(i).name) = feval(f); + % + % Error in Polyhedron (line 264) + % MPTOPTIONS = mptopt; + % + % Error in NonlinearNNCS/nextInputSetStar (line 287) + % I1 = Polyhedron('lb', lb, 'ub', ub); + % + % Error in NonlinearNNCS/reach (line 183) + % input_set = obj.nextInputSetStar(fb_I{1}); + % + % Error in reach_point (line 41) + % [R,rT] = nncs.reach(reachPRM); + + % Begin computation + t = tic; + for i=1:num_steps + % disp(i); + + % Compute controller output set + input_set = net.reach(init_set,reachOptions); + + % Compute plant reachable set + init_set = plant.stepReachStar(init_set, input_set, 'poly'); + reachAll = [reachAll init_set]; + % toc(t); + + end + + rT = toc(t); + + R = reachAll; + + % Save results + if is_codeocean + save('/results/logs/nav_point.mat', 'R','rT','-v7.3'); + else + save('nav_point.mat', 'R','rT','-v7.3'); + end + + + %% Visualize results + plant.get_interval_sets; + + f = figure; + rectangle('Position',[-0.5,-0.5,1,1],'FaceColor',[0 0.5 0 0.5],'EdgeColor','y', 'LineWidth',0.1); % goal region + hold on; + rectangle('Position',[1,1,1,1],'FaceColor',[0.7 0 0 0.8], 'EdgeColor','r', 'LineWidth', 0.1); % obstacle + Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,1,2,'b'); + grid; + xlabel('x_1'); + ylabel('x_2'); + + % f5 = figure; + % % rectangle('Position',[-1,-1,2,2],'FaceColor',[0 0.5 0 0.5],'EdgeColor','y', 'LineWidth',0.1) + % hold on; + % Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,3,4,'b'); + % grid; + % xlabel('x_3'); + % ylabel('x_4'); + + % Save figure + if is_codeocean + exportgraphics(f,'/results/logs/nav-point.pdf', 'ContentType', 'vector'); + else + exportgraphics(f,'nav-point.pdf','ContentType', 'vector'); + end + + % end \ No newline at end of file diff --git a/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_set.m b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_set.m new file mode 100644 index 000000000..20de7d875 --- /dev/null +++ b/code/nnv/examples/Submission/ARCH-COMP2024/benchmarks/NAV/reach_set.m @@ -0,0 +1,95 @@ +% function rT = reach_set() + + %% Reachability analysis of NAV Benchmark + + %% Load Components + + % Load the controller + net = importNetworkFromONNX('networks/nn-nav-set.onnx', "InputDataFormats", "BC"); + net = matlab2nnv(net); + % Load plant + reachStep = 0.02; + controlPeriod = 0.2; + plant = NonLinearODE(4, 2, @dynamics, reachStep, controlPeriod, eye(4)); + plant.options.zonotopeOrder = 160; + plant.options.intermediateOrder = 200; + plant.options.taylorTerms = 3; + plant.set_tensorOrder(3); + + + %% Reachability analysis + + % Initial set + lb = [2.999; 2.999; 0; 0]; + ub = [3.0; 3.0; 0; 0]; + init_set = Star(lb,ub); + + % Store all reachable sets + reachAll = init_set; + + % Reachability options + num_steps = 28; + reachOptions.reachMethod = 'approx-star'; + + % Begin computation + t = tic; + for i=1:num_steps + + % Compute controller output set + input_set = net.reach(init_set,reachOptions); + + % input_set = input_set.getBox; + % input_set = Star.get_hypercube_hull(input_set); + % input_set = input_set.toStar; + + % Compute plant reachable set + init_set = plant.stepReachStar(init_set, input_set,'lin-adaptive'); + % init_set = Star.get_hypercube_hull(init_set); + % init_set = init_set.toStar; + + reachAll = [reachAll init_set]; + + end + + rT = toc(t); + + R = reachAll; + + % Save results + if is_codeocean + save('/results/logs/nav_set.mat', 'R','rT','-v7.3'); + else + save('nav_set.mat', 'R','rT','-v7.3'); + end + + + %% Visualize results + plant.get_point_sets; + + f = figure; + rectangle('Position',[-0.5,-0.5,1,1],'FaceColor',[0 0.5 0 0.5],'EdgeColor','y', 'LineWidth', 0.1); % goal region + hold on; + rectangle('Position',[1,1,1,1],'FaceColor',[0.7 0 0 0.8], 'EdgeColor','r', 'LineWidth', 0.1); % obstacle + Star.plotBoxes_2D_noFill(plant.intermediate_pointSet,1,2,'b'); + grid; + xlabel('x_1'); + ylabel('x_2'); + + % f5 = figure; + % % rectangle('Position',[-1,-1,2,2],'FaceColor',[0 0.5 0 0.5],'EdgeColor','y', 'LineWidth',0.1) + % hold on; + % Star.plotBoxes_2D_noFill(plant.intermediate_reachSet,3,4,'b'); + % grid; + % xlabel('x_3'); + % ylabel('x_4'); + + % Save figure + if is_codeocean + exportgraphics(f,'/results/logs/nav-set.pdf', 'ContentType', 'vector'); + else + exportgraphics(f,'nav-set.pdf','ContentType', 'vector'); + end + + % end + +% end \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/README.md b/code/nnv/examples/Submission/VNN_COMP2024/README.md new file mode 100644 index 000000000..c2ba5ffef --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/README.md @@ -0,0 +1,35 @@ +# Local Testing for VNN-COMP Scripts + +## File Summaries +`prepare_instance.sh` -- a script for starting a local matlab engine within which `nnv` can be ran on an instance. +`run_instance.sh` -- a script for running `nnv` on an instance. + +## `prepare_instance.sh` +Provided for the competition. Handles error-handling and set up of MATLAB engine prior to running `nnv` on the test instance. + +## `run_instance.sh` +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. diff --git a/code/nnv/examples/Submission/VNN_COMP2024/config.yaml b/code/nnv/examples/Submission/VNN_COMP2024/config.yaml new file mode 100644 index 000000000..1ed3d08d9 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/config.yaml @@ -0,0 +1,9 @@ +name: nnv +ami: ami-080fce32dc8c15ced +scripts_dir: code/nnv/examples/Submission/VNN_COMP2023/ +manual_installation_step: True +run_installation_script_as_root: False +run_post_installation_script_as_root: False +run_toolkit_as_root: False +description: > + Matlab Toolbox for Neural Network Verification. This toolbox implements reachability methods for analyzing deep learning models including but not limited to convolutional, recurrent and binary neural networks. NNV is also capable of analyzing neural networks on closed-loop controllers in autonomous cyber-physical systems (CPS). diff --git a/code/nnv/examples/Submission/VNN_COMP2024/execute.py b/code/nnv/examples/Submission/VNN_COMP2024/execute.py new file mode 100644 index 000000000..2fc237127 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/execute.py @@ -0,0 +1,119 @@ +"""Launch MATLAB Engines with Python + +This module was created for local testing of reachability analysis (https://github.com/verivital/nnv.git) ahead of VNN-COMP 2023. +To perform testing, the following functionality is enabled. + +- Start a MATLAB engine. +- Run an instance of reachability analysis given some arguments through the open MATLAB engine. + +Arguments can be passed to the call to the script and will be parsed accordingly. + +Created by: Samuel Sasaki (VeriVITAL) +Date: June 28, 2023 +""" + + +import sys +import matlab.engine +import time +import os + + +def prepare_instance(category: str, onnx: str, vnnlib: str) -> None: + """Set up the MATLAB engine for running an instance. + + Parameters: + onnx (str): the path to the .onnx file + vnnlib (str): the path to the .vnnlib file + """ + # start matlab engine as a shared engine +# eng = matlab.engine.start_matlab(background=True, option='-r "matlab.engine.shareEngine"') +# print('Engine starting...') + + # keep MATLAB engine open until manually killed +# while True: +# time.sleep(0.5) + print("We aren't actually doing anything here...") + +def run_instance(category, onnx, vnnlib, timeout, outputlocation) -> None: + """Run an instance based on parameters defined in .csv file. + + Parameters: + onnx (str): the path to the .onnx file + vnnlib (str): the path to the .vnnlib file + timeout (int): the time (in ms) to wait before proceeding to the next instance + """ + + eng = matlab.engine.start_matlab() +# eng_name = matlab.engine.find_matlab()[0] +# eng = matlab.engine.connect_matlab(name=eng_name) +# +# print(f'Successfully connected to engine: {eng_name}.') + + eng.addpath(os.getcwd()) + eng.addpath(eng.genpath('/home/ubuntu/toolkit/code/nnv/')) + + status = 2 #initialize with an 'Unknown' status + #toc = time.perf_counter() + #print('timestep :',toc) + future = eng.run_vnncomp2023_instance(category, onnx, vnnlib, outputlocation, nargout = 2, background=True) + + try: + [status, total_time] = future.result(timeout=float(timeout)) + #print('extra time = ',int(toc-tic)) + except matlab.engine.TimeoutError: + print("timeout") + #print('extra time = ',int(toc-tic)) + total_time = timeout + status = 3 + + future.cancel() + eng.quit() + + if status == 3: + resultfile = outputlocation + with open(resultfile, 'w') as f: + f.write('timeout') + # All the other results are written from matlab + + +def _get_args() -> None: + """Get the arguments passed to the script from the command line. + + Expected usage is : [ACTION, PATH_TO_ONNX, PATH_TO_VNNLIB, TIMEOUT, OUTPUTLOCATION] + """ + args = sys.argv[1:] + ACTION = args[0] + + # prepare_instance expects: benchmark_category, onnx, vnnlib + if (ACTION == 'prepare_instance'): + if len(args) != 4: + raise ValueError(f'Incorrect number of arguments, expected 4 got {len(args)}.') + args.append(None) # timeout + args.append(None) # outputlocation + + # run_instance expects: benchmark_category, onnx, vnnlib, timeout, outputlocation + if (ACTION == 'run_instance'): + if len(args) != 6: + raise ValueError(f'Incorrect number of arguments, expected 6 got {len(args)}.') + + print(args) + + return args + + +if __name__=="__main__": + # parse the arguments. + ACTION, CATEGORY, PATH_TO_ONNX, PATH_TO_VNNLIB, TIMEOUT, OUTPUTLOCATION = _get_args() + + # implement logic for each action we might want to take. + switcher = { + 'prepare_instance': lambda: prepare_instance(CATEGORY, PATH_TO_ONNX, PATH_TO_VNNLIB), # prepare_instance(PATH_TO_ONNX, PATH_TO_VNNLIB), + 'run_instance': lambda: run_instance(CATEGORY, PATH_TO_ONNX, PATH_TO_VNNLIB, TIMEOUT, OUTPUTLOCATION) # run_instance(PATH_TO_ONNX, PATH_TO_VNNLIB, TIMEOUT, OUTPUTLOCATION), + } + + # retrieve the correct function call based on the input action. + func = switcher.get(ACTION, 'Invalid')() + + if func == 'Invalid': + raise ValueError(f'Incorrect ACTION. Expected one of {list(switcher.keys())}; instead got {ACTION}.') \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/install_tool.sh b/code/nnv/examples/Submission/VNN_COMP2024/install_tool.sh new file mode 100644 index 000000000..a8e0be54d --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/install_tool.sh @@ -0,0 +1,36 @@ +#!/bin/bash + +# Installation script used for VNN-COMP. Ubuntu, MATLAB R2024a (https://github.com/verivital/nnv) + +TOOL_NAME="nnv" +VERSION_STRING="v1" + +# check arguments +if [ "$1" != ${VERSION_STRING} ]; then + echo "Expected first argument (version string) '$VERSION_STRING', got '$1'" + exit 1 +fi + +echo "Installing $TOOL_NAME dependencies" + +# Install support packages (ONNX importer) +curl --retry 100 --retry-connrefused -L -O https://www.dropbox.com/s/4p17xm4tlm8r9gs/sppFile.zip # need to do this step for R2024a +sleep 60 +sudo unzip sppFile.zip -d /home/ubuntu/toolkit/code/nnv +sudo rm sppFile.zip + +# This is called networks2023, but it contains the MATLAB networks for most of 2022 and 2023 (Do we need this step for 2024?) +cd /home/ubuntu/toolkit/code/nnv/examples/Submission/VNN_COMP2023/ +curl --retry 100 --retry-connrefused -L -O https://www.dropbox.com/scl/fi/chb0fotern4r5sycz57r9/networks2023.zip?rlkey=1cwvh73b5zgtnb67xdrvlg8am&dl=0 + +sleep 60 + +unzip *.zip* + +ip link show # get mac address (for licensing) + +echo $USER # get usernme (for licensing) + +mkdir ~/.matlab/R2024a_licenses + +# ADD STEPS TO INSTALL GUROBI \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/post_install.sh b/code/nnv/examples/Submission/VNN_COMP2024/post_install.sh new file mode 100644 index 000000000..f6aa91127 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/post_install.sh @@ -0,0 +1,31 @@ +cd ~/.matlab/R2024a_licenses + +curl --retry 100 --retry-connrefused -L -O +sleep 60 +ls -al + +unzip *.zip* + +ls -al + +cp -f license.lic /usr/local/matlab/licenses/ + +rm /usr/local/matlab/licenses/license_info.xml + +matlab -nodisplay -r "cd /home/ubuntu/toolkit/code/nnv/examples/Submission/VNN_COMP2023/; prepare_run; quit" + +sudo apt install -y python3-pip +pip install numpy + +cd /usr/local/matlab/extern/engines/python +python3 -m pip install . + +# ADD STEPS TO INSTALL GUROBI + +# TEST IF MATLAB ENGINE IS INSTALLED PROPERLY +# START_ENGINE ='import matlab.engine\nimport time\neng = matlab.engine.start_matlab() \nprint(eng) \neng.prepare_run() \nexit()' +# python3 -c "exec('import matlab.engine\nimport time\neng = matlab.engine.start_matlab() \nprint(eng) \neng.prepare_run(nargout = 0, background=True) \nexit()')" + +# TEST IF WE CAN FIND MATLAB +# cd /home/ubuntu/toolkit/code/nnv/examples/Submission/VNN_COMP2023/ +# ./prepare_instance.sh v1 acasxu acas xu diff --git a/code/nnv/examples/Submission/VNN_COMP2024/prepare_instance.sh b/code/nnv/examples/Submission/VNN_COMP2024/prepare_instance.sh new file mode 100644 index 000000000..04452300c --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/prepare_instance.sh @@ -0,0 +1,38 @@ +#!/bin/bash + +# example prepare_instance.sh script for VNNCOMP 2024 for nnv (https://github.com/verivital/nnv.git) +# four arguments, first is "v1", second is a benchmark category identifier string such as "acasxu", third is a path to the .onnx file and fourth is a path to .vnnlib file + +TOOL_NAME="nnv" +VERSION_STRING="v1" + +# check arguments +if [ "$1" != ${VERSION_STRING} ]; then + echo "Expected first argument (version string) '$VERSION_STRING', got '$1'" + exit 1 +fi + +CATEGORY=$2 +ONNX_FILE=$3 +VNNLIB_FILE=$4 + +echo "Preparing $TOOL_NAME for benchmark instance in category '$CATEGORY' with onnx file '$ONNX_FILE' and vnnlib file '$VNNLIB_FILE'" + +# kill any zombie processes +killall -q python3 +# killall -q python +killall -q matlab + +#WAIT_FOR_CONNECTION_TO_CLOSE='import matlab.engine\nimport time\nwhile matlab.engine.find_matlab(): time.sleep(1)' +# python3 -c "exec('$WAIT_FOR_CONNECTION_TO_CLOSE')" +# python -c "exec('$WAIT_FOR_CONNECTION_TO_CLOSE')" + +# start the matlab engine in background and keep the connection open +# python3 /home/ubuntu/toolkit/code/nnv/examples/Submission/VNN_COMP2023/execute.py 'prepare_instance' $CATEGORY $ONNX_FILE $VNNLIB_FILE & +# python execute.py 'prepare_instance' $CATEGORY $ONNX_FILE $VNNLIB_FILE & + +WAIT_FOR_CONNECTION_TO_OPEN='import matlab.engine\nimport time\nwhile not matlab.engine.find_matlab(): time.sleep(1) \nprint(eng)' +# python3 -c "exec('$WAIT_FOR_CONNECTION_TO_OPEN')" +# python -c "exec('$WAIT_FOR_CONNECTION_TO_OPEN')" + +exit 0 diff --git a/code/nnv/examples/Submission/VNN_COMP2024/prepare_run.m b/code/nnv/examples/Submission/VNN_COMP2024/prepare_run.m new file mode 100644 index 000000000..a0b21a7b3 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/prepare_run.m @@ -0,0 +1,32 @@ +function prepare_run() + +%% Print out some info to prepare for the comp + +% remove paths from any prior installation (if any) +% rmpath(genpath('/home/ubuntu/toolkit/code/nnv/')); savepath; + +% installing nnv +cd /home/ubuntu/toolkit/code/nnv/; +install; +% save path to NNV +addpath(genpath('/home/ubuntu/toolkit/code/nnv/')); savepath; + +%disp(""); +%disp("Support package path"); +%disp(matlabshared.supportpkg.getSupportPackageRoot); + +%disp(" ") +%disp("MATLAB root"); +%disp(matlabroot); + +% set support package root to import onnx location +%matlabshared.supportpkg.setSupportPackageRoot('/usr/local/MATLAB/R2022b'); +%addpath(genpath('/usr/local/MATLAB')); + +disp("Support package path"); +disp(matlabshared.supportpkg.getSupportPackageRoot); + +savepath; +% quit; + +end \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/run_all_instances_from_csv.m b/code/nnv/examples/Submission/VNN_COMP2024/run_all_instances_from_csv.m new file mode 100644 index 000000000..d21a17660 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/run_all_instances_from_csv.m @@ -0,0 +1,37 @@ +%% Run as many benchmarks as possible from 2023 + +vnncomp_path = "C:\Users\diego\Documents\Research\vnncomp2023_benchmarks\benchmarks\"; + +benchmarks = dir(vnncomp_path); + +notSupported = {'test'; 'traffic_signs_recognition'; 'cctsdb_yolo'}; % skip for now + +for i=4:length(benchmarks) + + if ~contains(notSupported, benchmarks(i).name) % skip evaluation of benchmarks not supported + + benchpath = vnncomp_path + benchmarks(i).name; + + instances = readmatrix(benchpath + "/instances.csv", "OutputType","string", "Delimiter",","); + + results_dir = "results_approx_" + benchmarks(i).name; + mkdir(results_dir); + + for k=1:size(instances,1) + + onnx = benchpath + filesep + instances(k,1); + vnnlib = benchpath + filesep + instances(k,2); + + try + run_vnncomp2024_instance(benchmarks(i).name,onnx,vnnlib, results_dir + "/instance_" + string(k)+".txt"); + catch ME + fid = fopen(results_dir + "/instance_" + string(k)+".txt", 'w'); + fprintf(fid, [ME.message '\n']); + fclose(fid); + end + + end + + end + +end \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/run_instance.sh b/code/nnv/examples/Submission/VNN_COMP2024/run_instance.sh new file mode 100644 index 000000000..d7016a5e8 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/run_instance.sh @@ -0,0 +1,37 @@ +#!/bin/bash + +# example run_instance.sh script for VNNCOMP 2024 for nnv (https://github.com/verivital/nnv.git) +# four arguments, first is "v1", second is a benchmark category identifier string such as "acasxu", third is a path to the .onnx file and fourth is a path to .vnnlib file +# modified: Samuel Sasaki, June 28th 2023 + +TOOL_NAME="nnv" +VERSION_STRING="v1" + +# check arguments +if [ "$1" != ${VERSION_STRING} ]; then + echo "Expected first argument (version string) '$VERSION_STRING', got '$1'" + exit 1 + +fi + +CATEGORY=$2 +ONNX_FILE=$3 +VNNLIB_FILE=$4 +RESULTS_FILE=$5 +TIMEOUT=$6 + +echo "Running $TOOL_NAME on benchmark instance in category '$CATEGORY' with onnx file '$ONNX_FILE', vnnlib file '$VNNLIB_FILE', results file $RESULTS_FILE, and timeout $TIMEOUT" + +# setup environment variable for tool (doing it earlier won't be persistent with docker)" +#DIR=$(dirname $(dirname $(realpath $0))) +#export PYTHONPATH="$PYTHONPATH:$DIR/src" + +echo $PYTHONPATH +# TIMEOUT=$5 + +# echo "Running $TOOL_NAME on benchmark instance in category '$CATEGORY' with onnx file '$ONNX_FILE', vnnlib file '$VNNLIB_FILE', and timeout $TIMEOUT" + +python3 /home/ubuntu/toolkit/code/nnv/examples/Submission/VNN_COMP2023/execute.py 'run_instance' "$CATEGORY" "$ONNX_FILE" "$VNNLIB_FILE" "$TIMEOUT" "$RESULTS_FILE" +# sudo python3 execute.py 'run_instance' "$CATEGORY" "$ONNX_FILE" "$VNNLIB_FILE" "$TIMEOUT" "$RESULTS_FILE" + +echo "" diff --git a/code/nnv/examples/Submission/VNN_COMP2024/run_vnncomp2024_instance.m b/code/nnv/examples/Submission/VNN_COMP2024/run_vnncomp2024_instance.m new file mode 100644 index 000000000..1903521ac --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/run_vnncomp2024_instance.m @@ -0,0 +1,533 @@ +function [status, tTime] = run_vnncomp2024_instance(category, onnx, vnnlib, outputfile) + +% single script to run all instances (supported) from the vnncomp2024 + +t = tic; % start timer +status = 2; % unknown (to start with) + +% Process: +% 1) Load components +% 2) SAT? - Randomly evaluate network to search for counterexample +% 3) UNSAT? +% a) Compute reachability +% b) Verify (compute intersection between reach set and output property halfspace) + +%% 1) Load components + +% Load networks + +[net, nnvnet, needReshape] = load_vnncomp_network(category, onnx); + +inputSize = net.Layers(1, 1).InputSize; + + +% Load property to verify +property = load_vnnlib(vnnlib); +lb = property.lb; % input lower bounds +ub = property.ub; % input upper bounds +prop = property.prop; % output spec to verify + + +%% 2) SAT? + +nRand = 100; % number of random inputs (this can be changed) +% We got some penalties last year, why? +% Wrong vnnlib parsing? Wrong counterrexample writing? Do we need to reshape it? +% Let's test last years properties and make sure those errors/bugs are +% fixed before this year's submission + +% Choose how to falsify based on vnnlib file +if ~isa(lb, "cell") && length(prop) == 1 % one input, one output + counterEx = falsify_single(net, lb, ub, inputSize, nRand, prop{1}.Hg, needReshape); +elseif isa(lb, "cell") && length(lb) == length(prop) % multiple inputs, multiple outputs + for spc = 1:length(lb) % try parfeval, parfor does not work for early return + counterEx = falsify_single(net, lb{spc}, ub{spc}, inputSize, nRand, prop{spc}.Hg, needReshape); + if iscell(counterEx) + break + end + end +elseif isa(lb, "cell") && length(prop) == 1 % can violate the output property from any of the input sets + for arr = 1:length(lb) % try parfeval, parfor does not work for early return + counterEx = falsify_single(net, lb{arr}, ub{arr}, inputSize, nRand, prop{1}.Hg, needReshape); + if iscell(counterEx) + break + end + end +else + warning("Working on adding support to other vnnlib properties"); +end + +cEX_time = toc(t); + +%% 3) UNSAT? + +% Define reachability options +% Let's try to choose this better from the get-go + +% Option 1 +% reachOptions_relax100 = struct; +% reachOptions_relax100.reachMethod = 'relax-star-range'; +% reachOptions_relax100.relaxFactor = 1; +% +% % Option 2 +% reachOptions_relax50 = struct; +% reachOptions_relax50.reachMethod = 'relax-star-range'; +% reachOptions_relax50.relaxFactor = 0.5; +% +% % Option 3 +% reachOptions_exact = struct; +% reachOptions_exact.reachMethod = 'exact-star'; +% reachOptions_exact.reachOption = 'parallel'; +% reachOptions_exact.numCores = feature('numcores'); +% +% % Option 4 +% reachOptions_approx.reachMethod = 'approx-star'; +% +% % Choosing reachOptions (based on size, but not sure how to decice really...) +% if prod(inputSize) > 3000 % [32 32 3] +% reachOptions = {reachOptions_relax100; reachOptions_relax50; reachOptions_approx}; +% else +% reachOptions = {reachOptions_relax50; reachOptions_approx; reachOptions_exact}; +% end + +reachOptions = struct; +reachOptions.reachMethod = 'approx-star'; +% reachOptions.reachMethod = 'exact-star'; + + +% Check if property was violated earlier +if iscell(counterEx) + status = 0; +end + +vT = tic; + +if status == 2 && isa(nnvnet, "NN") % no counterexample found and supported for reachability (otherwise, skip step 3 and write results) + +% Choose how to verify based on vnnlib file + if ~isa(lb, "cell") && length(prop) == 1 % one input, one output + + IS = create_input_set(lb, ub, inputSize, needReshape); + + % Compute reachability + ySet = nnvnet.reach(IS, reachOptions); + + % Verify property + status = verify_specification(ySet, prop); + + elseif isa(lb, "cell") && length(lb) == length(prop) % multiple inputs, multiple outputs + + local_status = ones(length(lb),1); % track status for each specification in the vnnlib + + parfor spc = 1:length(lb) % We can compute these in parallel for faster computation + + lb_spc = lb{spc}; + ub_spc = ub{spc}; + + IS = create_input_set(lb_spc, ub_spc, inputSize, needReshape); + + % Compute reachability + ySet = nnvnet.reach(IS, reachOptions); + + % Verify property + if isempty(ySet.C) + dd = ySet.V; DD = ySet.V; + ySet = Star(dd,DD); + end + + % Add verification status + local_status(spc) = verify_specification(ySet, prop(spc)); + + end + + % Check for the global verification result + if all(local_status == 1) + status = 1; + else + status = 2; + end + + elseif isa(lb, "cell") && length(prop) == 1 % one specification, multiple input definitions + + local_status = ones(length(lb),1); % track status for each specification in the vnnlib + + parfor spc = 1:length(lb) % We can compute these in parallel for faster computation + + lb_spc = lb{spc}; + ub_spc = ub{spc}; + + IS = create_input_set(lb_spc, ub_spc, inputSize, needReshape); + + % Compute reachability + ySet = nnvnet.reach(IS, reachOptions); + + % Verify property + local_status(spc) = verify_specification(ySet, prop); + + end + + % Check for the global verification result + if all(local_status == 1) + status = 1; + else + status = 2; + end + + else + warning("Working on adding support to other vnnlib properties") + end + +end + +vT = toc(vT); + +%% 4) Process results + +tTime = toc(t); % save total computation time + +disp("Verification result: " + string(status)); +disp("Counterexample search time: " + string(cEX_time)); +disp("Reachability time: " + string(vT)); +disp("Total Time: "+ string(tTime)); +disp( " "); + +% Write results to output file +if status == 0 + fid = fopen(outputfile, 'w'); + fprintf(fid, 'sat \n'); + fprintf(fid, '%f \n', tTime); % remove this line when running on submission site + fclose(fid); + write_counterexample(outputfile, counterEx) +elseif status == 1 + fid = fopen(outputfile, 'w'); + fprintf(fid, 'unsat \n'); + fprintf(fid, '%f \n', tTime); % remove this line when running on submission site + fclose(fid); +elseif status == 2 + fid = fopen(outputfile, 'w'); + fprintf(fid, 'unknown \n'); + fprintf(fid, '%f \n', tTime); % remove this line when running on submission site + fclose(fid); +end + +% quit; % does this work when running matlab.engine from python in background? + + +end + +%% Helper functions + +function IS = create_input_set(lb, ub, inputSize, needReshape) + + % Get input bounds + if ~isscalar(inputSize) + lb = reshape(lb, inputSize); + ub = reshape(ub, inputSize); + end + + % Format bounds into correct dimensions + if needReshape == 1 + lb = permute(lb, [2 1 3]); + ub = permute(ub, [2 1 3]); + elseif needReshape == 2 + newSize = [inputSize(2) inputSize(1) inputSize(3:end)]; + lb = reshape(lb, newSize); + lb = permute(lb, [2 1 3 4]); + ub = reshape(ub, newSize); + ub = permute(ub, [2 1 3 4]); + end + + % Create input set + % IS = ImageStar(lb, ub); % too many constraints, slower + i_diff = ub - lb; + V(:,:,:,1) = lb; % assume lb is center of set (instead of img) + V(:,:,:,2) = i_diff ; % basis vectors + C = [1; -1]; % constraints + d = [1; -1]; + IS = ImageStar(V, C, d, 0, 1); % input set + +end + +function [net,nnvnet,needReshape] = load_vnncomp_network(category, onnx) +% load participating vnncomp 2024 benchmark NNs +% +% Regular Track Benchmarks +% - 2024 +% - safeNLP +% - cora +% - linearizeNN +% - cifar100 +% - tinyimagenet +% - 2023 +% - nn4sys +% - dist-shift +% - acasxu +% - cgan +% - collins_rul_cnn +% - metaroom +% - tllverifybench +% +% Extended Track Benchmarks +% - 2024 +% - ml4acopf +% - dynaroars/benchmark-generation (name may change for competition) +% - collins_yolo +% - LSNC (not supported) +% - 2023 +% - yolo +% - cctsdb_yolo +% - collins_yolo_robustness (same as collins_yolo I believe) +% - ml4acopf (different than this year's?) +% - traffic_sign_recognition +% - vggnet16 +% - vit +% + + needReshape = 0; % default is to use MATLAB reshape, otherwise use the python reshape + + if contains(category, 'collins_rul') + net = importNetworkFromONNX(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") + % nn4sys: onnx to nnv + net = importNetworkFromONNX(onnx, "OutputDataFormats", "BC"); % lindex + nnvnet = matlab2nnv(net); + else + error("We don't have those"); + end + + elseif contains(category, "ml4acopf") + % ml4acopf: onnx to matlab + net = importNetworkFromONNX(onnx, "InputDataFormats", "BC"); + nnvnet = ""; + + elseif contains(category, "dist_shift") + % dist_shift: onnx to matlab, , matlab to nnv? + net = importNetworkFromONNX(onnx, "InputDataFormats", "BC", 'OutputDataFormats',"BC"); %reshape + try + nnvnet = matlab2nnv(net); + catch + nnvnet = ""; + end + + elseif contains(category, "cgan") + % cgan: onnx to nnv + net = importNetworkFromONNX(onnx,"InputDataFormats", "BC", 'OutputDataFormats',"BC"); %reshape + nnvnet = matlab2nnv(net); + + elseif contains(category, "vggnet16") + % vgg16: onnx to matlab + net = importNetworkFromONNX(onnx); % flattenlayer + nnvnet = ""; + needReshape = 1; + + elseif contains(category, "tllverify") + % tllverify: onnx to nnv + net = importNetworkFromONNX(onnx,"InputDataFormats", "BC", 'OutputDataFormats',"BC"); + nnvnet = matlab2nnv(net); + + elseif contains(category, "vit") + % vit: onnx to matlab + net = importNetworkFromONNX(onnx, "InputDataFormats", "BCSS", 'OutputDataFormats',"BC"); + nnvnet = ""; + needReshape= 1; + + elseif contains(category, "cctsdb_yolo") + % cctsdb_yolo: onnx to matlab + error("We do not support this one"); + % net = importNetworkFromONNX(onnx); + % nnvnet = ""; + % needReshape = ?; + % We cannot support this one + + elseif contains(category, "collins_yolo") + % collins_yolo: onnx to matlab + net = importNetworkFromONNX(onnx); + nnvnet = ""; + + elseif contains(category, "yolo") + % yolo: onnx to nnv + net = importNetworkFromONNX(onnx); % padlayer + nnvnet = matlab2nnv(net); + + elseif contains(category, "acasxu") + % acasxu: onnx to nnv + net = importNetworkFromONNX(onnx, "InputDataFormats","BCSS"); + nnvnet = matlab2nnv(net); + + elseif contains(category, "cifar100") + % cifar100: onnx to nnv + net = importNetworkFromONNX(onnx, "InputDataFormats","BCSS", "OutputDataFormats","BC"); + nnvnet = matlab2nnv(net); + needReshape = 1; + + elseif contains(category, "tinyimagenet") + % tinyimagenet: onnx to nnv + net = importNetworkFromONNX(onnx, "InputDataFormats","BCSS", "OutputDataFormats","BC"); + nnvnet = matlab2nnv(net); + % needReshpae = ? + + elseif contains(category, "LinearizeNN") + % LinerizeNN: onnx to nnv + net = importNetworkFromONNX(onnx, "InputDataFormats","BC", "OutputDataFormats","BC"); + nnvnet = matlab2nnv(net); + % needReshape = ? + + elseif contains(category, "safeNLP") + % safeNLP: onnx to nnv + net = importNetworkFromONNX(onnx, "InputDataFormats","BC", "OutputDataFormats","BC"); + nnvnet = matlab2nnv(net); + % needReshape = ? + + elseif contains(category, "cora") + % cora benchmark: onnx 2 nnv + net = importNetworkFromONNX(onnx, "InputDataFormats","BC", "OutputDataFormats","BC"); + nnvnet = matlab2nnv(net); + % needReshape = ? + + elseif contains(category, "LSNC") + % lyapunov benchmark: onnx to nnv (barely, some IR and opset version differences) + net = importNetworkFromONNX(onnx, "InputDataFormats","BC", "OutputDataFormats","BC"); + nnvnet = ""; + % needReshape = ? + + elseif contains(category, "generation") + % dynaroars/vnncomp-benchmark-generation + net = importNetworkFromONNX(onnx, "InputDataFormats","BCSS", "OutputDataFormats","BC"); + nnvnet = matlab2nnv(net); + % needReshape = ? + + elseif contains(category, "metaroom") + % metaroom: onnx to matlab + net = importNetworkFromONNX(onnx, "InputDataFormats","BCSS", "OutputDataFormats","BC"); + nnvnet = matlab2nnv(net); + needReshape = 2; + + else % all other benchmarks + % traffic: onnx to matlab: opset15 issues + error("ONNX model not supported") + end + +end + +% Create an array of random examples from input set and reshape if necessary +% We use dlnetwork for simulation (MATLAB data structure) +function xRand = create_random_examples(net, lb, ub, nR, inputSize, needReshape) + xB = Box(lb, ub); % lb, ub must be vectors + xRand = xB.sample(nR-2); + xRand = [lb, ub, xRand]; + if needReshape + if needReshape ==2 % for collins only (full_window_40) and metaroom + newSize = [inputSize(2) inputSize(1) inputSize(3:end)]; + xRand = reshape(xRand, [newSize nR]); + xRand = permute(xRand, [2 1 3 4]); + else + xRand = reshape(xRand, [inputSize nR]); + xRand = permute(xRand, [2 1 3 4]); + end +% xRand = python_reshape(xRand, [inputSize nR]); + else + xRand = reshape(xRand,[inputSize nR]); % reshape vectors into net input size + end + if isa(net, 'dlnetwork') % need to convert to dlarray + if isa(net.Layers(1, 1), 'nnet.cnn.layer.ImageInputLayer') + xRand = dlarray(xRand, "SSCB"); + elseif isa(net.Layers(1, 1), 'nnet.cnn.layer.FeatureInputLayer') || isa(net.Layers(1, 1), 'nnet.onnx.layer.FeatureInputLayer') + xRand = dlarray(xRand, "CB"); + else + disp(net.Layers(1,1)); + error("Unknown input format"); + end + end +end + +% Write counterexample to output file +function write_counterexample(outputfile, counterEx) + % First line - > sat + % after that, write the variables for each input dimension of the counterexample + % + % Example: + % ( (X_0 0.12132) + % (X_1 3.45454) + % ( .... ) + % (Y_0 2.32342) + % (Y_1 3.24355) + % ( ... ) + % (Y_N 0.02456)) + % + + precision = '%.16g'; % set the precision for all variables written to txt file + % open file and start writing counterexamples + fid = fopen(outputfile, 'a+'); + x = counterEx{1}; + x = reshape(x, [], 1); + % begin specifying value for input example + fprintf(fid,'('); + for i = 1:length(x) + fprintf(fid, "(X_" + string(i-1) + " " + num2str(x(i), precision)+ ")\n"); + end + y = counterEx{2}; + y = reshape(y, [], 1); + % specify values for output example + for j =1:length(y) + fprintf(fid, "(Y_" + string(j-1) + " " + num2str(y(j), precision)+ ")\n"); + end + fprintf(fid, ')'); + % close and save file + fclose(fid); + +end + +% Falsification function (random simulation looking for counterexamples) +function counterEx = falsify_single(net, lb, ub, inputSize, nRand, Hs, needReshape) + counterEx = nan; + xRand = create_random_examples(net, lb, ub, nRand, inputSize, needReshape); + s = size(xRand); + n = length(s); + % look for counterexamples + for i=1:s(n) + x = get_example(xRand, i); + yPred = predict(net, x); + if isa(x, 'dlarray') % if net is a dlnetwork + x = extractdata(x); + yPred = extractdata(yPred); + end + % check if property violated + yPred = reshape(yPred, [], 1); % convert to column vector (if needed) + for h=1:length(Hs) + if Hs(h).contains(double(yPred)) % property violated + counterEx = {x; yPred}; % save input/output of countex-example + break; + end + end + end + +end + +% Get random example from input set +function x = get_example(xRand,i) + s = size(xRand); + n = length(s); + if n == 4 + x = xRand(:,:,:,i); + elseif n == 3 + x = xRand(:,:,i); + elseif n == 2 + x = xRand(:,i); + xsize = size(x); + if xsize(1) ~= 1 && ~isa(x,"dlarray") + x = x'; + end + else + error("InputSize = "+string(s)); + end +end + diff --git a/code/nnv/examples/Submission/VNN_COMP2024/test_extendedTrack_instances.m b/code/nnv/examples/Submission/VNN_COMP2024/test_extendedTrack_instances.m new file mode 100644 index 000000000..58c65071a --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/test_extendedTrack_instances.m @@ -0,0 +1,90 @@ +%% Run some verification instances from the competition + +% path to 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/"; +vnncomp_path = "C:\Users\diego\Documents\Research\vnncomp2023_benchmarks\benchmarks\"; + + +%% ViT + +disp("Running ViT...") + +vit_path = vnncomp_path + "vit/"; + +vit_instances = [... + "onnx/ibp_3_3_8.onnx" , "vnnlib/ibp_3_3_8_9119.vnnlib";... + "onnx/pgd_2_3_16.onnx","vnnlib/pgd_2_3_16_4021.vnnlib";... + ]; + +% Run verification for vit +for i=1:length(vit_instances) + onnx = vit_path + vit_instances(i,1); + vnnlib = vit_path + vit_instances(i,2); + run_vnncomp2024_instance("vit",onnx,vnnlib,"vit_results_" + string(i)+".txt"); +end + + + +%% traffic_sign +% we should be able to support it, but matlab does not, so we would have to create the models manually... +% can load most info with Keras importer + + +%% vggnet16 + +disp("Running vggnet16...") + +vgg_path = vnncomp_path + "vggnet16/"; + +vgg_instances = ["onnx/vgg16-7.onnx","vnnlib/spec0_pretzel.vnnlib";... + "onnx/vgg16-7.onnx","vnnlib/spec6_groom.vnnlib";... + "onnx/vgg16-7.onnx","vnnlib/spec16_restaurant.vnnlib";... +]; + +% Run verification for vgg16 (error when creating random examples, array size too large) +% I can imagine that similar errors will be encountered when running verification +% It seems okay on my home computer (MATLAB R2024a) + +% Run verification for vgg16 +for i=1:length(vgg_instances) + onnx = vgg_path + vgg_instances(i,1); + vnnlib = vgg_path + vgg_instances(i,2); + run_vnncomp2024_instance("vggnet16",onnx,vnnlib,"vgg_results_" + string(i)+".txt"); +end + + +%% ml4acopf + +disp("Running ml4acopf..") + +ml4_path = vnncomp_path + "ml4acopf/"; + +ml4_instances = ["onnx/118_ieee_ml4acopf.onnx","vnnlib/118_ieee_prop2.vnnlib";... + "onnx/14_ieee_ml4acopf.onnx","vnnlib/14_ieee_prop9.vnnlib";... + "onnx/300_ieee_ml4acopf.onnx","vnnlib/300_ieee_prop3.vnnlib"]; + +% Run verification for ml4acopf +for i=1:length(ml4_instances) + onnx = ml4_path + ml4_instances(i,1); + vnnlib = ml4_path + ml4_instances(i,2); + run_vnncomp2024_instance("ml4acopf",onnx,vnnlib,"ml4_results_" + string(i)+".txt"); +end + +%% cctsdb_yolo + +disp("Running cctsdb_yolo..") + +cctyolo_path = vnncomp_path + "cctsdb_yolo/"; + +cctyolo_instances = ["onnx/patch-1.onnx", "spec_onnx_patch-1_idx_00087_1.vnnlib"; ... + "onnx/patch-3.onnx", "spec_onnx_patch-1_idx_00055_0.vnnlib"; ... +]; + +% Run verification for cctsdb_yolo +for i=1:length(cctyolo_instances) + onnx = cctyolo_path + cctyolo_instances(i,1); + vnnlib = cctyolo_path + cctyolo_instances(i,2); + run_vnncomp2024_instance("cctsdb_yolo",onnx,vnnlib,"cctsdb_yolo_results_" + string(i)+".txt"); +end + diff --git a/code/nnv/examples/Submission/VNN_COMP2024/test_mainTrack_instances.m b/code/nnv/examples/Submission/VNN_COMP2024/test_mainTrack_instances.m new file mode 100644 index 000000000..81764a3a9 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/test_mainTrack_instances.m @@ -0,0 +1,267 @@ +%% Run some verification instances from the competition + +% path to benchmarks ( change to whatever local path vnncomp benchmarks are) +% vnncomp_path = "/home/manzand/Documents/MATLAB/vnncomp2023_benchmarks/benchmarks/"; +% vnncomp_path = "/home/dieman95/Documents/MATLAB/vnncomp2023_benchmarks/benchmarks/"; +vnncomp_path = "C:\Users\diego\Documents\Research\vnncomp2023_benchmarks\benchmarks\"; + +% Things look better than last year, let's make sure we have no penalties this time +% Can we support any other benchmarks? what are the errors we are getting +% in some of them? + + +%% acasxu + +disp("Running acas xu...") + +acas_path = vnncomp_path + "acasxu/"; + +acas_instances = [... + "onnx/ACASXU_run2a_1_1_batch_2000.onnx" , "vnnlib/prop_1.vnnlib";... + "onnx/ACASXU_run2a_2_3_batch_2000.onnx","vnnlib/prop_2.vnnlib";... + "onnx/ACASXU_run2a_3_4_batch_2000.onnx","vnnlib/prop_3.vnnlib";... + "onnx/ACASXU_run2a_2_5_batch_2000.onnx","vnnlib/prop_4.vnnlib";... + "onnx/ACASXU_run2a_1_1_batch_2000.onnx","vnnlib/prop_5.vnnlib";... + "onnx/ACASXU_run2a_1_1_batch_2000.onnx","vnnlib/prop_6.vnnlib";... + "onnx/ACASXU_run2a_1_9_batch_2000.onnx","vnnlib/prop_7.vnnlib";... + "onnx/ACASXU_run2a_2_9_batch_2000.onnx","vnnlib/prop_8.vnnlib";... + "onnx/ACASXU_run2a_3_3_batch_2000.onnx","vnnlib/prop_9.vnnlib";... + "onnx/ACASXU_run2a_4_5_batch_2000.onnx","vnnlib/prop_10.vnnlib";... + ]; + +% Run verification for acas +for i=1:length(acas_instances) + onnx = acas_path + acas_instances(i,1); + vnnlib = acas_path + acas_instances(i,2); + run_vnncomp2024_instance("acasxu",onnx,vnnlib,"acas_results_" + string(i)+".txt"); +end + + +%% nn4sys + +disp("Running nn4sys...") + +% We got some penalties here as well... +% I already looked into this after competition 2023 and it seems fixed + +nn4sys_path = vnncomp_path + "nn4sys/"; + +nn4sys_instances = [... % all other networks are not supported... + "onnx/lindex.onnx","vnnlib/lindex_1.vnnlib";... + "onnx/lindex_deep.onnx", "vnnlib/lindex_200.vnnlib";... + ]; + +% Run verification for nn4sys +for i=1:length(nn4sys_instances) + onnx = nn4sys_path + nn4sys_instances(i,1); + vnnlib = nn4sys_path + nn4sys_instances(i,2); + run_vnncomp2024_instance("nn4sys",onnx,vnnlib,"nn4sys_results_" + string(i)+".txt"); +end + +% need to update the support for these vnnlib properties, should be pretty quick + +%% dist_shift + +disp("Running dist_shift...") + +dist_path = vnncomp_path + "dist_shift/"; + +dist_instances = ["onnx/mnist_concat.onnx" ,"vnnlib/index6731_delta0.13.vnnlib";... + "onnx/mnist_concat.onnx" ,"vnnlib/index7_delta0.13.vnnlib";... + "onnx/mnist_concat.onnx" ,"vnnlib/index9830_delta0.13.vnnlib";... + ]; % something is failing with these ones, let's take a look at that + +% Run verification for dist_shift +for i=1:length(dist_instances) + onnx = dist_path + dist_instances(i,1); + vnnlib = dist_path + dist_instances(i,2); + run_vnncomp2024_instance("dist_shift",onnx,vnnlib,"dist_results_" + string(i)+".txt"); +end + + +%% collins_rul + +% We got penaltis here last year? Let's check that out +% Results (SAT/UNSAT seem to match those of nnenum which had no penalties) +% let's check the counterexamples generated... + +disp("Running collins_rul..") + +rul_path = vnncomp_path + "collins_rul_cnn/"; + +rul_instances = ["onnx/NN_rul_small_window_20.onnx" ,"vnnlib/robustness_2perturbations_delta5_epsilon10_w20.vnnlib";... + "onnx/NN_rul_small_window_20.onnx" ,"vnnlib/monotonicity_CI_shift5_w20.vnnlib";... + "onnx/NN_rul_small_window_20.onnx" ,"vnnlib/if_then_5levels_w20.vnnlib";... + "onnx/NN_rul_full_window_20.onnx", "vnnlib/robustness_2perturbations_delta5_epsilon10_w20.vnnlib";... + "onnx/NN_rul_full_window_40.onnx" ,"vnnlib/robustness_2perturbations_delta5_epsilon10_w40.vnnlib"]; + +% Run verification for collins_rul +for i=1:length(rul_instances) + onnx = rul_path + rul_instances(i,1); + vnnlib = rul_path + rul_instances(i,2); + run_vnncomp2024_instance("collins_rul",onnx,vnnlib,"collins_rul_results_" + string(i)+".txt"); +end + +%% cgan + +disp("Running cgan..") + +cgan_path = vnncomp_path + "cgan/"; + +cgan_instances = ["onnx/cGAN_imgSz32_nCh_1.onnx", "vnnlib/cGAN_imgSz32_nCh_1_prop_0_input_eps_0.010_output_eps_0.015.vnnlib";... + "onnx/cGAN_imgSz32_nCh_3.onnx", "vnnlib/cGAN_imgSz32_nCh_3_prop_0_input_eps_0.015_output_eps_0.020.vnnlib";... + "onnx/cGAN_imgSz64_nCh_1.onnx", "vnnlib/cGAN_imgSz64_nCh_1_prop_1_input_eps_0.005_output_eps_0.010.vnnlib";... + "onnx/cGAN_imgSz64_nCh_3.onnx", "vnnlib/cGAN_imgSz64_nCh_3_prop_2_input_eps_0.005_output_eps_0.010.vnnlib";... + % "onnx/cGAN_imgSz32_nCh_3_nonlinear_activations.onnx", "vnnlib/cGAN_imgSz32_nCh_3_nonlinear_activations_prop_0_input_eps_0.010_output_eps_0.015.vnnlib";... % conv2D error (data and filter have different data types) + "onnx/cGAN_imgSz32_nCh_1_transposedConvPadding_1.onnx", "vnnlib/cGAN_imgSz32_nCh_1_transposedConvPadding_1_prop_0_input_eps_0.010_output_eps_0.015.vnnlib";... + % "onnx/cGAN_imgSz32_nCh_3_upsample.onnx", "vnnlib/cGAN_imgSz32_nCh_3_upsample_prop_0_input_eps_0.010_output_eps_0.015.vnnlib";... % reshape error reachability + % "onnx/cGAN_imgSz32_nCh_3_small_transformer.onnx", "vnnlib/cGAN_imgSz32_nCh_3_small_transformer_prop_0_input_eps_0.005_output_eps_0.010.vnnlib";... % onnx loading error +]; + +% Run verification for cgan +for i=1:length(cgan_instances) + onnx = cgan_path + cgan_instances(i,1); + vnnlib = cgan_path + cgan_instances(i,2); + run_vnncomp2024_instance("cgan",onnx,vnnlib,"cgan_results_" + string(i)+".txt"); +end + + +%% tllverify + +disp("Running tllverify..") + +tll_path = vnncomp_path + "tllverifybench/"; + +tll_instances = ["onnx/tllBench_n=2_N=M=8_m=1_instance_0_0.onnx","vnnlib/property_N=8_0.vnnlib";... + "onnx/tllBench_n=2_N=M=16_m=1_instance_1_0.onnx","vnnlib/property_N=16_0.vnnlib";... + "onnx/tllBench_n=2_N=M=24_m=1_instance_2_2.onnx","vnnlib/property_N=24_2.vnnlib";... + "onnx/tllBench_n=2_N=M=32_m=1_instance_3_0.onnx","vnnlib/property_N=32_0.vnnlib";... + "onnx/tllBench_n=2_N=M=48_m=1_instance_5_3.onnx","vnnlib/property_N=48_3.vnnlib";... + "onnx/tllBench_n=2_N=M=56_m=1_instance_6_0.onnx","vnnlib/property_N=56_0.vnnlib";... + % "onnx/tllBench_n=2_N=M=64_m=1_instance_7_0.onnx","vnnlib/property_N=64_0.vnnlib";... + ]; % last one not finishing after a loooong time + +% Run verification for tllverify +for i=1:length(tll_instances) + onnx = tll_path + tll_instances(i,1); + vnnlib = tll_path + tll_instances(i,2); + run_vnncomp2024_instance("tllverifybench",onnx,vnnlib,"tllverify_results_" + string(i)+".txt"); +end + +%% metaroom + +disp("Running metaroom..") + +metaroom_path = vnncomp_path + "metaroom/"; + +% We can probably do exact analysis from the beginning on all instances here +metaroom_instances = ["onnx/6cnn_ry_20_3_no_custom_OP.onnx", "vnnlib/spec_idx_109_eps_0.00000436.vnnlib";... + "onnx/4cnn_ry_117_19_no_custom_OP.onnx", "vnnlib/spec_idx_3_eps_0.00000436.vnnlib";... + "onnx/6cnn_ry_65_10_no_custom_OP.onnx", "vnnlib/spec_idx_133_eps_0.00000436.vnnlib";... + "onnx/6cnn_ry_104_17_no_custom_OP.onnx", "vnnlib/spec_idx_96_eps_0.00000436.vnnlib";... + "onnx/6cnn_ry_94_15_no_custom_OP.onnx", "vnnlib/spec_idx_149_eps_0.00000436.vnnlib";... + "onnx/4cnn_ry_19_3_no_custom_OP.onnx", "vnnlib/spec_idx_5_eps_0.00000436.vnnlib";... + ]; + +% Run verification for metaroom +for i=1:length(metaroom_instances) + onnx = metaroom_path + metaroom_instances(i,1); + vnnlib = metaroom_path + metaroom_instances(i,2); + run_vnncomp2024_instance("metaroom",onnx,vnnlib,"metaroom_results_" + string(i)+".txt"); +end + + +%% safeNLP + +disp("Running safeNLP..") + +safeNLP_path = "C:/Users/diego/Documents/Research/vnncomp2024/safeNLP/"; + +% All are unsat in about a second, we can prob do exact on all as well + +% We can probably do exact analysis from the beginning on all instances here +safeNLP_instances = ["onnx/ruarobot.onnx", "vnnlib/ruarobot/prop_8_perturbations.vnnlib";... + "onnx/ruarobot.onnx", "vnnlib/ruarobot/prop_1239_perturbations.vnnlib";... + "onnx/ruarobot.onnx", "vnnlib/ruarobot/prop_6012_perturbations.vnnlib";... + "onnx/medical.onnx", "vnnlib/medical/prop_0_perturbations.vnnlib";... + "onnx/medical.onnx", "vnnlib/medical/prop_5_perturbations.vnnlib";... + "onnx/medical.onnx", "vnnlib/medical/prop_53_perturbations.vnnlib";... + ]; + +% Run verification for safeNLP +for i=1:length(safeNLP_instances) + onnx = safeNLP_path + safeNLP_instances(i,1); + vnnlib = safeNLP_path + safeNLP_instances(i,2); + run_vnncomp2024_instance("safeNLP",onnx,vnnlib,"safeNLP_results_" + string(i)+".txt"); +end + + +%% Cora + +disp("Running Cora benchmark..") + +cora_path = "C:/Users/diego/Documents/Research/vnncomp2024/cora-vnncomp2024-benchmark/"; + +% Some sat, most unsat, fairly fast using exact, can go with that as well +% Some unknowns... How is this possible with exact analysis? + +% We can probably do exact analysis from the beginning on all instances here +cora_instances = ["nns/mnist-point.onnx", "benchmark-files/mnist-img0.vnnlib";... + "nns/mnist-trades.onnx", "benchmark-files/mnist-img1.vnnlib";... + "nns/mnist-set.onnx", "benchmark-files/mnist-img20.vnnlib";... + "nns/svhn-point.onnx", "benchmark-files/svhn-img140.vnnlib";... + "nns/svhn-set.onnx", "benchmark-files/svhn-img323.vnnlib";... + "nns/svhn-trades.onnx", "benchmark-files/svhn-img472.vnnlib";... + "nns/cifar10-set.onnx", "benchmark-files/cifar10-img347.vnnlib";... + "nns/cifar10-point.onnx", "benchmark-files/cifar10-img353.vnnlib";... + "nns/cifar10-trades.onnx", "benchmark-files/cifar10-img266.vnnlib"... + ]; + +% Run verification for safeNLP +for i=1:length(cora_instances) + onnx = cora_path + cora_instances(i,1); + vnnlib = cora_path + cora_instances(i,2); + run_vnncomp2024_instance("cora",onnx,vnnlib,"cora_results_" + string(i)+".txt"); +end + + +%% Cifar100 + +disp("Running Cifar-100..") + +cifar100_path = "C:/Users/diego/Documents/Research/vnncomp2024/vnncomp2024-cifar100_benchmark/"; + +% no vnnlib properties provided in this year's repo +cifar100_instances = ["onnx/CIFAR100_resnet_medium.onnx", ""; ... + "onnx/CIFAR100_resnet_large.onnx", "";... + ]; + +% Run verification for cifar100 +for i=1:length(cifar100_instances) + onnx = cifar100_path + cifar100_instances(i,1); + vnnlib = cifar100_path + cifar100_instances(i,2); + run_vnncomp2024_instance("cifar100",onnx,vnnlib,"cifar100_results_" + string(i)+".txt"); +end + + +%% tinyimagenet + +disp("Running tinyimagenet..") + +tinyimagenet_path = "C:/Users/diego/Documents/Research/vnncomp2024/vnncomp2024-cifar100_benchmark/"; + +% no vnnlib properties provided in this year's repo +% (Some may be available in 2022 repo) +tinyimagenet_instances = ["onnx/TinyImageNet_resnet_medium.onnx", ""; ... + ]; + +% Run verification for tinyimagenet +for i=1:length(tinyimagenet_instances) + onnx = tinyimagenet_path + tinyimagenet_instances(i,1); + vnnlib = tinyimagenet_path + tinyimagenet_instances(i,2); + run_vnncomp2024_instance("tinyimagenet",onnx,vnnlib,"tinyimagenet_results_" + string(i)+".txt"); +end + +%% TODO +% Add benchmarks from 2024 +% update nn4sys and dist_shift as they have been updated \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/LSNC_VNNCOMP2024/load_networks.m b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/LSNC_VNNCOMP2024/load_networks.m new file mode 100644 index 000000000..cf2c4d3ce --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/LSNC_VNNCOMP2024/load_networks.m @@ -0,0 +1,18 @@ +% Load LSNC benchmarks + +netPath = "onnx/"; + +nns = dir(netPath); + +for i=1:length(nns) + if endsWith(nns(i).name, ".onnx") + disp(nns(i).name); + onnxNet = importNetworkFromONNX(netPath + nns(i).name, "InputDataFormats","BC", "OutputDataFormats","BC"); + end +end + +% We get these warnings... Not great, probably customized part of the +% network function during training +% Warning: The ONNX file uses IR version 8, while the highest fully-supported IR is version 7. +% Warning: The ONNX file uses Opset version 16, while the fully-supported version is 6~14. The imported network may differ from the ONNX +% network. \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/LSNC_VNNCOMP2024/readme.md b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/LSNC_VNNCOMP2024/readme.md new file mode 100644 index 000000000..379e48a57 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/LSNC_VNNCOMP2024/readme.md @@ -0,0 +1 @@ +https://github.com/shizhouxing/LSNC_VNNCOMP2024 \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/LinearizeNN_benchmark2024/load_networks.m b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/LinearizeNN_benchmark2024/load_networks.m new file mode 100644 index 000000000..809e30e56 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/LinearizeNN_benchmark2024/load_networks.m @@ -0,0 +1,7 @@ +% Load LinearizeNN benchmarks + +netPath = "onnx/AllInOne.onnx"; + +onnxNet = importNetworkFromONNX(netPath, "InputDataFormats","BC", "OutputDataFormats","BC"); + +% All good as well, only one network here \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/LinearizeNN_benchmark2024/readme.md b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/LinearizeNN_benchmark2024/readme.md new file mode 100644 index 000000000..f4027567d --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/LinearizeNN_benchmark2024/readme.md @@ -0,0 +1 @@ +https://github.com/aliabigdeli/LinearizeNN_benchmark2024 \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/cora-vnncomp2024-benchmark/load_networks.m b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/cora-vnncomp2024-benchmark/load_networks.m new file mode 100644 index 000000000..0d602e1b0 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/cora-vnncomp2024-benchmark/load_networks.m @@ -0,0 +1,14 @@ +% Load CORA benchmarks + +netPath = "nns/"; + +nns = dir(netPath); + +for i=1:length(nns) + if endsWith(nns(i).name, ".onnx") + disp(nns(i).name); + onnxNet = importNetworkFromONNX(netPath + nns(i).name, "InputDataFormats","BC", "OutputDataFormats","BC"); + end +end + +% All good, simple as expected \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/cora-vnncomp2024-benchmark/readme.md b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/cora-vnncomp2024-benchmark/readme.md new file mode 100644 index 000000000..190dc253c --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/cora-vnncomp2024-benchmark/readme.md @@ -0,0 +1 @@ +https://github.com/kollerlukas/cora-vnncomp2024-benchmark \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/ml4acopf_benchmark/README.md b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/ml4acopf_benchmark/README.md new file mode 100644 index 000000000..89fb41f63 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/ml4acopf_benchmark/README.md @@ -0,0 +1 @@ +https://github.com/AI4OPT/ml4acopf_benchmark \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/ml4acopf_benchmark/load_networks.m b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/ml4acopf_benchmark/load_networks.m new file mode 100644 index 000000000..6dd318030 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/ml4acopf_benchmark/load_networks.m @@ -0,0 +1,14 @@ +% Load ml4acopf benchmarks + +netPath = "onnx/"; + +nns = dir(netPath); + +for i=1:length(nns) + if endsWith(nns(i).name, ".onnx") + disp(nns(i).name); + onnxNet = importNetworkFromONNX(netPath + nns(i).name, "InputDataFormats","BC", "OutputDataFormats","BC"); + end +end + +% All networks are loaded, no problem here \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/safeNLP/README.md b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/safeNLP/README.md new file mode 100644 index 000000000..7e848784d --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/safeNLP/README.md @@ -0,0 +1 @@ +https://github.com/ANTONIONLP/safeNLP \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/safeNLP/load_networks.m b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/safeNLP/load_networks.m new file mode 100644 index 000000000..2aff97026 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/safeNLP/load_networks.m @@ -0,0 +1,14 @@ +% Load safeNLP benchmarks + +netPath = "onnx/"; + +nns = dir(netPath); + +for i=1:length(nns) + if endsWith(nns(i).name, ".onnx") + disp(nns(i).name); + onnxNet = importNetworkFromONNX(netPath + nns(i).name, "InputDataFormats","BC", "OutputDataFormats","BC"); + end +end + +% Networks seem very simple... Are we missing something? \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp-benchmark-generation-dynaroars/README.md b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp-benchmark-generation-dynaroars/README.md new file mode 100644 index 000000000..dff9c1703 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp-benchmark-generation-dynaroars/README.md @@ -0,0 +1 @@ +https://github.com/dynaroars/vnncomp-benchmark-generation \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp-benchmark-generation-dynaroars/load_networks.m b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp-benchmark-generation-dynaroars/load_networks.m new file mode 100644 index 000000000..a8d0d05a2 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp-benchmark-generation-dynaroars/load_networks.m @@ -0,0 +1,14 @@ +% Load dynaroars benchmarks + +netPath = "networks/"; + +nns = dir(netPath); + +for i=1:length(nns) + if endsWith(nns(i).name, ".onnx") + disp(nns(i).name); + onnxNet = importNetworkFromONNX(netPath + nns(i).name, "InputDataFormats","BCSS", "OutputDataFormats","BC"); + end +end + +% All networks are loaded, no problem here \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2023_collins/README.md b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2023_collins/README.md new file mode 100644 index 000000000..84bad156e --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2023_collins/README.md @@ -0,0 +1 @@ +https://github.com/loonwerks/vnncomp2023 \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2023_collins/load_networks.m b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2023_collins/load_networks.m new file mode 100644 index 000000000..9cb707eb0 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2023_collins/load_networks.m @@ -0,0 +1,20 @@ +% Load Collins benchmarks + +netPath = "onnx/"; + +nns = dir(netPath); + +for i=1:length(nns) + if endsWith(nns(i).name, ".onnx") + disp(nns(i).name); + onnxNet = importNetworkFromONNX(netPath + nns(i).name, "InputDataFormats","BCSS", "OutputDataFormats","BCT"); + end +end + +% 1) OutputDataFormats (empty, or BCT) +% Probably not, we can skip this one. 3 reshape to reshape layers, not +% standard, lots of parameters in these custom layers... +% Could be accomplished with some manual conversion for these... +% 2) OutputDataFormats (TBC) +% Only generated 1 custom layer (reshape_to_concat), this may be doable +% But still looks like a very challenging benchmark \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2024_cifar100_benchmark/README.md b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2024_cifar100_benchmark/README.md new file mode 100644 index 000000000..6461082c1 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2024_cifar100_benchmark/README.md @@ -0,0 +1 @@ +https://github.com/huanzhang12/vnncomp2024_cifar100_benchmark \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2024_cifar100_benchmark/load_networks.m b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2024_cifar100_benchmark/load_networks.m new file mode 100644 index 000000000..7a3ed3737 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2024_cifar100_benchmark/load_networks.m @@ -0,0 +1,14 @@ +% Load cifar100 benchmarks + +netPath = "onnx/"; + +nns = dir(netPath); + +for i=1:length(nns) + if endsWith(nns(i).name, ".onnx") + disp(nns(i).name); + onnxNet = importNetworkFromONNX(netPath + nns(i).name, "InputDataFormats","BCSS", "OutputDataFormats","BC"); + end +end + +% Both networks seem fine \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2024_tinyimagenet_benchmark/README.md b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2024_tinyimagenet_benchmark/README.md new file mode 100644 index 000000000..0fb643cee --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2024_tinyimagenet_benchmark/README.md @@ -0,0 +1 @@ +https://github.com/huanzhang12/vnncomp2024_tinyimagenet_benchmark \ No newline at end of file diff --git a/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2024_tinyimagenet_benchmark/load_networks.m b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2024_tinyimagenet_benchmark/load_networks.m new file mode 100644 index 000000000..ab0b81845 --- /dev/null +++ b/code/nnv/examples/Submission/VNN_COMP2024/vnncomp2024/vnncomp2024_tinyimagenet_benchmark/load_networks.m @@ -0,0 +1,14 @@ +% Load tinyImagenet benchmarks + +netPath = "onnx/"; + +nns = dir(netPath); + +for i=1:length(nns) + if endsWith(nns(i).name, ".onnx") + disp(nns(i).name); + onnxNet = importNetworkFromONNX(netPath + nns(i).name, "InputDataFormats","BCSS", "OutputDataFormats","BC"); + end +end + +% One network only, it also seems fine \ No newline at end of file