From 5405b1f04e3ed84ccc58edcd5ea519bd708750a8 Mon Sep 17 00:00:00 2001 From: Diego Manzanas Date: Mon, 15 Jul 2024 23:32:37 -0500 Subject: [PATCH 1/4] Working on counterexamples for exact reachability --- .../examples/NN/FairNNV/adult_exact_verify.m | 24 +++++++----- code/nnv/examples/NN/FairNNV/adult_verifiy.m | 11 +++--- .../examples/NN/FairNNV/getCounterRegion.m | 38 +++++++++++++++++++ 3 files changed, 59 insertions(+), 14 deletions(-) create mode 100644 code/nnv/examples/NN/FairNNV/getCounterRegion.m diff --git a/code/nnv/examples/NN/FairNNV/adult_exact_verify.m b/code/nnv/examples/NN/FairNNV/adult_exact_verify.m index c7838bbb2..15590f10c 100644 --- a/code/nnv/examples/NN/FairNNV/adult_exact_verify.m +++ b/code/nnv/examples/NN/FairNNV/adult_exact_verify.m @@ -12,6 +12,7 @@ clear; clc; modelDir = './adult_onnx'; % Directory containing ONNX models onnxFiles = dir(fullfile(modelDir, '*.onnx')); % List all .onnx files +onnxFiles = onnxFiles(1); % simplify for debugging load("adult_data.mat", 'X', 'y'); % Load data once @@ -58,12 +59,12 @@ % First, we define the reachability options reachOptions = struct; % initialize reachOptions.reachMethod = 'exact-star'; - reachOptions.relaxFactor = 0.5; nR = 50; % ---> just chosen arbitrarily % ADJUST epsilons value here - epsilon = [0.0,0.001,0.01]; + % epsilon = [0.001,0.01]; + epsilon = 0.01; % Set up results nE = 3; @@ -87,19 +88,23 @@ start(verificationTimer); % Start the timer - for i=1:numObs + % for i=1:numObs + for i=57 idx = rand_indices(i); IS = perturbationIF(X_test_loaded(:, idx), epsilon(e), min_values, max_values); - + + unsafeRegion = net.robustness_set(y_test_loaded(idx), 'min'); t = tic; % Start timing the verification for each sample - temp = net.verify_robustness(IS, reachOptions, y_test_loaded(idx)); + temp = net.verify_robustness(IS, reachOptions, unsafeRegion); met(i,e) = 'exact'; - res(i,e) = temp; % robust result - % end - + res(i,e) = temp; % robust result time(i,e) = toc(t); % store computation time + + if ~(temp == 1) + counterExs = getCounterRegion(IS,unsafeRegion,net.reachSet{end}); + end % Check for timeout flag if evalin('base', 'timeoutOccurred') @@ -164,6 +169,7 @@ % Calculate disturbed lower and upper bounds considering min and max values lb = max(x - disturbance, min_values); ub = min(x + disturbance, max_values); - IS = ImageStar(single(lb), single(ub)); % default: single (assume onnx input models) + IS = Star(single(lb), single(ub)); % default: single (assume onnx input models) + end diff --git a/code/nnv/examples/NN/FairNNV/adult_verifiy.m b/code/nnv/examples/NN/FairNNV/adult_verifiy.m index d093f7b7a..845fcfdf9 100644 --- a/code/nnv/examples/NN/FairNNV/adult_verifiy.m +++ b/code/nnv/examples/NN/FairNNV/adult_verifiy.m @@ -64,7 +64,7 @@ nR = 50; % ---> just chosen arbitrarily % ADJUST epsilon values here - epsilon = [0.0,0.001,0.01]; + epsilon = [0.001,0.01]; % Set up results @@ -90,7 +90,7 @@ start(verificationTimer); % Start the timer % Iterate through observations - for i=1:numObs + for i=38 idx = rand_indices(i); [IS, xRand] = perturbationIF(X_test_loaded(:, idx), epsilon(e), nR, min_values, max_values); @@ -109,6 +109,7 @@ time(i,e) = toc(t); met(i,e) = "counterexample"; skipTryCatch = true; % Set the flag to skip try-catch block + disp('Counter example found'); continue; end end @@ -198,7 +199,7 @@ % Calculate disturbed lower and upper bounds considering min and max values lb = max(x - disturbance, min_values); ub = min(x + disturbance, max_values); - IS = ImageStar(single(lb), single(ub)); % default: single (assume onnx input models) + IS = Star(single(lb), single(ub)); % default: single (assume onnx input models) % Create random samples from initial set % Adjusted reshaping according to specific needs @@ -208,7 +209,7 @@ xRand = xB.sample(nR); xRand = reshape(xRand,[13,nR]); xRand(:,nR+1) = x; % add original image - xRand(:,nR+2) = IS.im_lb; % add lower bound image - xRand(:,nR+3) = IS.im_ub; % add upper bound image + xRand(:,nR+2) = xB.lb; % add lower bound image + xRand(:,nR+3) = xB.ub; % add upper bound image end diff --git a/code/nnv/examples/NN/FairNNV/getCounterRegion.m b/code/nnv/examples/NN/FairNNV/getCounterRegion.m new file mode 100644 index 000000000..40b8206a4 --- /dev/null +++ b/code/nnv/examples/NN/FairNNV/getCounterRegion.m @@ -0,0 +1,38 @@ +function counterExamples = getCounterRegion(inputSet, unsafeRegion, reachSet) + % counterExamples = getCounterRegion(inputSet, unsafeRegion, reachSet) + % NOTE: This is only to be used with exact-star method + % unsafeRegion = HalfSpace (unsafe/undesired region) + % inputSet = ImageStar/Star + % reachSet = Star + % + % check the "safety" of the reachSet + % Then, generate counterexamples + + % Initialize variables + counterExamples = []; + + % Get halfspace variables + G = unsafeRegion.G; + g = unsafeRegion.g; + + % Check for valid inputs + if ~isa(inputSet, "Star") + error("Must be a Star"); + end + if ~isa(reachSet, "Star") + error("Must be Star or ImageStar"); + end + + % Begin counterexample computation + n = length(reachSet); % number of stars in the output set + V = inputSet.V; + for i=1:n + % Check for safety, if unsafe, add to counter + if ~isempty(reachSet(i).intersectHalfSpace(G, g)) + counterExamples = [counterExamples Star(V, reachSet(i).C, reachSet(i).d,... + reachSet(i).predicate_lb, reachSet(i).predicate_ub)]; + end + end + +end + From b0f7933f646274fc53ab62dc98ef84a932238b89 Mon Sep 17 00:00:00 2001 From: Diego Manzanas Date: Wed, 24 Jul 2024 09:01:46 -0500 Subject: [PATCH 2/4] Delete unused files --- .../VNN_COMP2024/results_approx_tinyimagenet/instance_1.txt | 1 - 1 file changed, 1 deletion(-) delete mode 100644 code/nnv/examples/Submission/VNN_COMP2024/results_approx_tinyimagenet/instance_1.txt diff --git a/code/nnv/examples/Submission/VNN_COMP2024/results_approx_tinyimagenet/instance_1.txt b/code/nnv/examples/Submission/VNN_COMP2024/results_approx_tinyimagenet/instance_1.txt deleted file mode 100644 index c0804f6cc..000000000 --- a/code/nnv/examples/Submission/VNN_COMP2024/results_approx_tinyimagenet/instance_1.txt +++ /dev/null @@ -1 +0,0 @@ -Operands to the logical AND (&&) and OR (||) operators must be convertible to logical scalar values. Use the ANY or ALL functions to reduce operands to logical scalar values. From f06303b306fbedfb351220e59ce874a6841e063c Mon Sep 17 00:00:00 2001 From: Diego Manzanas Date: Fri, 26 Jul 2024 13:30:40 -0500 Subject: [PATCH 3/4] Speed up computations, new method for reduced RAM needs --- code/nnv/engine/nn/funcs/PosLin.m | 3 ++ .../nnv/engine/nn/layers/ConcatenationLayer.m | 8 +++-- code/nnv/engine/nn/layers/ReluLayer.m | 34 ++++++++++++++++++- code/nnv/engine/set/ImageStar.m | 30 +++++----------- 4 files changed, 50 insertions(+), 25 deletions(-) diff --git a/code/nnv/engine/nn/funcs/PosLin.m b/code/nnv/engine/nn/funcs/PosLin.m index ca6136826..70fb06a43 100644 --- a/code/nnv/engine/nn/funcs/PosLin.m +++ b/code/nnv/engine/nn/funcs/PosLin.m @@ -2073,6 +2073,9 @@ R = PosLin.reach_star_approx2(I, option, dis_opt, lp_solver); elseif strcmp(method, 'relax-star-range') R = PosLin.reach_relaxed_star_range(I, relaxFactor, option, dis_opt, lp_solver); + if contains(method, 'reduceMem') + R = R.reduceConstraints; + end elseif strcmp(method, 'relax-star-bound') R = PosLin.reach_relaxed_star_bound(I, relaxFactor, option, dis_opt, lp_solver); elseif strcmp(method, 'relax-star-area') diff --git a/code/nnv/engine/nn/layers/ConcatenationLayer.m b/code/nnv/engine/nn/layers/ConcatenationLayer.m index d6ea69c95..4576f88e8 100644 --- a/code/nnv/engine/nn/layers/ConcatenationLayer.m +++ b/code/nnv/engine/nn/layers/ConcatenationLayer.m @@ -107,9 +107,11 @@ % Get max size of V vSize = size(inputs{1}.V); + indexMax = 1; for i = 2:length(inputs) - if numel(size(inputs{i}.V)) > numel(vSize) - vSize = inputs{i}.V; + if numel(inputs{i}.V) > prod(vSize) + vSize = size(inputs{i}.V); + indexMax = i; end end @@ -125,7 +127,7 @@ end % Create output set - outputs = ImageStar(new_V, inputs{1}.C, inputs{1}.d, inputs{1}.pred_lb, inputs{1}.pred_ub); + outputs = ImageStar(new_V, inputs{indexMax}.C, inputs{indexMax}.d, inputs{indexMax}.pred_lb, inputs{indexMax}.pred_ub); end % handle multiple inputs diff --git a/code/nnv/engine/nn/layers/ReluLayer.m b/code/nnv/engine/nn/layers/ReluLayer.m index 380f2ca7f..fb4d53580 100644 --- a/code/nnv/engine/nn/layers/ReluLayer.m +++ b/code/nnv/engine/nn/layers/ReluLayer.m @@ -104,13 +104,45 @@ h = in_image.height; w = in_image.width; c = in_image.numChannel; - + reduceMem = 0; + if contains(method, "reduceMem") + method = split(method, '-'); + method = strjoin(method(1:end-1),'-'); + reduceMem = 1; + end Y = PosLin.reach(in_image.toStar, method, [], relaxFactor, dis_opt, lp_solver); % reachable set computation with ReLU n = length(Y); images(n) = ImageStar; % transform back to ImageStar for i=1:n images(i) = Y(i).toImageStar(h,w,c); + if reduceMem + [l,u] = images(i).estimateRanges; + % Get dimensions + h = images(i).height; + w = images(i).width; + c = images(i).numChannel; + % create ImageStar variables + center = cast(0.5*(u+l), 'like', in_image.V); + v = 0.5*(u-l); + idxRegion = find((l-u)); + n = length(idxRegion); + V = zeros(h, w, c, n, 'like', center); + bCount = 1; + for i1 = 1:size(v,1) + for i2 = 1:size(v,2) + basisValue = v(i1,i2); + if basisValue + V(i1,i2,:,bCount) = v(i1,i2); + bCount = bCount + 1; + end + end + end + C = zeros(1, n, 'like', V); + d = zeros(1, 1, 'like', V); + % Construct ImageStar + images(i) = ImageStar(cat(4,center,V), C, d, -1*ones(n,1), ones(n,1), l, u); + end end else % star images = PosLin.reach(in_image, method, [], relaxFactor, dis_opt, lp_solver); % reachable set computation with ReLU diff --git a/code/nnv/engine/set/ImageStar.m b/code/nnv/engine/set/ImageStar.m index 63374727e..020bf56bc 100644 --- a/code/nnv/engine/set/ImageStar.m +++ b/code/nnv/engine/set/ImageStar.m @@ -847,30 +847,18 @@ end if isempty(obj.C) || isempty(obj.d) - error('The imagestar is empty'); + warning('The imagestar is empty'); + % no ranges, so bounds are the same as image + obj.im_lb = obj.V; + obj.im_ub = obj.V; end if isempty(obj.im_lb) || isempty(obj.im_ub) - image_lb = zeros(obj.height, obj.width, obj.numChannel); - image_ub = zeros(obj.height, obj.width, obj.numChannel); - reverseStr = ''; - N = obj.height*obj.width*obj.numChannel; - if strcmp(dis_opt, 'display') - fprintf('\nEstimating Range: '); - end - for i=1:obj.height - for j=1:obj.width - for k=1:obj.numChannel - [image_lb(i, j, k), image_ub(i, j, k)] = obj.estimateRange(i,j,k); - if strcmp(dis_opt, 'display') - msg = sprintf('%d/%d', i*j*k, N); - fprintf([reverseStr, msg]); - reverseStr = repmat(sprintf('\b'), 1, length(msg)); - end - end - end - end + x1 = obj.V(:,:,:,1) + tensorprod(obj.V(:,:,:,2:end), obj.pred_lb, 4, 1); + x2 = obj.V(:,:,:,1) + tensorprod(obj.V(:,:,:,2:end), obj.pred_ub, 4, 1); + image_lb = min(x1,x2); + image_ub = max(x1,x2); obj.im_lb = image_lb; obj.im_ub = image_ub; @@ -1523,7 +1511,7 @@ function addInputSize(obj, name, inputSize) new_d = [in_IS.d; new_d]; end - + end From e1d003f2d2a1296cee40cc39afb0cc179851b195 Mon Sep 17 00:00:00 2001 From: Diego Manzanas Date: Mon, 5 Aug 2024 09:56:23 -0500 Subject: [PATCH 4/4] Fix bug checkRobust --- code/nnv/engine/nn/NN.m | 2 +- code/nnv/engine/set/ImageStar.m | 24 +++++++++++++----------- 2 files changed, 14 insertions(+), 12 deletions(-) diff --git a/code/nnv/engine/nn/NN.m b/code/nnv/engine/nn/NN.m index a40891212..e79136353 100644 --- a/code/nnv/engine/nn/NN.m +++ b/code/nnv/engine/nn/NN.m @@ -369,7 +369,7 @@ nr = length(outputSet); R = Star; for s=1:nr - R = outputSet(s).toStar; + R(s) = outputSet(s).toStar; end else R = outputSet; diff --git a/code/nnv/engine/set/ImageStar.m b/code/nnv/engine/set/ImageStar.m index 020bf56bc..ec05645ec 100644 --- a/code/nnv/engine/set/ImageStar.m +++ b/code/nnv/engine/set/ImageStar.m @@ -511,17 +511,19 @@ end function image = recurrentMap(obj, h_t_1, inputWeight, recurrentWeight, bias) - n = obj.numPred; - N = obj.height*obj.width*obj.numChannel; - for i=1:n+1 - I = in_image.V(:,:,:,i); - %I = reshape(I,N,1); % flatten input - if i==1 - V(1, 1,:,i) = double(inputWeight)*I + double(recurrentWeight)*h_t_1 + double(bias); - else - V(1, 1,:,i) = double(inputWeight)*I; - end - end + % Whoever implemented this, did not use it as it would return an error + % n = obj.numPred; + % N = obj.height*obj.width*obj.numChannel; + % for i=1:n+1 + % I = in_image.V(:,:,:,i); + % %I = reshape(I,N,1); % flatten input + % if i==1 + % V(1, 1,:,i) = double(inputWeight)*I + double(recurrentWeight)*h_t_1 + double(bias); + % else + % V(1, 1,:,i) = double(inputWeight)*I; + % end + % end + error("Not supported yet."); end function image = HadamardProduct(obj, I)