vnncomp installation, 3d verification

code/nnv/engine/nn/layers/ReluLayer.m

@@ -93,7 +93,7 @@
                 dp = in_image.depth;
                 c = in_image.numChannel;
                 % transform to star and compute relu reachability
-                Y = PosLin.reach(in_image.toStar, method, [], relaxFactor); % reachable set computation with ReLU
+                Y = PosLin.reach(in_image.toStar, method, [], relaxFactor, dis_opt, lp_solver); % reachable set computation with ReLU
                 n = length(Y);
                 % transform back to VolumeStar
                 images(n) = VolumeStar;
@@ -105,15 +105,15 @@
                 w = in_image.width;
                 c = in_image.numChannel;
 
-                Y = PosLin.reach(in_image.toStar, method, [], relaxFactor); % reachable set computation with ReLU
+                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);
                 end
             else % star
-                images = PosLin.reach(in_image, method, [], relaxFactor); % reachable set computation with ReLU
+                images = PosLin.reach(in_image, method, [], relaxFactor, dis_opt, lp_solver); % reachable set computation with ReLU
             end
 
         end

code/nnv/engine/nncs/NonLinearODE.m

@@ -313,6 +313,10 @@ function set_output_mat(obj, output_mat)
 
             I = init_set.getZono;
             U = input_set.getZono;
+            if isempty(U)
+                U = Star(zeros(input_set.dim,1), zeros(input_set.dim,1));
+                U = U.getZono;
+            end
 
             if ~isempty(varargin)
                 if string(varargin{1}) == "poly" || string(varargin{1}) == "lin" || string(varargin{1}) == "lin-adaptive" || string(varargin{1}) == "poly-adaptive"

code/nnv/examples/Submission/VNN_COMP2024/config.yaml

@@ -1,6 +1,6 @@
 name: nnv
 ami: ami-080fce32dc8c15ced
-scripts_dir: code/nnv/examples/Submission/VNN_COMP2023/
+scripts_dir: code/nnv/examples/Submission/VNN_COMP2024/
 manual_installation_step: True
 run_installation_script_as_root: False
 run_post_installation_script_as_root: False

code/nnv/examples/Submission/VNN_COMP2024/install_tool.sh

@@ -13,24 +13,27 @@ 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
+ip link show # get mac address (for licensing)
 
-# 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
+echo $USER # get usernme (for licensing)
 
-sleep 60
+mkdir ~/.matlab/R2024a_licenses 
 
-unzip  *.zip*
+# INSTALL MPM TO INSTALL ADDITIONAL MATLAB PACKAGES
 
-ip link show # get mac address (for licensing)
+apt install wget
 
-echo $USER # get usernme (for licensing)
+wget https://www.mathworks.com/mpm/glnxa64/mpm
 
-mkdir ~/.matlab/R2024a_licenses 
+chmod +x mpm
+
+./mpm install --release=R2024a --products Deep_Learning_Toolbox_Converter_for_ONNX_Model_Format
+
+# ADD STEPS TO INSTALL GUROBI
+
+cd ~/
+
+wget https://packages.gurobi.com/11.0/gurobi11.0.2_linux64.tar.gz
+
+tar xvfz gurobi11.0.2_linux64.tar.gz
 
-# ADD STEPS TO INSTALL GUROBI

code/nnv/examples/Submission/VNN_COMP2024/post_install.sh

@@ -10,22 +10,33 @@ 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"
+# rm *.zip*
 
-sudo apt install -y python3-pip 
-pip install numpy 
+rm /usr/local/matlab/licenses/license_info.xml
 
 cd /usr/local/matlab/extern/engines/python
 python3 -m pip install .
 
 # ADD STEPS TO INSTALL GUROBI
 
+cp -f gurobi.lic ~/gurobi1102/
+
+echo 'export GUROBI_HOME="~/gurobi1102/linux64"' >> ~/.bashrc
+echo 'export GRB_LICENSE_FILE="~/gurobi1102/gurobi.lic"' >> ~/.bashrc
+echo 'export PATH="${PATH}:${GUROBI_HOME}/bin"' >> ~/.bashrc
+echo 'export LD_LIBRARY_PATH="${LD_LIBRARY_PATH}:${GUROBI_HOME}/lib"' >> ~/.bashrc
+
+# Ensure installation is correct
+matlab -nodisplay -r "cd /home/ubuntu/toolkit/code/nnv/examples/Submission/VNN_COMP2024/; prepare_run; quit"
+
+sudo apt install -y python3-pip 
+pip install numpy 
+
 # 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/
+# cd /home/ubuntu/toolkit/code/nnv/examples/Submission/VNN_COMP2024/
 # ./prepare_instance.sh v1 acasxu acas xu
+

code/nnv/examples/Submission/VNN_COMP2024/prepare_run.m

@@ -5,6 +5,10 @@ function prepare_run()
 % remove paths from any prior installation (if any)
 % rmpath(genpath('/home/ubuntu/toolkit/code/nnv/')); savepath;
 
+% install gurobi
+cd ~/gurobi1102/linux64/matlab;
+gurobi_setup;
+
 % installing nnv
 cd /home/ubuntu/toolkit/code/nnv/;
 install;
@@ -23,8 +27,8 @@ function prepare_run()
 %matlabshared.supportpkg.setSupportPackageRoot('/usr/local/MATLAB/R2022b'); 
 %addpath(genpath('/usr/local/MATLAB')); 
 
-disp("Support package path");
-disp(matlabshared.supportpkg.getSupportPackageRoot);
+#disp("Support package path");
+#disp(matlabshared.supportpkg.getSupportPackageRoot);
 
 savepath; 
 % quit;

code/nnv/examples/Submission/VNN_COMP2024/run_vnncomp2024_instance.m

@@ -91,6 +91,7 @@
 % end
 
 reachOptions = struct;
+reachOptions.lp_solver = "gurobi";
 reachOptions.reachMethod = 'approx-star';
 % reachOptions.reachMethod = 'exact-star';
 % reachOptions.device = 'cpu';

code/nnv/examples/Submission/WiP_3d/functions/add_voxels.m

@@ -0,0 +1,45 @@
+function I = add_voxels(vol, voxels, noise_disturbance)
+    % noise_disturnamce can be kept fixed here, more interesting on number
+    % of voxels changed
+
+    % Return a VolumeStar of a brightening attack on a few pixels
+
+    % Initialize vars
+    ct = 0; % keep track of pixels modified
+    flag = 0; % determine when to stop modifying pixels
+    vol = single(vol);
+    at_vol = vol;
+
+    % Create brightening attack
+    for i=1:size(vol,1)
+        for j=1:size(vol,2)
+            for k=1:size(vol,3)
+                if vol(i,j,k) < threshold
+                    at_vol(i,j,k) = 255;
+                    ct = ct + 1;
+                    if ct >= max_pixels
+                        flag = 1;
+                        break;
+                    end
+                end
+            end
+            if flag == 1
+                break
+            end
+        end
+        if flag == 1
+            break;
+        end
+    end
+
+    % Define input set as VolumeStar
+    dif_vol = -vol + at_vol;
+    noise = dif_vol;
+    V(:,:,:,:,1) = vol;   % center of set
+    V(:,:,:,:,2) = noise; % basis vectors
+    C = [1; -1];          % constraints
+    d = [1; -1];          % constraints
+    I = VolumeStar(V, C, d, 1-noise_disturbance, 1); % input set
+
+
+end

code/nnv/examples/Submission/WiP_3d/functions/verify_instance_shape.m

@@ -0,0 +1,65 @@
+function results = verify_instance_shape(net, vol, target, attack, reachOptions)
+    % verify medmnist with inputs (input images), targets (labels) and attack
+    % (struct with adversarial attack info)
+    % results =  verify_medmnist(net, matlabNet, inputs, targets, attack, max_value*, min_value*)
+
+    % Check what type of attack to consider
+    if strcmp(attack.Name, 'add') || strcmp(attack.Name, 'remove')
+        max_pixels = attack.max_pixels;
+        threshold = attack.threshold;
+        noise_disturbance = attack.noise_de;
+    else
+        error("Adversarial attack not supported.");
+    end
+
+    % Choose attack
+    if strcmp(attack.Name, 'add')
+        I = add_voxels(vol, max_pixels, threshold, noise_disturbance);
+    elseif strcmp(attack.Name, 'remove')
+        I = remove_voxels(vol, max_pixels, threshold, noise_disturbance);
+    end
+
+    % Begin analysis
+
+    t = tic; % start timer
+
+    results = zeros(1,2);
+
+    % Check for missclassification
+    vol = single(vol);
+    y = net.evaluate(vol);
+    [~, y] = max(y);
+    if y ~= target
+        results(1) = -1; % missclassified
+        results(2) = toc(t);
+        return
+    end
+
+    % Check for falsification 
+    n_samples = 100; % number of random samples to try for falsification
+    xRand = I.sample(n_samples);
+    for k = 1:n_samples
+        x = xRand{k};
+        y = net.evaluate(x);
+        [~,idx] = max(y);
+        if idx ~= target
+            results(1) = 0;
+            results(2) = toc(t);
+            return
+        end
+    end
+
+    % Compute reachability for verification
+    try
+        results(1) = net.verify_robustness(I, reachOptions, target);
+    catch ME
+        results(1) = -2;
+        warning(ME.message);
+    end
+
+    % Save results
+    results(2) = toc(t);
+
+end
+
+