From d75dfde1694f8eebb8dff067b61139e3d9957255 Mon Sep 17 00:00:00 2001 From: Diego Manzanas Date: Thu, 11 Jan 2024 18:14:19 -0600 Subject: [PATCH] Fix precision error on CAV23, add tests and other small fixes --- code/nnv/engine/nn/NN.m | 23 +++- code/nnv/engine/set/ImageStar.m | 24 ++++ code/nnv/engine/set/ImageZono.m | 17 ++- code/nnv/engine/set/Star.m | 34 ++++- code/nnv/engine/set/VolumeStar.m | 25 +++- code/nnv/engine/set/Zono.m | 14 ++ code/nnv/engine/utils/load_vnnlib.m | 14 +- .../Tutorial/other/set_representations.m | 5 +- .../layers/Conv2DLayer/test_layers_Conv2D.m | 122 +++++++++++------- code/nnv/tests/set/star/test_star_getZono.m | 1 + .../tests/set/star/test_star_plotBoxes_3D.m | 1 + 11 files changed, 219 insertions(+), 61 deletions(-) diff --git a/code/nnv/engine/nn/NN.m b/code/nnv/engine/nn/NN.m index b7f10d78ba..5e2977d6aa 100644 --- a/code/nnv/engine/nn/NN.m +++ b/code/nnv/engine/nn/NN.m @@ -237,13 +237,15 @@ if strcmp(obj.dis_opt, 'display') fprintf('\nPerform reachability analysis for the network %s \n', obj.Name); end + + % ensure NN parameters and input set share same precision + inputSet = obj.consistentPrecision(inputSet); % change only input, this can be changed in the future % Perform reachability based on connections or assume no skip/sparse connections if isempty(obj.Connections) outputSet = obj.reach_noConns(inputSet); else outputSet = obj.reach_withConns(inputSet); - end end @@ -945,6 +947,25 @@ reachOptions.numCores = 1; end end + + % Ensure input and parameter precision is the same + function inputSet = consistentPrecision(obj, inputSet) + % (assume parameters have same precision across layers) + % approach: change input precision based on network parameters + inputPrecision = class(inputSet.V); + netPrecision = 'double'; % default + for i=1:length(obj.Layers) + if isa(obj.Layers{i}, "FullyConnectedLayer") || isa(obj.Layers{i}, "Conv2DLayer") + netPrecision = class(obj.Layers{i}.Weights); + break; + end + end + if ~strcmp(inputPrecision, netPrecision) + % input and parameter precision does not match + warning("Changing input set precision to "+string(netPrecision)); + inputSet = inputSet.changeVarsPrecision(netPrecision); + end + end % Create input set based on input vector and bounds function R = create_input_set(obj, x_in, disturbance, lb_allowable, ub_allowable) % assume tol is applied to every vale of the input diff --git a/code/nnv/engine/set/ImageStar.m b/code/nnv/engine/set/ImageStar.m index 46f130373a..44bed518ad 100644 --- a/code/nnv/engine/set/ImageStar.m +++ b/code/nnv/engine/set/ImageStar.m @@ -656,6 +656,30 @@ end + % change variable precision + function S = changeVarsPrecision(obj, precision) + S = obj; + if strcmp(precision, 'single') + S.V = single(S.V); + S.C = single(S.C); + S.d = single(S.d); + S.pred_lb = single(S.pred_lb); + S.pred_ub = single(S.pred_lb); + S.im_lb = single(S.im_lb); + S.im_ub = single(S.im_ub); + elseif strcmp(precision, 'double') + S.V = double(S.V); + S.C = double(S.C); + S.d = double(S.d); + S.pred_lb = double(S.pred_lb); + S.pred_ub = double(S.pred_lb); + S.im_lb = double(S.im_lb); + S.im_ub = double(S.im_ub); + else + error("Only single or double precision arrays allowed. GpuArray/dlarray are coming.") + end + end + end diff --git a/code/nnv/engine/set/ImageZono.m b/code/nnv/engine/set/ImageZono.m index a3ca88f01b..111bad7316 100644 --- a/code/nnv/engine/set/ImageZono.m +++ b/code/nnv/engine/set/ImageZono.m @@ -280,7 +280,22 @@ S = obj.toImageStar; S = S.toStar; end - + + % change variable precision + function S = changeVarsPrecision(obj, precision) + S = obj; + if strcmp(precision, 'single') + S.V = single(S.V); + S.lb_image = single(S.lb_image); + S.ub_image = single(S.ub_image); + elseif strcmp(precision, 'double') + S.V = double(S.V); + S.lb_image = double(S.lb_image); + S.ub_image = double(S.ub_image); + else + error("Only single or double precision arrays allowed. GpuArray/dlarray are coming.") + end + end end diff --git a/code/nnv/engine/set/Star.m b/code/nnv/engine/set/Star.m index bdc91248f1..f02941c02e 100644 --- a/code/nnv/engine/set/Star.m +++ b/code/nnv/engine/set/Star.m @@ -1448,6 +1448,30 @@ end + % change variable precision + function S = changeVarsPrecision(obj, precision) + S = obj; + if strcmp(precision, 'single') + S.V = single(S.V); + S.C = single(S.C); + S.d = single(S.d); + S.predicate_lb = single(S.predicate_lb); + S.predicate_ub = single(S.predicate_lb); + S.state_lb = single(S.state_lb); + S.state_ub = single(S.state_ub); + elseif strcmp(precision, 'double') + S.V = double(S.V); + S.C = double(S.C); + S.d = double(S.d); + S.predicate_lb = double(S.predicate_lb); + S.predicate_ub = double(S.predicate_lb); + S.state_lb = double(S.state_lb); + S.state_ub = double(S.state_ub); + else + error("Only single or double precision arrays allowed. GpuArray/dlarray are coming.") + end + end + end @@ -1526,8 +1550,14 @@ function plot(varargin) end end else - P = obj.toPolyhedron; - P.plot('color', color); + if isa(obj.V, 'single') || isa(obj.C,'single') || isa(obj.d, 'single') + S = obj.changeVarsPrecision('double'); + P = S.toPolyhedron; + P.plot('color', color); + else + P = obj.toPolyhedron; + P.plot('color', color); + end end else diff --git a/code/nnv/engine/set/VolumeStar.m b/code/nnv/engine/set/VolumeStar.m index db2a0d396b..bec37d75c2 100644 --- a/code/nnv/engine/set/VolumeStar.m +++ b/code/nnv/engine/set/VolumeStar.m @@ -523,7 +523,30 @@ end - % TODO: add a 3D projection to ImageStar + % change variable precision + function S = changeVarsPrecision(obj, precision) + S = obj; + if strcmp(precision, 'single') + S.V = single(S.V); + S.C = single(S.C); + S.d = single(S.d); + S.pred_lb = single(S.pred_lb); + S.pred_ub = single(S.pred_lb); + S.vol_lb = single(S.vol_lb); + S.vol_ub = single(S.vol_ub); + elseif strcmp(precision, 'double') + S.V = double(S.V); + S.C = double(S.C); + S.d = double(S.d); + S.pred_lb = double(S.pred_lb); + S.pred_ub = double(S.pred_lb); + S.vol_lb = double(S.vol_lb); + S.vol_ub = double(S.vol_ub); + else + error("Only single or double precision arrays allowed. GpuArray/dlarray are coming.") + end + end + end diff --git a/code/nnv/engine/set/Zono.m b/code/nnv/engine/set/Zono.m index 5745181d67..7970d0d19a 100644 --- a/code/nnv/engine/set/Zono.m +++ b/code/nnv/engine/set/Zono.m @@ -343,6 +343,20 @@ imageStar = im1.toImageStar(height, width, numChannels); end + + % change variable precision + function S = changeVarsPrecision(obj, precision) + S = obj; + if strcmp(precision, 'single') + S.V = single(S.V); + S.c = single(S.c); + elseif strcmp(precision, 'double') + S.V = double(S.V); + S.c = double(S.c); + else + error("Only single or double precision arrays allowed. GpuArray/dlarray are coming.") + end + end end diff --git a/code/nnv/engine/utils/load_vnnlib.m b/code/nnv/engine/utils/load_vnnlib.m index cb96228e7f..c850736151 100644 --- a/code/nnv/engine/utils/load_vnnlib.m +++ b/code/nnv/engine/utils/load_vnnlib.m @@ -35,8 +35,8 @@ dim = dim + 1; % only have seen inputs defined as vectors, so this should work % the more general approach would require some extra work, but should be easy as well elseif contains(tline, "declare-const") && contains(tline, "Y_") - lb_template = zeros(dim,1); - ub_template = zeros(dim,1); + lb_template = zeros(dim,1,'single'); + ub_template = zeros(dim,1,'single'); dim = 0; % reset dimension counter phase = "DeclareOutput"; continue; % redo this line in correct phase @@ -51,7 +51,7 @@ dim = 1; % reset dimension counter phase = "DefineInput"; % Initialize variables - lb_input = lb_template; + lb_input = lb_template; ub_input = ub_template; continue; % redo this line in correct phase end @@ -240,7 +240,7 @@ H(idx2) = -1; else var2 = split(var2, ')'); - g = str2double(var2{1}); + g = single(str2double(var2{1})); end else H(idx1) = -1; @@ -252,7 +252,7 @@ H(idx2) = 1; else var2 = split(var2, ')'); - g = -str2double(var2{1}); + g = -single(str2double(var2{1})); end end % Add constraint (H, g) to assertion variable (ast) @@ -346,7 +346,7 @@ dim = split(t{2},'_'); dim = str2double(dim{2})+1; value = split(t{3},')'); - value = str2double(value{1}); + value = single(str2double(value{1})); if contains(t{1},">=") lb_input(dim) = value; else @@ -401,7 +401,7 @@ dim = split(t{2},'_'); dim = str2double(dim{2})+1; value = split(t{3},')'); - value = str2double(value{1}); + value = single(str2double(value{1})); if contains(t{1},">=") || contains(t{1}, ">") Hvec(dim) = -1; gval = -value; diff --git a/code/nnv/examples/Tutorial/other/set_representations.m b/code/nnv/examples/Tutorial/other/set_representations.m index 78ad4d44d8..08b748fe08 100644 --- a/code/nnv/examples/Tutorial/other/set_representations.m +++ b/code/nnv/examples/Tutorial/other/set_representations.m @@ -64,11 +64,12 @@ S1 = S.affineMap([1 0 0 0 0; 0 1 0 0 0], []); % 2D, dims 1 and 2 figure; -Star.plot(S1); +Star.plotBoxes_2D(S1,1,2,'r'); +hold on; S3 = S.affineMap([1 0 0 0 0; 0 1 0 0 0; 0 0 1 0 0], []); % 3D, dims 1,2 and 3 figure; -Star.plot(S3); +Star.plotBoxes_3D(S3,1,2,3,'r'); % 2) Plot an overapproximation (box around Star) of the set and plot diff --git a/code/nnv/tests/nn/layers/Conv2DLayer/test_layers_Conv2D.m b/code/nnv/tests/nn/layers/Conv2DLayer/test_layers_Conv2D.m index 6e3712613b..3042dc4fb7 100644 --- a/code/nnv/tests/nn/layers/Conv2DLayer/test_layers_Conv2D.m +++ b/code/nnv/tests/nn/layers/Conv2DLayer/test_layers_Conv2D.m @@ -10,13 +10,9 @@ -%___________________________________________________________________________________________________ -%tests below originally taken from test_Conv2DLayer_compute_featureMap.m - %% test 1: Conv2DLayer feature map - I = [1 1 1 0 0; 0 1 1 1 0; 0 0 1 1 1; 0 0 1 1 0; 0 1 1 0 0]; % input W = [1 0 1; 0 1 0; 1 0 1]; % filter @@ -24,21 +20,13 @@ stride = [1 1]; dilation = [1 1]; - featureMap = Conv2DLayer.compute_featureMap(I, W, padding, stride, dilation); - checker=[I(1, 1)+I(1, 3)+I(2, 2)+I(3, 1)+I(3, 3), I(1, 2)+I(1, 4)+I(2, 3)+I(3, 2)+I(3, 4), I(1, 3)+I(1, 5)+I(2, 4)+I(3, 3)+I(3, 5); I(2, 1)+I(2, 3)+I(3, 2)+I(4, 1)+I(4, 3), I(2, 2)+I(2, 4)+I(3, 3)+I(4, 2)+I(4, 4), I(2, 3)+I(2, 5)+I(3, 4)+I(4, 3)+I(4, 5); I(3, 1)+I(3, 3)+I(4, 2)+I(5, 1)+I(5, 3), I(3, 2)+I(3, 4)+I(4, 3)+I(5, 2)+I(5, 4), I(3, 3)+I(3, 5)+I(4, 4)+I(5, 3)+I(5, 5);]; assert(isequal(checker, featureMap)) - - -%___________________________________________________________________________________________________ -%tests below originally taken from test_Conv2DLayer_constructor.m - - %% test 2: Conv2DLayer constructor @@ -50,6 +38,7 @@ W(:,:, 1, 1) = [1 1 1; 1 1 -1; 0 -1 0]; % channel 1 W(:, :, 2, 1) = [0 1 1; 0 -1 0; 0 0 -1]; % channel 2 W(:, :, 3, 1) = [1 -1 0; 1 1 0; -1 0 1]; % channel 3 + % filter 2 weight matrix with 3 channels W(:, :, 1, 2) = [1 1 -1; -1 0 1; 1 -1 -1]; % channel 1 W(:, :, 2, 2) = [-1 1 1; 0 1 1; 0 -1 1]; % channel 2 @@ -59,27 +48,17 @@ b(:, :, 1) = 1; % filter 1 b(:, :, 2) = 0; % filter 2 - L0 = Conv2DLayer(W, b); L1 = Conv2DLayer('Test_Cov2DLayer', W, b, [1 1 1 1], [1 1], [1 1]); - - -%___________________________________________________________________________________________________ -%tests below originally taken from test_Conv2DLayer_get_zero_padding_input.m - - %% test 3: Conv2DLayer zero padding - - % original input volume: color image with 3 channels inputVol(:, :, 1) = [2 0 1 2 1; 1 0 2 2 2; 1 2 2 0 2; 1 2 0 0 1; 1 0 1 1 2]; % channel 1 input matrix inputVol(:, :, 2) = [0 0 1 0 1; 0 0 2 1 1; 1 1 0 1 1; 1 1 0 2 2; 2 1 2 0 0]; % channel 2 input matrix inputVol(:, :, 3) = [1 2 2 1 0; 2 0 0 2 0; 0 0 1 0 1; 1 2 0 2 0; 1 0 2 1 0]; % channel 3 input matrix - % construct input with padding operation paddingSize = [1 1 1 1]; I = Conv2DLayer.get_zero_padding_input(inputVol, paddingSize); @@ -95,11 +74,6 @@ assert(isempty(find(left_right))) - -%___________________________________________________________________________________________________ -%tests below originally taken from test_Conv2DLayer_reach.m - - %% test 4: Conv2DLayer reach % construct a Conv2DLayer object @@ -110,6 +84,7 @@ W(:,:, 1, 1) = [1 1 1; 1 1 -1; 0 -1 0]; % channel 1 W(:, :, 2, 1) = [0 1 1; 0 -1 0; 0 0 -1]; % channel 2 W(:, :, 3, 1) = [1 -1 0; 1 1 0; -1 0 1]; % channel 3 + % filter 2 weight matrix with 3 channels W(:, :, 1, 2) = [1 1 -1; -1 0 1; 1 -1 -1]; % channel 1 W(:, :, 2, 2) = [-1 1 1; 0 1 1; 0 -1 1]; % channel 2 @@ -119,7 +94,6 @@ b(:, :, 1) = 1; % filter 1 b(:, :, 2) = 0; % filter 2 - L0 = Conv2DLayer(W, b); LB(:,:,1) = [-0.1 -0.2 0 0; 0 0 0 0; 0 0 0 0; 0 0 0 0]; % attack on pixel (1,1) and (1,2) @@ -130,21 +104,49 @@ UB(:,:,2) = [0.1 0.15 0 0; 0 0 0 0; 0 0 0 0; 0 0 0 0]; UB(:,:,3) = UB(:,:,2); -image = ImageZono(LB, UB); +image = ImageStar(LB, UB); + +L0.reach(image); + +%% %% test 4b: Conv2DLayer reach (single precision) -%Z = L0.reach(image); %THIS TRIGGERS AN ERROR, BECAUSE IT'S NOT AN IMAGE +% construct a Conv2DLayer object +% this convolution layer is from the link: +% http://cs231n.github.io/convolutional-networks/ + +% filter 1 weight matrix with 3 channels +W(:,:, 1, 1) = [1 1 1; 1 1 -1; 0 -1 0]; % channel 1 +W(:, :, 2, 1) = [0 1 1; 0 -1 0; 0 0 -1]; % channel 2 +W(:, :, 3, 1) = [1 -1 0; 1 1 0; -1 0 1]; % channel 3 + +% filter 2 weight matrix with 3 channels +W(:, :, 1, 2) = [1 1 -1; -1 0 1; 1 -1 -1]; % channel 1 +W(:, :, 2, 2) = [-1 1 1; 0 1 1; 0 -1 1]; % channel 2 +W(:, :, 3, 2) = [-1 1 -1; -1 0 -1; -1 -1 -1]; % channel 3 + +% biases for 2 filters +b(:, :, 1) = 1; % filter 1 +b(:, :, 2) = 0; % filter 2 -S = L0.reach(image.toImageStar); +L0 = Conv2DLayer(single(W), single(b)); +LB(:,:,1) = [-0.1 -0.2 0 0; 0 0 0 0; 0 0 0 0; 0 0 0 0]; % attack on pixel (1,1) and (1,2) +LB(:,:,2) = [-0.1 -0.15 0 0; 0 0 0 0; 0 0 0 0; 0 0 0 0]; +LB(:,:,3) = LB(:,:,2); +UB(:,:,1) = [0 0.2 0 0; 0 0 0 0; 0 0 0 0; 0 0 0 0]; +UB(:,:,2) = [0.1 0.15 0 0; 0 0 0 0; 0 0 0 0; 0 0 0 0]; +UB(:,:,3) = UB(:,:,2); -%___________________________________________________________________________________________________ -%tests below originally taken from test_Conv2DLayer_reach_star_exact_single_input.m +image = ImageStar(LB, UB); +image = image.changeVarsPrecision('single'); -%% test 5: Conv2DLayer reach star exact +L0.reach(image); +%% test 5: Conv2DLayer reach star exact + % construct a Conv2DLayer object % this convolution layer is from the link: % http://cs231n.github.io/convolutional-networks/ @@ -164,12 +166,8 @@ b(:, :, 1) = 1; % filter 1 b(:, :, 2) = 0; % filter 2 - - - L = Conv2DLayer(W, b); -L.set_weights_biases(W, b); - +% L.set_weights_biases(W, b); % the convolutional layer has 2 filters of size 3x3 padding = 1; @@ -185,7 +183,6 @@ IM(:, :, 2) = [1 2 2 1 2; 2 1 2 0 2; 2 2 2 0 1; 1 1 1 0 0; 1 0 2 2 1]; % channel 2 input matrix IM(:, :, 3) = [0 0 2 2 1; 0 2 1 1 2; 0 2 0 0 1; 0 2 1 0 1; 1 2 1 0 0]; % channel 3 input matrix - LB(:,:,1) = [-0.1 -0.2 0 0 0; 0 0 0 0 0; 0 0 0 0 0; 0 0 0 0 0; 0 0 0 0 0]; % attack on pixel (1,1) and (1,2) LB(:,:,2) = [-0.1 -0.15 0 0 0; 0 0 0 0 0; 0 0 0 0 0; 0 0 0 0 0; 0 0 0 0 0]; LB(:,:,3) = LB(:,:,2); @@ -196,24 +193,55 @@ input = ImageStar(IM, LB, UB); - Y = L.reach_star_single_input(input); +%% test 5b: Conv2DLayer reach star exact (single precision input) +% construct a Conv2DLayer object +% this convolution layer is from the link: +% http://cs231n.github.io/convolutional-networks/ +% filter has a size of 3 x 3 +% filter 1 weight matrix with 3 channels +W(:,:, 1, 1) = [-1 0 0; 1 1 0; -1 0 -1]; % channel 1 +W(:, :, 2, 1) = [-1 0 -1; 1 -1 1; 1 1 0]; % channel 2 +W(:, :, 3, 1) = [-1 1 1; -1 -1 -1; 0 0 -1]; % channel 3 +% filter 2 weight matrix with 3 channels +W(:, :, 1, 2) = [-1 1 0; 0 0 -1; 1 0 0]; % channel 1 +W(:, :, 2, 2) = [1 0 0; 0 0 -1; 0 0 1]; % channel 2 +W(:, :, 3, 2) = [1 -1 -1; 1 1 0; -1 0 1]; % channel 3 +% biases for 2 filters +b(:, :, 1) = 1; % filter 1 +b(:, :, 2) = 0; % filter 2 +L = Conv2DLayer(single(W), single(b)); +% L.set_weights_biases(W, b); +% the convolutional layer has 2 filters of size 3x3 +padding = 1; +stride = 2; +dilation = 1; +L.set_stride(stride); +L.set_padding(padding); +L.set_dilation(dilation); +% original input volume: color image with 3 channels +IM(:, :, 1) = [0 0 2 0 0; 1 2 0 2 0; 0 0 2 2 0; 0 2 2 2 2; 2 2 2 1 1]; % channel 1 input matrix +IM(:, :, 2) = [1 2 2 1 2; 2 1 2 0 2; 2 2 2 0 1; 1 1 1 0 0; 1 0 2 2 1]; % channel 2 input matrix +IM(:, :, 3) = [0 0 2 2 1; 0 2 1 1 2; 0 2 0 0 1; 0 2 1 0 1; 1 2 1 0 0]; % channel 3 input matrix +LB(:,:,1) = [-0.1 -0.2 0 0 0; 0 0 0 0 0; 0 0 0 0 0; 0 0 0 0 0; 0 0 0 0 0]; % attack on pixel (1,1) and (1,2) +LB(:,:,2) = [-0.1 -0.15 0 0 0; 0 0 0 0 0; 0 0 0 0 0; 0 0 0 0 0; 0 0 0 0 0]; +LB(:,:,3) = LB(:,:,2); +UB(:,:,1) = [0.1 0.2 0 0 0; 0 0 0 0 0; 0 0 0 0 0; 0 0 0 0 0;0 0 0 0 0]; +UB(:,:,2) = [0.1 0.15 0 0 0; 0 0 0 0 0; 0 0 0 0 0; 0 0 0 0 0;0 0 0 0 0]; +UB(:,:,3) = UB(:,:,2); +input = ImageStar(IM, LB, UB); +input = input.changeVarsPrecision('single'); - - - - - - +Y = L.reach_star_single_input(input); \ No newline at end of file diff --git a/code/nnv/tests/set/star/test_star_getZono.m b/code/nnv/tests/set/star/test_star_getZono.m index 179ed60855..e309740f0a 100644 --- a/code/nnv/tests/set/star/test_star_getZono.m +++ b/code/nnv/tests/set/star/test_star_getZono.m @@ -1,3 +1,4 @@ +rng(3); center = [1; 1]; V = [1 0 1; 0 1 1]; P = ExamplePoly.randHrep('d',3); diff --git a/code/nnv/tests/set/star/test_star_plotBoxes_3D.m b/code/nnv/tests/set/star/test_star_plotBoxes_3D.m index b6d08f9b7e..80d873f943 100644 --- a/code/nnv/tests/set/star/test_star_plotBoxes_3D.m +++ b/code/nnv/tests/set/star/test_star_plotBoxes_3D.m @@ -1,3 +1,4 @@ +rng(1); center = [1; 1; 1]; V = [1 0 1; 0 1 1; 1 0 0]; P = ExamplePoly.randHrep('d',3);