Merge pull request #17 from verivital/master

Merge latest changes to test reproducible results

.codeoceandatasets

@@ -0,0 +1,2 @@
+MNIST
+CIFAR

.gitmodules

@@ -1,9 +1,9 @@
+[submodule "code/nnv/engine/hyst"]
+	path = code/nnv/engine/hyst
+	url = https://github.com/verivital/hyst.git
 [submodule "code/nnv/engine/cora"]
 	path = code/nnv/engine/cora
-    url = https://github.com/verivital/CORA.git
+	url = https://github.com/verivital/CORA
 [submodule "code/nnv/engine/nnmt"]
 	path = code/nnv/engine/nnmt
 	url = https://github.com/verivital/nnmt
-[submodule "code/nnv/engine/hyst"]
-	path = code/nnv/engine/hyst
-	url = https://github.com/verivital/hyst.git

README.md

@@ -15,6 +15,10 @@ nnv can be executed online without installing Matlab or other dependencies throu
     1) Install Matlab
 
     2) Clone or download the nnv toolbox from (https://github.com/verivital/nnv)
+
+    Note: to operate correctly, nnv depends on other tools (CORA, NNMT, HyST), which are included as git submodules. As such, you must clone recursively, e.g., with the following:
+
+    git clone --recursive https://github.com/verivital/nnv.git
 
     3) Open matlab, then go to the directory where nnv exists on your machine, then run the `install.m` script located at /nnv/
 

code/nnv/engine/nn/cnn/CNN.m

@@ -361,15 +361,13 @@ function start_pool(obj)
     methods % evaluate robustness
 
         % evaluate robustness of a network on an array of input (test) sets
-        function [r, ids] = evaluateRobustness(varargin)
+        function r = evaluateRobustness(varargin)
             % @in_images: input sets
             % @correct_ids: an array of correct labels corresponding to the input sets
             % @method: reachability method: 'exact-star', 'approx-star',
             % 'approx-zono' and 'abs-dom'
             % @numCores: number of cores used in computation
-            % @r: robustness value (in percentage)
-            % @ids: classified ids
-
+            % @r: robustness value (in percentage)           
 
             % author: Dung Tran
             % date:1/9/2020
@@ -392,68 +390,67 @@ function start_pool(obj)
             end
 
 
-            if length(correct_ids) ~= length(in_images)
+            N = length(in_images);
+            if length(correct_ids) ~= N
                 error('Inconsistency between the number of correct_ids and the number of input sets');
             end
 
-
-            N = length(in_images);
-            % compute reachable set
-            if strcmp(method, 'exact-star')
-                outputSets = cell(1, N);
-                for i=1:N
-                    outputSets{i} = obj.reach(in_images, method, numOfCores);
-                end
-            else
+
+            count = zeros(1, N);
+            if ~strcmp(method, 'exact-star')                
+                % compute reachable set
                 outputSets = obj.reach(in_images, method, numOfCores);
-            end
-
-            % classify outputset             
-            ids = cell(1,N);
-            for i=1:N
-                if iscell(outputSets)
-                    outputSet = outputSets{i};
+
+                % verify reachable set              
+                if numOfCores> 1
+                    parfor i=1:N
+                        count(i) = CNN.isRobust(outputSets(i), correct_ids(i));                            
+                    end
                 else
-                    outputSet = outputSets(i);
-                end
-                M = length(outputSet);
-                id = [];
-                for j=1:M
-                    id1 = CNN.classifyOutputSet(outputSet(j));
-                    if ~isempty(id1)
-                        id = [id id1];
-                    else
-                        id = [];
+                    for i=1:N
+                        count(i) = CNN.isRobust(outputSets(i), correct_ids(i));
                     end
                 end
-                ids{i} = id;
+
             end
 
-            % compute percentage of cases that we successfully prove the
-            % robustness of the network on the test input sets
-
-            count = 0; 
-            for i=1:N
-                id = ids{i};                
-                if ~isempty(id)
-                    M = length(id);
-                    count1 = 0;
-                    for j=1:M
-                        if id(j) ~= correct_ids(i)
-                            count1 = count1 + 1;
+            if strcmp(method, 'exact-star')
+                % compute reachable set
+                if numOfCores > 1
+                    parfor i=1:N
+                        outputSets = obj.reach(in_images(i), method);
+                        % verify reachable set
+                        M = length(outputSets);
+                        count1 = 0;
+                        for j=1:M
+                            count1 = count1 + CNN.isRobust(outputSets(j), correct_ids(i));
+                        end
+                        if count1 == M
+                            count(i) = 1;
                         end
+
                     end
-
-                    if count1 == 0
-                        count = count + 1;
+                else
+                    for i=1:N
+                        outputSets = obj.reach(in_images(i), method);
+                        % verify reachable set
+                        M = length(outputSets);
+                        count1 = 0;
+                        for j=1:M
+                            count1 = count1 + CNN.isRobust(outputSets(j), correct_ids(i));
+                        end
+                        if count1 == M
+                            count(i) = 1;
+                        end
                     end
                 end
-
-            end
-
-            r = count/N; 
+                                    
+            end          
+                        
+            r = sum(count)/N; 
 
-        end
+        end      
+
 
 
     end
@@ -529,6 +526,37 @@ function start_pool(obj)
 
         end
 
+
+        % check robustness using the outputSet
+        function bool = isRobust(outputSet, correct_id)
+            % @outputSet: the outputSet we need to check
+            % @correct_id: the correct_id of the classified output
+
+            % author: Dung Tran
+            % date: 1/11/2020
+
+            if correct_id > outputSet.numChannel || correct_id < 1
+                error('Invalid correct id');
+            end
+
+            count = 0;
+            for i=1:outputSet.numChannel
+                if correct_id ~= i
+                    if outputSet.is_p1_larger_p2([1 1 i], [1 1 correct_id]);
+                       bool = 0;
+                       break;
+                    else
+                        count = count + 1;
+                    end
+                end
+            end
+
+            if count == outputSet.numChannel - 1
+                bool = 1;
+            end
+
+        end
+
 
         % classify outputset
         function classified_id = classifyOutputSet(outputSet)
@@ -545,9 +573,10 @@ function start_pool(obj)
 
             if ~isa(outputSet, 'ImageStar') && ~isa(outputSet, 'ImageZono')
                 error('Output set is not an ImageStar or an ImageZono');
-            end
-                       
+            end           
+
             [lb, ub] = outputSet.getRanges; 
+
 
             [max_lb, max_lb_id] = max(lb);
             ub(max_lb_id) = [];
@@ -563,6 +592,7 @@ function start_pool(obj)
 
 
 
+
     end
 
 

code/nnv/engine/nn/fnn/FFNNS.m

@@ -28,6 +28,9 @@
         numSamples = 2000; % default number of samples using to falsify a property
         unsafeRegion = []; % unsafe region of the network
 
+
+        Operations = []; % flatten a network into a sequence of operations
+
     end
 
 
@@ -1327,6 +1330,50 @@ function start_pool(obj)
 
 
 
+    end
+
+
+    methods % verify using Deep First Search + exact star for verification (on testing phase)
+
+
+        % flatten a FFNN into a sequence of operations for reachability
+        function flatten(obj, reachMethod)
+            % @reachMethod: reachability method
+
+            % author: Dung Tran
+            % date: 1/18/2020
+
+
+            Ops = [];
+
+            for i=1:obj.nL
+                Op = obj.Layers(i).flatten(reachMethod);
+                Ops = [Ops Op];
+            end
+
+            obj.Operations = Ops;
+
+        end
+
+
+        function [safe, counterExamples] = verify_DFS(obj, inputSets, unsafeRegion, numCores)
+            % @inputSets: an array of star set
+            % @unsafeRegion: a HalfSpace object
+            % @numCores: number of cores used for verification
+
+            % author: Dung Tran
+            % date: 1/18/2020
+
+
+
+
+        end
+
+
+
+
+
+
     end
 
 

code/nnv/engine/nn/fnn/LayerS.m

@@ -179,7 +179,104 @@
 
 
         end
+
+    end
+
 
+    methods % flattening a layer into a sequence of operation
+
+
+        function Ops = flatten(obj, reachMethod)
+            % @reachMethod: reachability method
+            % @Ops: an array of operations for the reachability of
+            % the layer
+
+            % author: Dung Tran
+            % date: 1/18/2020
+
+            O1 = Operation('AffineMap', obj.W, obj.b);
+
+
+            if strcmp(obj.f, 'poslin')
+
+                if strcmp(reachMethod, 'exact-star')
+                    O2(obj.N) = Operation;
+                    for i=1:obj.N
+                        O2(i) = Operation('PosLin_stepExactReach', i);
+                    end
+                elseif strcmp(reachMethod, 'approx-star')
+                    O2 = Operation('PosLin_approxReachStar');
+                elseif strcmp(reachMethod, 'approx-zono')
+                    O2 = Operation('PosLin_approxReachZono');
+                elseif strcmp(reachMethod, 'abs-dom')
+                    O2 = Operation('PosLin_approxReachAbsDom');
+                end
+
+            elseif strcmp(obj.f, 'satlin')
+
+                if strcmp(reachMethod, 'exact-star')
+                    O2(obj.N) = Operation;
+                    for i=1:obj.N
+                        O2(i) = Operation('SatLin_stepExactReach', i);
+                    end
+                elseif strcmp(reachMethod, 'approx-star')
+                    O2 = Operation('SatLin_approxReachStar');
+                elseif strcmp(reachMethod, 'approx-zono')
+                    O2 = Operation('SatLin_approxReachZono');
+                elseif strcmp(reachMethod, 'abs-dom')
+                    O2 = Operation('SatLin_approxReachAbsDom');
+                end
+
+            elseif strcmp(obj.f, 'satlins')
+
+                if strcmp(reachMethod, 'exact-star')
+                    O2(obj.N) = Operation;
+                    for i=1:obj.N
+                        O2(i) = Operation('SatLins_stepExactReach', i);
+                    end
+                elseif strcmp(reachMethod, 'approx-star')
+                    O2 = Operation('SatLins_approxReachStar');
+                elseif strcmp(reachMethod, 'approx-zono')
+                    O2 = Operation('SatLins_approxReachZono');
+                elseif strcmp(reachMethod, 'abs-dom')
+                    O2 = Operation('SatLins_approxReachAbsDom');
+                end
+
+            elseif strcmp(obj.f, 'purelin')
+
+                O2 = [];
+
+            elseif strcmp(obj.f, 'logsig')
+
+                if strcmp(reachMethod, 'exact-star')
+                    error('\nCannot do exact analysis for layer with logsig activation function, use approximate method');
+                elseif strcmp(reachMethod, 'approx-star')
+                    O2 = Operation('LogSig_approxReachStar');
+                elseif strcmp(reachMethod, 'approx-zono')
+                    O2 = Operation('LogSig_approxReachZono');
+                elseif strcmp(reachMethod, 'abs-dom')
+                    O2 = Operation('LogSig_approxReachAbsDom');
+                end
+
+            elseif strcmp(obj.f, 'tansig')
+
+
+                if strcmp(reachMethod, 'exact-star')
+                    error('\nCannot do exact analysis for layer with logsig activation function, use approximate method');
+                elseif strcmp(reachMethod, 'approx-star')
+                    O2 = Operation('TanSig_approxReachStar');
+                elseif strcmp(reachMethod, 'approx-zono')
+                    O2 = Operation('TanSig_approxReachZono');
+                elseif strcmp(reachMethod, 'abs-dom')
+                    O2 = Operation('TanSig_approxReachAbsDom');
+                end
+
+            end
+
+            Ops = [O1 O2];
+
+        end
+
     end