diff --git a/code/nnv/engine/cora b/code/nnv/engine/cora index eeb971d84..99c635121 160000 --- a/code/nnv/engine/cora +++ b/code/nnv/engine/cora @@ -1 +1 @@ -Subproject commit eeb971d8412777e1f0cad839138af34761dbbba5 +Subproject commit 99c6351214eb847f920b2d2227726196bafae1a1 diff --git a/code/nnv/engine/nn/layers/FullyConnectedLayer.m b/code/nnv/engine/nn/layers/FullyConnectedLayer.m index aa8e10bf3..525463e9f 100644 --- a/code/nnv/engine/nn/layers/FullyConnectedLayer.m +++ b/code/nnv/engine/nn/layers/FullyConnectedLayer.m @@ -198,10 +198,6 @@ % @in_image: an input imagestar % @image: output set % @option: = 'single' or 'parallel' - - % author: Dung Tran - % date: 6/26/2019 - % update: 1/6/2020 update reason: add zonotope method switch nargin @@ -210,24 +206,18 @@ in_images = varargin{2}; method = varargin{3}; option = varargin{4}; - % relaxFactor = varargin{5}; do not use - % dis_opt = varargin{6}; do not use - % lp_solver = varargin{7}; do not use case 6 obj = varargin{1}; in_images = varargin{2}; method = varargin{3}; option = varargin{4}; - %relaxFactor = varargin{5}; do not use - % dis_opt = varargin{6}; do not use case 5 obj = varargin{1}; in_images = varargin{2}; method = varargin{3}; option = varargin{4}; - %relaxFactor = varargin{5}; do not use case 4 obj = varargin{1}; @@ -281,9 +271,6 @@ % @in_image: input imagestar % @image: output set - % author: Dung Tran - % date: 6/26/2019 - if ~isa(in_image, 'ImageStar') && ~isa(in_image, 'Star') error('Input set is not an ImageStar or Star'); end @@ -296,12 +283,13 @@ end n = in_image.numPred; - V(1, 1, :, in_image.numPred + 1) = zeros(obj.OutputSize, 1, 'like', in_image.V); + V(1, 1, :, in_image.numPred + 1) = zeros(obj.OutputSize, 1, 'like', in_image.V); for i=1:n+1 I = in_image.V(:,:,:,i); I = reshape(I,N,1); % flatten input if i==1 V(1, 1,:,i) = obj.Weights*I + obj.Bias; + V2(1,1,:,i) = gpuArray(obj.Weights)*I + gpuArray(obj.Bias); else V(1, 1,:,i) = obj.Weights*I; end @@ -320,9 +308,6 @@ % @option: = 'parallel' or 'single' % @S: output ImageStar - % author: Dung Tran - % date: 1/6/2020 - n = length(inputs); if isa(inputs, "ImageStar") S(n) = ImageStar; @@ -350,10 +335,7 @@ function image = reach_zono(obj, in_image) % @in_image: input imagezono % @image: output set - - % author: Dung Tran - % date: 1/2/2020 - + if ~isa(in_image, 'ImageZono') && ~isa(in_image, 'Zono') error('Input set is not an ImageZono or Zono'); end @@ -390,9 +372,6 @@ % @option: = 'parallel' or 'single' % @S: output ImageZono - % author: Dung Tran - % date: 1/6/2020 - n = length(inputs); if isa(inputs, 'ImageZono') S(n) = ImageZono; @@ -416,22 +395,13 @@ end - function image = reachSequence_star(obj, in_image, option) + function image = reachSequence_star(obj, in_image, ~) % @in_image: input imagestar - % @image: output set - - % author: Dung Tran - % date: 6/26/2019 - + % @image: output set if ~isa(in_image, 'ImageStar') error('Input set is not an ImageStar'); end - -% N = in_image.height*in_image.width*in_image.numChannel; -% if N~= obj.InputSize -% error('Inconsistency between the size of the input image and the InputSize of the network'); -% end n = in_image.numPred; V(:, :, 1, in_image.numPred + 1) = zeros(obj.OutputSize, in_image.width); @@ -459,9 +429,6 @@ % neural network tool box % @L : a FullyConnectedLayer obj for reachability analysis purpose - % author: Dung Tran - % date: 6/26/2019 - if ~isa(fully_connected_layer, 'nnet.cnn.layer.FullyConnectedLayer') error('Input is not a Matlab nnet.cnn.layer.FullyConnectedLayer class'); end diff --git a/code/nnv/examples/Tutorial/NN/MNIST/verify_fc_gpu.m b/code/nnv/examples/Tutorial/NN/MNIST/verify_fc_gpu.m index 36d57f01d..0e61b246d 100644 --- a/code/nnv/examples/Tutorial/NN/MNIST/verify_fc_gpu.m +++ b/code/nnv/examples/Tutorial/NN/MNIST/verify_fc_gpu.m @@ -72,6 +72,7 @@ end toc(t); +net_app = net; %% Let's visualize the ranges for every possible output diff --git a/code/nnv/examples/other/numerical_discrepancies.m b/code/nnv/examples/other/numerical_discrepancies.m new file mode 100644 index 000000000..fc0bdcfe8 --- /dev/null +++ b/code/nnv/examples/other/numerical_discrepancies.m @@ -0,0 +1,224 @@ +%% There are some discrepancies that we can observe here + +% Load network +mnist_model = load('../Tutorial/NN/MNIST/mnist_model_fc.mat'); + +% Create NNV model +net1 = matlab2nnv(mnist_model.net); +net2 = matlab2nnv(mnist_model.net); +net3 = matlab2nnv(mnist_model.net); +net4 = matlab2nnv(mnist_model.net); + +% Load data (no download necessary) +digitDatasetPath = fullfile(matlabroot,'toolbox','nnet','nndemos', ... + 'nndatasets','DigitDataset'); +% Images +imds = imageDatastore(digitDatasetPath, ... + 'IncludeSubfolders',true,'LabelSource','foldernames'); + +% Load first image in dataset +[img, fileInfo] = readimage(imds,600); +img = single(img); % change precision + +% Create input set +ones_ = ones(size(img), 'single'); +disturbance = 2 .* ones_; % one pixel value (images are not normalized, they get normalized in the ImageInputLayer) + +% However, we need to ensure the values are within the valid range for pixels ([0 255]) +lb_min = zeros(size(img)); % minimum allowed values for lower bound is 0 +ub_max = 255*ones(size(img)); % maximum allowed values for upper bound is 255 +lb_clip = max((img-disturbance),lb_min); +ub_clip = min((img+disturbance), ub_max); +IS = ImageStar(lb_clip, ub_clip); % this is the input set we will use + +% First, we need to define the reachability options +reachOptions = struct; % initialize +reachOptions.reachMethod = 'approx-star'; % using approxiate method + + +%% Let's compute reach sets to evaluate the differences + +R1 = net1.reach(IS, reachOptions); +y1 = net1.evaluate(img); + +reachOptions.device = 'gpu'; +IS = ImageStar(lb_clip, ub_clip); % this is the input set we will use +R2 = net2.reach(IS, reachOptions); +y2 = net2.evaluate(gpuArray(img)); + + +%% Now on double precision +reachOptions = struct; % initialize +reachOptions.reachMethod = 'approx-star'; % using approximate method + +IS = ImageStar(lb_clip, ub_clip); % this is the input set we will use +IS = IS.changeVarsPrecision('double'); +net3 = net3.changeParamsPrecision('double'); +R3 = net3.reach(IS, reachOptions); +y3 = net3.evaluate(double(img)); + +reachOptions.device = 'gpu'; +ImageStar(lb_clip, ub_clip); % this is the input set we will use +IS = IS.changeVarsPrecision('double'); +net4.changeParamsPrecision('double'); +R4 = net4.reach(IS, reachOptions); +y4 = net4.evaluate(gpuArray(double(img))); + +%% What do the output ranges look like for all of them? + +[lb1, ub1] = R1.estimateRanges; +[lb2, ub2] = R2.estimateRanges; +[lb3, ub3] = R3.estimateRanges; +[lb4, ub4] = R4.estimateRanges; + +outputRanges = [lb1; lb2; lb3; lb4; ub1; ub2; ub3; ub4]; +outputRanges = squeeze(outputRanges)' + +%% where did it go wrong? +%% Layer 1 +r1 = net1.reachSet{1}; +r2 = net2.reachSet{1}; +r3 = net3.reachSet{1}; +r4 = net4.reachSet{1}; +% +% [lb1, ub1] = r1.estimateRanges; +% [lb2, ub2] = r2.estimateRanges; +% [lb3, ub3] = r3.estimateRanges; +% [lb4, ub4] = r4.estimateRanges; +% +% layer1 = {lb1; lb2; lb3; lb4; ub1; ub2; ub3; ub4}; +% % layer1 = squeeze(layer1)'; +% +%% Layer 2 +r1 = net1.reachSet{2}; +r2 = net2.reachSet{2}; +r3 = net3.reachSet{2}; +r4 = net4.reachSet{2}; +% +% [lb1, ub1] = r1.estimateRanges; +% [lb2, ub2] = r2.estimateRanges; +% [lb3, ub3] = r3.estimateRanges; +% [lb4, ub4] = r4.estimateRanges; +% +% layer2 = {lb1; lb2; lb3; lb4; ub1; ub2; ub3; ub4}; +% +%% Layer 3 +r1 = net1.reachSet{3}; +r2 = net2.reachSet{3}; +r3 = net3.reachSet{3}; +r4 = net4.reachSet{3}; +% +% [lb1, ub1] = r1.estimateRanges; +% [lb2, ub2] = r2.estimateRanges; +% [lb3, ub3] = r3.estimateRanges; +% [lb4, ub4] = r4.estimateRanges; +% +% layer3 = {lb1; lb2; lb3; lb4; ub1; ub2; ub3; ub4}; +% +%% Layer 4 +r1 = net1.reachSet{4}; +r2 = net2.reachSet{4}; +r3 = net3.reachSet{4}; +r4 = net4.reachSet{4}; +% +% [lb1, ub1] = r1.estimateRanges; +% [lb2, ub2] = r2.estimateRanges; +% [lb3, ub3] = r3.estimateRanges; +% [lb4, ub4] = r4.estimateRanges; +% +% layer4 = {lb1; lb2; lb3; lb4; ub1; ub2; ub3; ub4}; +% +%% Layer 5 +r1 = net1.reachSet{5}; +r2 = net2.reachSet{5}; +r3 = net3.reachSet{5}; +r4 = net4.reachSet{5}; +% +% [lb1, ub1] = r1.estimateRanges; +% [lb2, ub2] = r2.estimateRanges; +% [lb3, ub3] = r3.estimateRanges; +% [lb4, ub4] = r4.estimateRanges; +% +% layer5 = {lb1; lb2; lb3; lb4; ub1; ub2; ub3; ub4}; +% +% +%% Layer 6 +r1 = net1.reachSet{6}; +r2 = net2.reachSet{6}; +r3 = net3.reachSet{6}; +r4 = net4.reachSet{6}; +% +% [lb1, ub1] = r1.estimateRanges; +% [lb2, ub2] = r2.estimateRanges; +% [lb3, ub3] = r3.estimateRanges; +% [lb4, ub4] = r4.estimateRanges; +% +% layer6 = {lb1; lb2; lb3; lb4; ub1; ub2; ub3; ub4}; +% +% +%% Layer 7 +r1 = net1.reachSet{7}; +r2 = net2.reachSet{7}; +r3 = net3.reachSet{7}; +r4 = net4.reachSet{7}; +% +% [lb1, ub1] = r1.estimateRanges; +% [lb2, ub2] = r2.estimateRanges; +% [lb3, ub3] = r3.estimateRanges; +% [lb4, ub4] = r4.estimateRanges; +% +% layer7 = {lb1; lb2; lb3; lb4; ub1; ub2; ub3; ub4}; +% +% +%% Layer 8 +r1 = net1.reachSet{8}; +r2 = net2.reachSet{8}; +r3 = net3.reachSet{8}; +r4 = net4.reachSet{8}; +% +% [lb1, ub1] = r1.estimateRanges; +% [lb2, ub2] = r2.estimateRanges; +% [lb3, ub3] = r3.estimateRanges; +% [lb4, ub4] = r4.estimateRanges; +% +% layer8 = {lb1; lb2; lb3; lb4; ub1; ub2; ub3; ub4}; +% +% +%% Layer 9 +r1 = net1.reachSet{9}; +r2 = net2.reachSet{9}; +r3 = net3.reachSet{9}; +r4 = net4.reachSet{9}; +% +% [lb1, ub1] = r1.estimateRanges; +% [lb2, ub2] = r2.estimateRanges; +% [lb3, ub3] = r3.estimateRanges; +% [lb4, ub4] = r4.estimateRanges; +% +% layer9 = {lb1; lb2; lb3; lb4; ub1; ub2; ub3; ub4}; +% +%% Layer 10 +r1 = net1.reachSet{10}; +r2 = net2.reachSet{10}; +r3 = net3.reachSet{10}; +r4 = net4.reachSet{10}; +% +% [lb1, ub1] = r1.estimateRanges; +% [lb2, ub2] = r2.estimateRanges; +% [lb3, ub3] = r3.estimateRanges; +% [lb4, ub4] = r4.estimateRanges; +% +% layer10 = {lb1; lb2; lb3; lb4; ub1; ub2; ub3; ub4}; +% +%% Layer 11 +r1 = net1.reachSet{11}; +r2 = net2.reachSet{11}; +r3 = net3.reachSet{11}; +r4 = net4.reachSet{11}; +% +% [lb1, ub1] = r1.estimateRanges; +% [lb2, ub2] = r2.estimateRanges; +% [lb3, ub3] = r3.estimateRanges; +% [lb4, ub4] = r4.estimateRanges; +% +% layer11 = {lb1; lb2; lb3; lb4; ub1; ub2; ub3; ub4};