diff --git a/code/nnv/examples/NNV3.0/Dockerfile b/code/nnv/examples/NNV3.0/Dockerfile new file mode 100644 index 000000000..04db1daea --- /dev/null +++ b/code/nnv/examples/NNV3.0/Dockerfile @@ -0,0 +1,83 @@ +# NOTE: +# THIS DOCKERFILE IS A COPY OF THE ORIGINAL NNV DOCKERFILE +# ONLY THIS ONE WILL NOT CLONE NNV BUT INSTEAD MOUNT THE CURRENT +# LOCAL VERSION SO THAT WE CAN TEST CHANGES. + +# Building from Dockerfile provided by Mathworks +# https://github.com/mathworks-ref-arch/matlab-dockerfile/blob/main/Dockerfile + +# Specify MATLAB release +ARG MATLAB_RELEASE=R2024b + +# Specify the list of products to install into MATLAB. +ARG MATLAB_PRODUCT_LIST="MATLAB Computer_Vision_Toolbox Control_System_Toolbox Deep_Learning_Toolbox Image_Processing_Toolbox Optimization_Toolbox Parallel_Computing_Toolbox Statistics_and_Machine_Learning_Toolbox Symbolic_Math_Toolbox System_Identification_Toolbox Deep_Learning_Toolbox_Converter_for_ONNX_Model_Format" + +# Specify MATLAB Install Location. +ARG MATLAB_INSTALL_LOCATION="/opt/matlab/${MATLAB_RELEASE}" + +# Specify license server information using the format: port@hostname +ARG LICENSE_SERVER="27009@licenseserver.it.vanderbilt.edu" + +# To check the available matlab-deps images, see: https://hub.docker.com/r/mathworks/matlab-deps +FROM mathworks/matlab-deps:${MATLAB_RELEASE} + +# Declare build arguments to use at the current build stage. +ARG MATLAB_RELEASE +ARG MATLAB_PRODUCT_LIST +ARG MATLAB_INSTALL_LOCATION +ARG LICENSE_SERVER + +# Install mpm dependencies and Python (with shared library for MATLAB). +RUN export DEBIAN_FRONTEND=noninteractive \ + && apt-get update \ + && apt-get install --no-install-recommends --yes \ + wget \ + ca-certificates \ + python3 \ + python3-pip \ + python3-venv \ + libpython3-dev \ + && apt-get clean \ + && apt-get autoremove \ + && apt-get install -y git \ + && rm -rf /var/lib/apt/lists/* + +# Add "matlab" user and grant sudo permission. +RUN adduser --shell /bin/bash --disabled-password --gecos "" matlab \ + && echo "matlab ALL=(ALL) NOPASSWD: ALL" > /etc/sudoers.d/matlab \ + && chmod 0440 /etc/sudoers.d/matlab + +# Set user and work directory. +USER matlab +WORKDIR /home/matlab + +# Run mpm to install MATLAB in the target location and delete the mpm installation afterwards. +# If mpm fails to install successfully, then print the logfile in the terminal, otherwise clean up. +# Pass in $HOME variable to install support packages into the user's HOME folder. +RUN wget -q https://www.mathworks.com/mpm/glnxa64/mpm \ + && chmod +x mpm \ + && sudo HOME=${HOME} ./mpm install \ + --release=${MATLAB_RELEASE} \ + --destination=${MATLAB_INSTALL_LOCATION} \ + --products ${MATLAB_PRODUCT_LIST} \ + || (echo "MPM Installation Failure. See below for more information:" && cat /tmp/mathworks_root.log && false) \ + && sudo rm -rf mpm /tmp/mathworks_root.log \ + && sudo ln -s ${MATLAB_INSTALL_LOCATION}/bin/matlab /usr/local/bin/matlab + + +ENV MLM_LICENSE_FILE=$LICENSE_SERVER + +# Install nnv + +COPY --chown=matlab:matlab . /home/matlab/nnv +WORKDIR /home/matlab/nnv + +# Create Python virtual environment at .venv (required by cp_env.m) +RUN python3 -m venv /home/matlab/nnv/.venv \ + && /home/matlab/nnv/.venv/bin/pip install --no-cache-dir -r requirement.txt + +ENV PATH="/home/matlab/nnv/.venv/bin:$PATH" +ENV VIRTUAL_ENV="/home/matlab/nnv/.venv" + +# Configure MATLAB to use the venv Python and install NNV +RUN matlab -nodisplay -r "pyenv('Version', '/home/matlab/nnv/.venv/bin/python'); cd code/nnv/; install; savepath; exit()" diff --git a/code/nnv/examples/NNV3.0/FairNNV/adult_verify_fm26.m b/code/nnv/examples/NNV3.0/FairNNV/adult_verify_fm26.m new file mode 100644 index 000000000..a84edaa0f --- /dev/null +++ b/code/nnv/examples/NNV3.0/FairNNV/adult_verify_fm26.m @@ -0,0 +1,309 @@ +%% Exact Fairness Verification of Adult Classification Model (NN) +% FM26 Tool Paper Results Script +% Generates results for: (1) Counterfactual fairness table +% (2) Individual fairness stacked bar charts +% (3) Comprehensive timing table +% +% This script can be run standalone or called from run_fm26_fairnnv.m +% When run standalone, default paths are used. +% When called from runner, paths are set via config struct. + +% Suppress warnings +warning('off', 'nnet_cnn_onnx:onnx:WarnAPIDeprecation'); +warning('off', 'nnet_cnn_onnx:onnx:FillingInClassNames'); + +%% Load data into NNV +warning('on', 'verbose') + +%% Setup +% Check if config exists (set by runner script), otherwise use defaults +if ~exist('config', 'var') + % Default configuration for standalone execution + config.modelsDir = './adult_onnx'; + config.dataDir = './data'; + config.outputDir = './fm26_fairnnv_results'; + config.dataFile = 'adult_data.mat'; + config.modelList = {'AC-1', 'AC-3'}; + config.numObs = 100; + config.randomSeed = 500; + config.timeout = 600; + config.epsilon_counterfactual = [0.0]; + config.epsilon_individual = [0.01, 0.02, 0.03, 0.05, 0.07, 0.1]; + + % Clear workspace except config when running standalone + clearvars -except config; +end + +modelDir = config.modelsDir; +onnxFiles = dir(fullfile(modelDir, '*.onnx')); % List all .onnx files + +% Load data +dataFilePath = fullfile(config.dataDir, config.dataFile); +load(dataFilePath, 'X', 'y'); + +% Create results directory if it doesn't exist +resultsDir = config.outputDir; +if ~exist(resultsDir, 'dir') + mkdir(resultsDir); +end + +% Initialize results storage +results_counterfactual = {}; % For counterfactual fairness (epsilon = 0) +results_individual = {}; % For individual fairness (epsilon > 0) +results_timing = {}; % For comprehensive timing table + +% List of models to process +modelList = config.modelList; + +% Epsilon values +% 0.0 -> counterfactual fairness (flips sensitive attribute) +% >0.0 -> individual fairness (flips SA w/ perturbation of numerical features) +epsilon_counterfactual = config.epsilon_counterfactual; +epsilon_individual = config.epsilon_individual; +epsilon = [epsilon_counterfactual, epsilon_individual]; % Combined for processing + +% Number of observations to test +numObs = config.numObs; + +%% Loop through each model +for k = 1:length(onnxFiles) + [~, modelName, ~] = fileparts(onnxFiles(k).name); + if any(strcmp(modelName, modelList)) + + clear net netONNX outputSet IS R + + onnx_model_path = fullfile(onnxFiles(k).folder, onnxFiles(k).name); + + % Load the ONNX file as DAGNetwork + netONNX = importONNXNetwork(onnx_model_path, 'OutputLayerType', 'classification', 'InputDataFormats', {'BC'}); + + % Convert the DAGNetwork to NNV format + net = matlab2nnv(netONNX); + + net.OutputSize = 2; + + X_test_loaded = permute(X, [2, 1]); + y_test_loaded = y+1; % update labels + + % Normalize features in X_test_loaded + min_values = min(X_test_loaded, [], 2); + max_values = max(X_test_loaded, [], 2); + + % Ensure no division by zero for constant features + variableFeatures = max_values - min_values > 0; + min_values(~variableFeatures) = 0; % Avoids changing constant features + max_values(~variableFeatures) = 1; % Avoids division by zero + + % Normalizing X_test_loaded + X_test_loaded = (X_test_loaded - min_values) ./ (max_values - min_values); + + % Count total observations + total_obs = size(X_test_loaded, 2); + + % Test accuracy --> verify matches with python + total_corr= 0; + for i=1:total_obs + im = X_test_loaded(:, i); + predictedLabels = net.evaluate(im); + [~, Pred] = min(predictedLabels); + TrueLabel = y_test_loaded(i); + if Pred == TrueLabel + total_corr = total_corr + 1; + end + end + disp("Model: " + modelName); + disp("Accuracy of Model: "+string(total_corr/total_obs)); + + %% Verification + + % First, we define the reachability options + reachOptions = struct; % initialize + reachOptions.reachMethod = 'exact-star'; + + % Set up results + nE = length(epsilon); + res = zeros(numObs,nE); % robust result + time = zeros(numObs,nE); % computation time + met = repmat("exact", [numObs, nE]); % method used to compute result + + % Randomly select observations + rng(config.randomSeed); % Set a seed for reproducibility + rand_indices = randsample(total_obs, numObs); + + for e=1:length(epsilon) + clear R outputSet IS temp t + % Reset the timeout flag + assignin('base', 'timeoutOccurred', false); + + % Create and configure the timer + verificationTimer = timer; + verificationTimer.StartDelay = config.timeout; % Set timer (default: 10 minutes) + verificationTimer.TimerFcn = @(myTimerObj, thisEvent) ... + assignin('base', 'timeoutOccurred', true); + start(verificationTimer); % Start the timer + + + for i=1:numObs + idx = rand_indices(i); + IS = perturbationIF(X_test_loaded(:, idx), epsilon(e), min_values, max_values); + + t = tic; % Start timing the verification for each sample + outputSet = net.reach(IS,reachOptions); % Generate output set + target = y_test_loaded(idx); + + R = Star; + % Process set + if ~isa(outputSet, "Star") + nr = length(outputSet); + R(nr) = Star; + for s=1:nr + R(s) = outputSet(s).toStar; + end + else + R = outputSet; + end + + % Process fairness specification + target = net.robustness_set(target, 'min'); + + % Verify fairness + temp = 1; + for s = 1:length(R) + if verify_specification(R(s), target) ~= 1 + temp = 0; + break + end + end + + met(i,e) = 'exact'; + + res(i,e) = temp; % robust result + + time(i,e) = toc(t); % store computation time + + % Check for timeout flag + if evalin('base', 'timeoutOccurred') + disp(['Timeout reached for epsilon = ', num2str(epsilon(e)), ': stopping verification for this epsilon.']); + res(i+1:end,e) = 2; % Mark remaining as unknown + break; % Exit the inner loop after timeout + end + end + + % Summary results, stopping, and deleting the timer should be outside the inner loop + stop(verificationTimer); + delete(verificationTimer); + + % Get summary results + N = numObs; + rob = sum(res(:,e)==1); + not_rob = sum(res(:,e) == 0); + unk = sum(res(:,e) == 2); + totalTime = sum(time(:,e)); + avgTime = totalTime/N; + + % Print results to screen + fprintf('Model: %s\n', onnxFiles(k).name); + disp("======= FAIRNESS RESULTS e: "+string(epsilon(e))+" ==========") + disp(" "); + disp("Number of fair samples = "+string(rob)+ ", equivalent to " + string(100*rob/N) + "% of the samples."); + disp("Number of non-fair samples = " +string(not_rob)+ ", equivalent to " + string(100*not_rob/N) + "% of the samples.") + disp("Number of unknown samples = "+string(unk)+ ", equivalent to " + string(100*unk/N) + "% of the samples."); + disp(" "); + disp("It took a total of "+string(totalTime) + " seconds to compute the verification results, an average of "+string(avgTime)+" seconds per sample"); + + % Collect results based on epsilon type + if epsilon(e) == 0.0 + % Counterfactual fairness results + results_counterfactual{end+1} = {modelName, 100 * rob / N, 100 * not_rob / N}; + else + % Individual fairness results (for stacked bar chart) + results_individual{end+1} = {modelName, epsilon(e), 100 * rob / N, 100 * not_rob / N, 100 * unk / N}; + end + + % Timing results (all epsilon values) + results_timing{end+1} = {modelName, epsilon(e), totalTime, avgTime}; + end + end +end + +%% Save results to CSV files +% Get the current timestamp using datetime +timestamp = datetime('now', 'Format', 'yyyyMMdd_HHmmss'); +timestampStr = char(timestamp); + +% --- Save Counterfactual Fairness Results --- +% For Table: Counterfactual Fairness (epsilon = 0) +csv_counterfactual = fullfile(resultsDir, ['fm26_counterfactual_', timestampStr, '.csv']); +fid = fopen(csv_counterfactual, 'w'); +fprintf(fid, 'Model,FairPercent,UnfairPercent\n'); +for r = 1:length(results_counterfactual) + fprintf(fid, '%s,%f,%f\n', results_counterfactual{r}{1}, results_counterfactual{r}{2}, results_counterfactual{r}{3}); +end +fclose(fid); +disp(['Counterfactual results saved to ', csv_counterfactual]); + +% --- Save Individual Fairness Results --- +% For Stacked Bar Charts (epsilon > 0) +csv_individual = fullfile(resultsDir, ['fm26_individual_', timestampStr, '.csv']); +fid = fopen(csv_individual, 'w'); +fprintf(fid, 'Model,Epsilon,FairPercent,UnfairPercent,UnknownPercent\n'); +for r = 1:length(results_individual) + fprintf(fid, '%s,%f,%f,%f,%f\n', results_individual{r}{1}, results_individual{r}{2}, results_individual{r}{3}, results_individual{r}{4}, results_individual{r}{5}); +end +fclose(fid); +disp(['Individual fairness results saved to ', csv_individual]); + +% --- Save Comprehensive Timing Table --- +csv_timing = fullfile(resultsDir, ['fm26_timing_', timestampStr, '.csv']); +fid = fopen(csv_timing, 'w'); +fprintf(fid, 'Model,Epsilon,TotalTime,AvgTimePerSample\n'); +for r = 1:length(results_timing) + fprintf(fid, '%s,%f,%f,%f\n', results_timing{r}{1}, results_timing{r}{2}, results_timing{r}{3}, results_timing{r}{4}); +end +fclose(fid); +disp(['Timing results saved to ', csv_timing]); + +disp(" "); +disp("======= FM26 VERIFICATION COMPLETE =========="); +disp("Generated files:"); +disp(" 1. " + csv_counterfactual + " (for counterfactual fairness table)"); +disp(" 2. " + csv_individual + " (for individual fairness stacked bar charts)"); +disp(" 3. " + csv_timing + " (for comprehensive timing table)"); + +%% Helper Function +% Apply perturbation (individual fairness) to sample +function IS = perturbationIF(x, epsilon, min_values, max_values) + % Applies perturbations on selected features of input sample x + % Return an ImageStar (IS) and random images from initial set + SampleSize = size(x); + + disturbance = zeros(SampleSize, "like", x); + sensitive_rows = [9]; + nonsensitive_rows = [1,10,11,12]; + + % Flip the sensitive attribute + if epsilon ~= -1 + if x(sensitive_rows) == 1 + x(sensitive_rows) = 0; + else + x(sensitive_rows) = 1; + end + end + + % Apply epsilon perturbation to non-sensitive numerical features + for i = 1:length(nonsensitive_rows) + if epsilon ~= -1 + if nonsensitive_rows(i) <= size(x, 1) + disturbance(nonsensitive_rows(i), :) = epsilon; + else + error('The input data does not have enough rows.'); + end + end + end + + % Calculate disturbed lower and upper bounds considering min and max values + lb = max(x - disturbance, min_values); + ub = min(x + disturbance, max_values); + IS = Star(single(lb), single(ub)); % default: single (assume onnx input models) + +end diff --git a/code/nnv/examples/NNV3.0/FairNNV/plot_fm26_results.m b/code/nnv/examples/NNV3.0/FairNNV/plot_fm26_results.m new file mode 100644 index 000000000..90d5f8904 --- /dev/null +++ b/code/nnv/examples/NNV3.0/FairNNV/plot_fm26_results.m @@ -0,0 +1,294 @@ +%% Plot FM26 FairNNV Results +% Generates figures and LaTeX tables from FM26 verification results +% Outputs: +% (1) LaTeX table for counterfactual fairness +% (2) Combined individual fairness area plot (smooth lines with filled regions) +% (3) LaTeX table for timing results (separated by fairness type) +% +% This script can be run standalone or called from run_fm26_fairnnv.m +% When run standalone, default paths are used. +% When called from runner, paths are set via config struct. + +%% Setup +% Check if config exists (set by runner script), otherwise use defaults +if ~exist('config', 'var') + % Default configuration for standalone execution + config.outputDir = './fm26_fairnnv_results'; + config.savePNG = true; + config.savePDF = true; +end + +resultsDir = config.outputDir; + +% Find the most recent CSV files in the results directory +counterfactual_files = dir(fullfile(resultsDir, 'fm26_counterfactual_*.csv')); +individual_files = dir(fullfile(resultsDir, 'fm26_individual_*.csv')); +timing_files = dir(fullfile(resultsDir, 'fm26_timing_*.csv')); + +% Check if files exist +if isempty(counterfactual_files) || isempty(individual_files) || isempty(timing_files) + error('CSV files not found in %s. Please run adult_verify_fm26.m first.', resultsDir); +end + +% Get the most recent files (sorted by date) +[~, idx] = max([counterfactual_files.datenum]); +csv_counterfactual = fullfile(resultsDir, counterfactual_files(idx).name); + +[~, idx] = max([individual_files.datenum]); +csv_individual = fullfile(resultsDir, individual_files(idx).name); + +[~, idx] = max([timing_files.datenum]); +csv_timing = fullfile(resultsDir, timing_files(idx).name); + +disp("Loading results from:"); +disp(" " + csv_counterfactual); +disp(" " + csv_individual); +disp(" " + csv_timing); + +%% Load CSV Data +% Counterfactual fairness data +counterfactual_data = readtable(csv_counterfactual); + +% Individual fairness data +individual_data = readtable(csv_individual); + +% Timing data +timing_data = readtable(csv_timing); + +%% Figure Settings +% Professional color scheme (matching Python matplotlib style) +% Hex colors: #2ecc71 (green), #e74c3c (red) +color_fair = [46/255, 204/255, 113/255]; % Green (#2ecc71) +color_unfair = [231/255, 76/255, 60/255]; % Red (#e74c3c) + +% Get unique models +models = unique(individual_data.Model); + +% Model display names (fuller titles for figures/tables) +% Based on actual architectures: +% AC-1: 13→16→8→2 (~350 params) - Small +% AC-3: 13→50→2 (~750 params) - Medium +% AC-4: 13→100→100→2 (~11,500 params) - Large +model_display_names = containers.Map(); +model_display_names('AC-1') = 'Adult Census - Small Model'; +model_display_names('AC-3') = 'Adult Census - Medium Model'; +model_display_names('AC-4') = 'Adult Census - Large Model'; + +%% LaTeX Table 1: Counterfactual Fairness (with timing) +disp(" "); +disp("======= COUNTERFACTUAL FAIRNESS LATEX TABLE =========="); + +latex_cf_filename = fullfile(resultsDir, 'fm26_counterfactual_table.tex'); +fid = fopen(latex_cf_filename, 'w'); + +fprintf(fid, '\\begin{table}[ht]\n'); +fprintf(fid, '\\centering\n'); +fprintf(fid, '\\caption{Counterfactual Fairness Verification Results ($\\epsilon = 0$)}\n'); +fprintf(fid, '\\label{tab:counterfactual_fairness}\n'); +fprintf(fid, '\\begin{tabular}{lccc}\n'); +fprintf(fid, '\\toprule\n'); +fprintf(fid, 'Model & Fair (\\%%) & Unfair (\\%%) & Avg. Time (s) \\\\\n'); +fprintf(fid, '\\midrule\n'); + +for r = 1:height(counterfactual_data) + modelName = counterfactual_data.Model{r}; + % Use display name if available + if isKey(model_display_names, modelName) + displayName = model_display_names(modelName); + else + displayName = modelName; + end + % Find corresponding timing (epsilon = 0) + timing_idx = strcmp(timing_data.Model, modelName) & timing_data.Epsilon == 0; + if any(timing_idx) + avg_time = timing_data.AvgTimePerSample(timing_idx); + else + avg_time = NaN; + end + fprintf(fid, '%s & %.1f & %.1f & %.4f \\\\\n', ... + displayName, ... + counterfactual_data.FairPercent(r), ... + counterfactual_data.UnfairPercent(r), ... + avg_time); +end + +fprintf(fid, '\\bottomrule\n'); +fprintf(fid, '\\end{tabular}\n'); +fprintf(fid, '\\end{table}\n'); +fclose(fid); + +% Also print to console +type(latex_cf_filename); +disp(" "); +disp("Saved: " + latex_cf_filename); + +%% Figure: Combined Individual Fairness (Stacked Area Plot - Professional Style) +n_models = length(models); +fig = figure('Name', 'Individual Fairness - All Models', 'Position', [100, 100, 600*n_models, 500]); + +for m = 1:n_models + ax = subplot(1, n_models, m); + + modelName = models{m}; + + % Filter data for this model + model_data = individual_data(strcmp(individual_data.Model, modelName), :); + + % Sort by epsilon + model_data = sortrows(model_data, 'Epsilon'); + + % Extract values + epsilons = model_data.Epsilon; + fair_pct = model_data.FairPercent; + unfair_pct = model_data.UnfairPercent; + n_eps = length(epsilons); + + % Use discrete x positions (like Python version) + x = 0:(n_eps-1); + + % Create stacked area plot (bottom to top: unfair, then fair) + % This matches the Python stacking order + y1 = unfair_pct'; % Bottom layer: Unfair + y2 = y1 + fair_pct'; % Top layer: Fair (should sum to 100) + + hold on; + + % Fill area for Unfair (bottom, from 0 to y1) + fill([x, fliplr(x)], [y1, zeros(1, n_eps)], ... + color_unfair, 'FaceAlpha', 0.9, 'EdgeColor', 'none'); + + % Fill area for Fair (top, from y1 to y2) + fill([x, fliplr(x)], [y2, fliplr(y1)], ... + color_fair, 'FaceAlpha', 0.9, 'EdgeColor', 'none'); + + % Add white edge line between areas for clarity + plot(x, y1, 'w-', 'LineWidth', 1.5); + + hold off; + + % Labels and formatting with bold fonts and larger size + xlabel('Perturbation Level (\epsilon)', 'FontWeight', 'bold', 'FontSize', 12); + ylabel('Percentage (%)', 'FontWeight', 'bold', 'FontSize', 12); + + % Use full display name for title + if isKey(model_display_names, modelName) + displayTitle = model_display_names(modelName); + else + displayTitle = modelName; + end + title(displayTitle, 'FontWeight', 'bold', 'FontSize', 14); + + % Set x-axis with epsilon labels + set(ax, 'XTick', x); + eps_labels = arrayfun(@(e) sprintf('%.2f', e), epsilons, 'UniformOutput', false); + set(ax, 'XTickLabel', eps_labels); + + % Axis limits + ylim([0 100]); + xlim([-0.3, n_eps - 0.7]); + + % Professional grid styling + grid on; + set(ax, 'GridLineStyle', '--', 'GridAlpha', 0.3); + set(ax, 'Layer', 'top'); % Grid on top + + % Add legend only to the last subplot + if m == n_models + % Reverse order to match visual (Fair on top, Unfair on bottom) + legend({'Unfair', 'Fair'}, 'Location', 'northeast', ... + 'FontWeight', 'bold', 'Box', 'on'); + end +end + +% Adjust layout +set(fig, 'Color', 'w'); + +% Save combined figure with high resolution +if config.savePNG + print(gcf, fullfile(resultsDir, 'fm26_individual_fairness_combined.png'), '-dpng', '-r300'); +end +if config.savePDF + print(gcf, fullfile(resultsDir, 'fm26_individual_fairness_combined.pdf'), '-dpdf', '-bestfit'); +end +disp("Saved: fm26_individual_fairness_combined.png/pdf"); + +%% LaTeX Table 2: Individual Fairness Timing (Horizontal Layout) +% Epsilon values as columns, models as rows +disp(" "); +disp("======= INDIVIDUAL FAIRNESS TIMING LATEX TABLE =========="); + +latex_timing_filename = fullfile(resultsDir, 'fm26_timing_table.tex'); +fid = fopen(latex_timing_filename, 'w'); + +% Get unique epsilon values for individual fairness (epsilon > 0) +individual_timing = timing_data(timing_data.Epsilon > 0, :); +epsilons_unique = unique(individual_timing.Epsilon); +n_eps = length(epsilons_unique); + +fprintf(fid, '\\begin{table}[ht]\n'); +fprintf(fid, '\\centering\n'); +fprintf(fid, '\\caption{Individual Fairness Verification Timing (seconds per sample)}\n'); +fprintf(fid, '\\label{tab:individual_timing}\n'); + +% Create column format with spacing: l for model, then c with padding for each epsilon +col_format = 'l'; +for i = 1:n_eps + col_format = [col_format '@{\hskip 8pt}c']; +end +fprintf(fid, '\\begin{tabular}{%s}\n', col_format); +fprintf(fid, '\\toprule\n'); + +% Two-row header: first row spans epsilon columns with label +fprintf(fid, ' & \\multicolumn{%d}{c}{Perturbation Level ($\\epsilon$)} \\\\\n', n_eps); +fprintf(fid, '\\cmidrule(l){2-%d}\n', n_eps + 1); + +% Second header row with just epsilon values +fprintf(fid, 'Model'); +for i = 1:n_eps + fprintf(fid, ' & %.2f', epsilons_unique(i)); +end +fprintf(fid, ' \\\\\n'); +fprintf(fid, '\\midrule\n'); + +% Data rows (one per model) with full display names +for m = 1:length(models) + modelName = models{m}; + % Use display name if available + if isKey(model_display_names, modelName) + displayName = model_display_names(modelName); + else + displayName = modelName; + end + fprintf(fid, '%s', displayName); + + for i = 1:n_eps + eps_val = epsilons_unique(i); + % Find timing for this model and epsilon + idx = strcmp(individual_timing.Model, modelName) & individual_timing.Epsilon == eps_val; + if any(idx) + avg_time = individual_timing.AvgTimePerSample(idx); + fprintf(fid, ' & %.4f', avg_time); + else + fprintf(fid, ' & --'); + end + end + fprintf(fid, ' \\\\\n'); +end + +fprintf(fid, '\\bottomrule\n'); +fprintf(fid, '\\end{tabular}\n'); +fprintf(fid, '\\end{table}\n'); +fclose(fid); + +% Also print to console +type(latex_timing_filename); +disp(" "); +disp("Saved: " + latex_timing_filename); + +%% Summary +disp(" "); +disp("======= FM26 PLOTTING COMPLETE =========="); +disp("Generated outputs in " + resultsDir + ":"); +disp(" 1. fm26_counterfactual_table.tex (LaTeX table)"); +disp(" 2. fm26_individual_fairness_combined.png/pdf (Area plot)"); +disp(" 3. fm26_timing_table.tex (LaTeX table)"); diff --git a/code/nnv/examples/NNV3.0/FairNNV/run_fm26_fairnnv.m b/code/nnv/examples/NNV3.0/FairNNV/run_fm26_fairnnv.m new file mode 100644 index 000000000..210c0d5c6 --- /dev/null +++ b/code/nnv/examples/NNV3.0/FairNNV/run_fm26_fairnnv.m @@ -0,0 +1,148 @@ +%% FM26 FairNNV - Main Runner Script +% This script runs the complete FairNNV verification pipeline for FM26. +% +% INSTRUCTIONS: +% 1. Set the paths in the CONFIGURATION section below +% 2. Run this script +% 3. Results will be saved to the specified output folder +% +% OUTPUTS: +% - CSV files with verification results +% - PNG/PDF figures for the paper +% - Timing table +% +% REQUIREMENTS: +% - NNV toolbox must be installed +% - ONNX models in the specified models folder +% - Data file (adult_data.mat) in the specified data folder + +%% ================== CONFIGURATION ================== +% Set these paths before running + +% Path to NNV root folder (contains startup_nnv.m) +% This is used to add NNV to the MATLAB path +config.nnvDir = '/home/matlab/nnv/code/nnv'; % NOTE: these paths are for the docker container + + +% Path to folder containing ONNX models (e.g., AC-1.onnx, AC-3.onnx) +% The path to the folder: ~/nnv/code/nnv/examples/Submission/ICAIF24/adult_onnx +config.modelsDir = '/home/matlab/nnv/code/nnv/examples/Submission/ICAIF24/adult_onnx'; + +% Path to folder containing data files (e.g., adult_data.mat) +% The path to the folder: ~/nnv/code/nnv/examples/Submission/ICAIF24/data +config.dataDir = '/home/matlab/nnv/code/nnv/examples/Submission/ICAIF24/data'; + +% Path to output folder for results (will be created if it doesn't exist) +config.outputDir = './fm26_fairnnv_results'; + +% Data file name +config.dataFile = 'adult_data.mat'; + +% Models to verify (must match filenames without .onnx extension) +% AC-1: 13→16→8→2 (2 hidden, narrow) +% AC-3: 13→50→2 (1 hidden, shallow) +% AC-4: 13→100→100→2 (2 hidden, wide) +config.modelList = {'AC-1', 'AC-3'}; + +% Number of samples to test (default: 100) +config.numObs = 100; + +% Random seed for reproducibility +config.randomSeed = 500; + +% Timeout per epsilon value in seconds (default: 600 = 10 minutes) +config.timeout = 600; + +% Epsilon values for verification +% 0.0 = counterfactual fairness (flip sensitive attribute only) +% >0.0 = individual fairness (flip SA + perturb numerical features) +config.epsilon_counterfactual = [0.0]; +config.epsilon_individual = [0.01, 0.02, 0.03, 0.05, 0.07, 0.1]; + +% Figure export formats (set to false to skip) +config.savePNG = true; +config.savePDF = true; + +%% ================== END CONFIGURATION ================== + +%% Initialize NNV +disp("======= FM26 FairNNV Pipeline =========="); +disp(" "); +disp("Initializing NNV toolbox..."); + +% Check if NNV directory exists +if ~exist(config.nnvDir, 'dir') + error("NNV directory not found: %s", config.nnvDir); +end + +% Add NNV to path (simplified - avoids tbxmanager permission issues) +addpath(genpath(config.nnvDir)); +disp("NNV paths added successfully."); +disp(" "); + +%% Validate Configuration +disp("Validating configuration..."); + +% Check if models directory exists +if ~exist(config.modelsDir, 'dir') + error("Models directory not found: %s", config.modelsDir); +end + +% Check if data directory exists +if ~exist(config.dataDir, 'dir') + error("Data directory not found: %s", config.dataDir); +end + +% Check if data file exists +dataFilePath = fullfile(config.dataDir, config.dataFile); +if ~exist(dataFilePath, 'file') + error("Data file not found: %s", dataFilePath); +end + +% Check if at least one model exists +modelFound = false; +for i = 1:length(config.modelList) + modelPath = fullfile(config.modelsDir, [config.modelList{i}, '.onnx']); + if exist(modelPath, 'file') + modelFound = true; + disp(" Found model: " + config.modelList{i}); + else + warning("Model not found: %s", modelPath); + end +end +if ~modelFound + error("No models found in: %s", config.modelsDir); +end + +% Create output directory if it doesn't exist +if ~exist(config.outputDir, 'dir') + mkdir(config.outputDir); + disp(" Created output directory: " + config.outputDir); +else + disp(" Output directory: " + config.outputDir); +end + +disp(" "); +disp("Configuration validated successfully."); +disp(" "); + +%% Run Verification +disp("======= STEP 1: Running Verification =========="); +disp(" "); + +run('adult_verify_fm26.m'); + +disp(" "); +disp("Verification complete."); +disp(" "); + +%% Run Plotting +disp("======= STEP 2: Generating Figures =========="); +disp(" "); + +run('plot_fm26_results.m'); + +disp(" "); +disp("======= FM26 FairNNV Pipeline Complete =========="); +disp(" "); +disp("All results saved to: " + config.outputDir); diff --git a/code/nnv/examples/NNV3.0/GNNV/figures/dashboard.pdf b/code/nnv/examples/NNV3.0/GNNV/figures/dashboard.pdf new file mode 100644 index 000000000..6f479c82a Binary files /dev/null and b/code/nnv/examples/NNV3.0/GNNV/figures/dashboard.pdf differ diff --git a/code/nnv/examples/NNV3.0/GNNV/figures/dashboard.png b/code/nnv/examples/NNV3.0/GNNV/figures/dashboard.png new file mode 100644 index 000000000..138891885 Binary files /dev/null and b/code/nnv/examples/NNV3.0/GNNV/figures/dashboard.png differ diff --git a/code/nnv/examples/NNV3.0/GNNV/figures/results_table.tex b/code/nnv/examples/NNV3.0/GNNV/figures/results_table.tex new file mode 100644 index 000000000..9663d65bd --- /dev/null +++ b/code/nnv/examples/NNV3.0/GNNV/figures/results_table.tex @@ -0,0 +1,16 @@ +\begin{table}[h] +\centering +\caption{Verification results for GNN-based power flow prediction on the IEEE 24-bus system. Percentage of voltage nodes verified safe (out of 130 total across 10 scenarios) and average time to verify all 13 voltage nodes per graph.} +\label{tab:gnn-results} +\begin{tabular}{l @{\hspace{0.8em}} cc @{\hspace{0.8em}} cc @{\hspace{0.8em}} cc} +\toprule +& \multicolumn{2}{c}{$\epsilon=0.001$} & \multicolumn{2}{c}{$\epsilon=0.005$} & \multicolumn{2}{c}{$\epsilon=0.01$} \\ +\cmidrule(lr){2-3} \cmidrule(lr){4-5} \cmidrule(lr){6-7} +Model & Verified (\%) & Time (s) & Verified (\%) & Time (s) & Verified (\%) & Time (s) \\ +\midrule +GCN & 72.3 & 1.57 & 0.8 & 3.27 & 0.0 & 5.62 \\ +GINE & 92.3 & 1.45 & 83.8 & 2.48 & 49.2 & 3.76 \\ +GINE+Edge & 84.6 & 2.10 & 56.9 & 3.29 & 33.1 & 4.96 \\ +\bottomrule +\end{tabular} +\end{table} diff --git a/code/nnv/examples/NNV3.0/GNNV/generate_cav26_dashboard.m b/code/nnv/examples/NNV3.0/GNNV/generate_cav26_dashboard.m new file mode 100644 index 000000000..0c30bc9c6 --- /dev/null +++ b/code/nnv/examples/NNV3.0/GNNV/generate_cav26_dashboard.m @@ -0,0 +1,382 @@ +function generate_cav26_dashboard(results, model_data, figuresDir, varargin) +% generate_cav26_dashboard - Create publication-quality dashboard for CAV26 +% +% Generates a single dashboard with two sections: +% - Left: GINE network topology across 3 epsilon values (0.001, 0.005, 0.01) +% - Right: Epsilon sensitivity chart comparing all models (GCN, GINE, GINE+Edge) +% +% Usage: +% generate_cav26_dashboard(results, model_data, figuresDir) +% generate_cav26_dashboard(results, model_data, figuresDir, 'layout', 'manual') +% +% Inputs: +% results - Results struct from run_gnn_experiments +% model_data - Model data struct (from gine_ieee24.mat) +% figuresDir - Output directory for figures +% +% Options: +% 'layout' - 'force' (default) or 'manual' for node positioning +% +% Output: +% figures/dashboard.pdf, dashboard.png +% +% Author: Anne Tumlin +% Date: 01/21/2026 + +%% Parse options +p = inputParser; +addParameter(p, 'layout', 'force', @(x) ismember(x, {'force', 'manual'})); +parse(p, varargin{:}); +opts = p.Results; + +%% Color scheme (colorblind-friendly) +colors = struct(); +colors.verified = [0.2, 0.65, 0.3]; % Green +colors.unknown = [0.95, 0.6, 0.1]; % Orange +colors.violated = [0.8, 0.15, 0.15]; % Red +colors.na = [0.5, 0.5, 0.5]; % Gray + +%% Get graph structure from model data +if isfield(model_data, 'src') && isfield(model_data, 'dst') + src = double(model_data.src); + dst = double(model_data.dst); + adj_list = [src, dst]; + numNodes = max([src; dst]); +elseif isfield(model_data, 'ANorm_g') + A = double(model_data.ANorm_g); + [src, dst] = find(A); + adj_list = [src, dst]; + numNodes = size(A, 1); +else + error('Cannot determine graph structure from model data'); +end + +%% Get layout coordinates +[x, y] = get_ieee24_layout(opts.layout, adj_list, numNodes); + +%% Configuration +models = results.config.models; +epsilons = results.config.epsilons; +num_scenarios = results.config.num_scenarios; + +% Total nodes for percentage calculation +total_nodes = results.data{1,1,1}.verified + results.data{1,1,1}.unknown + results.data{1,1,1}.violated; + +%% Create figure with manual positioning for clean layout +fig = figure('Position', [100, 100, 1000, 400], 'Visible', 'off'); +set(fig, 'DefaultAxesFontName', 'Times New Roman'); +set(fig, 'DefaultAxesFontSize', 10); +set(fig, 'DefaultTextFontName', 'Times New Roman'); +set(fig, 'Color', 'white'); + +%% Define layout positions (normalized coordinates [left, bottom, width, height]) +% Topology section: left 60% of figure, with margins +topo_left = 0.03; +topo_bottom = 0.18; +topo_width = 0.55; +topo_height = 0.68; +topo_panel_width = topo_width / 3; + +% Sensitivity chart: right side - aligned with topology box +sens_left = 0.65; +sens_bottom = 0.10; +sens_width = 0.32; +sens_height = 0.74; + +%% Panels 1-3: GINE Network Topology across epsilon values +model_idx = 2; % GINE model (index 2 in {'GCN', 'GINE', 'GINE+Edge'}) +scenario_idx = 1; + +% Store handles for shared legend +legend_handles = []; +topo_axes = gobjects(1, 3); + +for e = 1:length(epsilons) + % Create axis for this topology panel + ax_left = topo_left + (e-1) * topo_panel_width; + topo_axes(e) = axes('Position', [ax_left, topo_bottom, topo_panel_width, topo_height]); + hold on; + + % Get verification results for this epsilon value + exp_data = results.data{model_idx, e, scenario_idx}; + verif_results = exp_data.verif_per_node; + + % Draw edges + for i = 1:size(adj_list, 1) + s = adj_list(i, 1); + t_node = adj_list(i, 2); + if s <= length(x) && t_node <= length(x) + plot([x(s), x(t_node)], [y(s), y(t_node)], '-', ... + 'Color', [0.7, 0.7, 0.7], 'LineWidth', 0.8); + end + end + + % Draw nodes by status (for legend ordering) + h_verified = []; + h_unknown = []; + h_na = []; + + for i = 1:length(x) + if i <= length(verif_results) + status = verif_results(i); + else + status = -1; + end + + switch status + case 1 + c = colors.verified; + h = scatter(x(i), y(i), 70, c, 'filled', 'MarkerEdgeColor', 'k', 'LineWidth', 0.5); + if isempty(h_verified), h_verified = h; end + case 2 + c = colors.unknown; + h = scatter(x(i), y(i), 70, c, 'filled', 'MarkerEdgeColor', 'k', 'LineWidth', 0.5); + if isempty(h_unknown), h_unknown = h; end + case 0 + c = colors.violated; + scatter(x(i), y(i), 70, c, 'filled', 'MarkerEdgeColor', 'k', 'LineWidth', 0.5); + otherwise + c = colors.na; + h = scatter(x(i), y(i), 70, c, 'filled', 'MarkerEdgeColor', 'k', 'LineWidth', 0.5); + if isempty(h_na), h_na = h; end + end + end + + % Store handles from first panel for shared legend + if e == 1 + legend_handles = [h_verified, h_unknown, h_na]; + end + + % Add node labels + for i = 1:length(x) + text(x(i), y(i) - 0.7, sprintf('%d', i), ... + 'HorizontalAlignment', 'center', 'FontSize', 7, 'FontWeight', 'bold', ... + 'FontName', 'Times New Roman'); + end + + hold off; + axis equal; axis off; +end + +%% Add box around the topology section +box_bottom = topo_bottom - 0.08; +box_height = topo_height + 0.06; +annotation(fig, 'rectangle', [topo_left - 0.01, box_bottom, topo_width + 0.02, box_height], ... + 'LineWidth', 1.5, 'Color', [0.3, 0.3, 0.3]); + +%% Add x-axis line with tick marks at bottom of topology section +axis_y = box_bottom + 0.12; +tick_height = 0.015; + +% Draw horizontal line +annotation(fig, 'line', [topo_left, topo_left + topo_width], [axis_y, axis_y], ... + 'LineWidth', 1.2, 'Color', 'k'); + +% Add tick marks and labels for each epsilon +for e = 1:length(epsilons) + tick_x = topo_left + (e - 0.5) * topo_panel_width; % Center of each panel + % Tick mark + annotation(fig, 'line', [tick_x, tick_x], [axis_y, axis_y - tick_height], ... + 'LineWidth', 1.2, 'Color', 'k'); + % Tick label (epsilon value) + annotation(fig, 'textbox', [tick_x - 0.04, axis_y - 0.045, 0.08, 0.03], ... + 'String', sprintf('%.3f', epsilons(e)), 'EdgeColor', 'none', ... + 'HorizontalAlignment', 'center', 'FontSize', 11, ... + 'FontName', 'Times New Roman'); +end + +% Add x-axis label below tick labels +annotation(fig, 'textbox', [topo_left, axis_y - 0.095, topo_width, 0.03], ... + 'String', 'Perturbation \epsilon', 'EdgeColor', 'none', ... + 'HorizontalAlignment', 'center', 'FontSize', 10, 'FontWeight', 'bold', ... + 'FontName', 'Times New Roman'); + +%% Add titles at same level for both sections +title_y = 0.92; % Same Y position for both titles + +% Topology title with GINE marker (orange line + square to match sensitivity chart) +gine_color = [0.9, 0.6, 0.0]; % Orange - same as GINE in sensitivity chart +title_center_x = topo_left + topo_width/2; % Center of topology section + +% Title text with opening parenthesis - centered +annotation(fig, 'textbox', [topo_left - 0.02, title_y - 0.05, topo_width * 0.52, 0.06], ... + 'String', 'IEEE 24-Bus GINE (', 'EdgeColor', 'none', ... + 'HorizontalAlignment', 'right', 'FontSize', 13, 'FontWeight', 'bold', ... + 'FontName', 'Times New Roman'); + +% Add orange line segment with square marker - centered in title +marker_x = title_center_x - 0.002; +marker_y = title_y - 0.02; +line_half_width = 0.012; +annotation(fig, 'line', [marker_x - line_half_width, marker_x + line_half_width], ... + [marker_y, marker_y], 'LineWidth', 1.5, 'Color', gine_color); +% Square marker in center +annotation(fig, 'rectangle', [marker_x - 0.004, marker_y - 0.012, 0.008, 0.024], ... + 'FaceColor', gine_color, 'Color', gine_color, 'LineWidth', 1); + +% Closing parenthesis and "Verification" +annotation(fig, 'textbox', [marker_x + line_half_width - 0.005, title_y - 0.05, 0.15, 0.06], ... + 'String', ') Verification', 'EdgeColor', 'none', ... + 'HorizontalAlignment', 'left', 'FontSize', 13, 'FontWeight', 'bold', ... + 'FontName', 'Times New Roman'); + +%% Add shared legend for node verification status (below topologies) +% Create a dummy axes for the legend +ax_legend = axes('Position', [topo_left, 0.03, topo_width, 0.05], 'Visible', 'off'); +hold(ax_legend, 'on'); +h1 = scatter(ax_legend, nan, nan, 60, colors.verified, 'filled', 'MarkerEdgeColor', 'k'); +h2 = scatter(ax_legend, nan, nan, 60, colors.unknown, 'filled', 'MarkerEdgeColor', 'k'); +h3 = scatter(ax_legend, nan, nan, 60, colors.na, 'filled', 'MarkerEdgeColor', 'k'); +lgd = legend([h1, h2, h3], {'Verified Safe', 'Unknown', 'Non-Voltage Bus'}, ... + 'Orientation', 'horizontal', 'FontSize', 11, 'FontName', 'Times New Roman', ... + 'Location', 'north'); +lgd.Box = 'off'; + +%% Sensitivity Chart (right side) +ax_sens = axes('Position', [sens_left, sens_bottom, sens_width, sens_height]); +hold on; + +% Calculate total percentage: sum verified across all scenarios / (total_nodes * num_scenarios) +total_possible = total_nodes * num_scenarios; % 13 * 10 = 130 +pct_total = zeros(length(models), length(epsilons)); + +for m = 1:length(models) + for e = 1:length(epsilons) + total_verified = 0; + for s = 1:num_scenarios + total_verified = total_verified + results.data{m, e, s}.verified; + end + pct_total(m, e) = (total_verified / total_possible) * 100; + end +end + +% Plot without error bars (clean lines) +markers = {'o-', 's-', 'd-'}; +line_colors = [0.0, 0.45, 0.7; % Blue (GCN) + 0.9, 0.6, 0.0; % Orange (GINE) + 0.0, 0.6, 0.5]; % Teal (GINE+Edge) + +for m = 1:length(models) + plot(epsilons, pct_total(m, :), markers{m}, ... + 'Color', line_colors(m, :), 'LineWidth', 2.0, 'MarkerSize', 8, ... + 'MarkerFaceColor', line_colors(m, :)); +end +hold off; + +xlabel('Perturbation \epsilon', 'FontSize', 11, 'FontWeight', 'bold', 'FontName', 'Times New Roman'); +ylabel('Verified (%)', 'FontSize', 11, 'FontWeight', 'bold', 'FontName', 'Times New Roman'); +legend(models, 'Location', 'southwest', 'FontSize', 9, 'FontName', 'Times New Roman'); + +% Add title at same level as topology title (using annotation) +annotation(fig, 'textbox', [sens_left, title_y - 0.05, sens_width, 0.06], ... + 'String', 'Verification vs. Perturbation', 'EdgeColor', 'none', ... + 'HorizontalAlignment', 'center', 'FontSize', 13, 'FontWeight', 'bold', ... + 'FontName', 'Times New Roman'); +xlim([0, max(epsilons) * 1.15]); +ylim([0, 100]); +grid on; +set(gca, 'GridLineStyle', '--', 'GridAlpha', 0.3); +set(gca, 'FontName', 'Times New Roman', 'FontSize', 10); + +%% Save figure +save_figure(fig, fullfile(figuresDir, 'dashboard')); +close(fig); + +fprintf('Dashboard saved to: %s\n', figuresDir); +end + + +%% ========================================================================= +% FIGURE SAVE HELPER +% ========================================================================= + +function save_figure(fig, filepath_base) +% Save figure to PDF and PNG + + % Save PNG at moderate resolution for easier viewing + print(fig, [filepath_base, '.png'], '-dpng', '-r150'); + + % For PDF, set paper size to match figure + fig.Units = 'inches'; + fig_pos = fig.Position; + fig.PaperUnits = 'inches'; + fig.PaperSize = [fig_pos(3), fig_pos(4)]; + fig.PaperPosition = [0, 0, fig_pos(3), fig_pos(4)]; + + % Save PDF + print(fig, [filepath_base, '.pdf'], '-dpdf', '-vector'); +end + + +%% ========================================================================= +% LAYOUT FUNCTIONS +% ========================================================================= + +function [x, y] = get_ieee24_layout(method, adj_list, numNodes) +% Get x,y coordinates for IEEE 24-bus system + + switch method + case 'force' + [x, y] = force_directed_layout(adj_list, numNodes); + case 'manual' + [x, y] = manual_ieee24_layout(); + otherwise + error('Unknown layout method: %s', method); + end +end + + +function [x, y] = force_directed_layout(adj_list, numNodes) +% Compute force-directed layout using MATLAB's graph functions + + G = graph(adj_list(:,1), adj_list(:,2)); + fig_temp = figure('Visible', 'off'); + h = plot(G, 'Layout', 'force', 'Iterations', 200); + x = h.XData'; + y = h.YData'; + close(fig_temp); + + % Normalize to [0, 12] range + x = (x - min(x)) / (max(x) - min(x)) * 12; + y = (y - min(y)) / (max(y) - min(y)) * 12; +end + + +function [x, y] = manual_ieee24_layout() +% Hand-tuned coordinates for IEEE 24-bus RTS + + x = zeros(24, 1); + y = zeros(24, 1); + + % Area 1: Buses 1-10 + x(1) = 1; y(1) = 1; + x(2) = 2; y(2) = 1; + x(3) = 3; y(3) = 1; + x(4) = 2; y(4) = 2; + x(5) = 3; y(5) = 2; + x(6) = 1; y(6) = 3; + x(7) = 2; y(7) = 3; + x(8) = 3; y(8) = 3; + x(9) = 1.5; y(9) = 4; + x(10) = 2.5; y(10) = 4; + + % Area 2: Buses 11-24 + x(11) = 5; y(11) = 3; + x(12) = 5; y(12) = 4; + x(13) = 6; y(13) = 1; + x(14) = 7; y(14) = 1; + x(15) = 8; y(15) = 1; + x(16) = 6; y(16) = 2; + x(17) = 7; y(17) = 2; + x(18) = 8; y(18) = 2; + x(19) = 6; y(19) = 3; + x(20) = 7; y(20) = 3; + x(21) = 8; y(21) = 3; + x(22) = 6; y(22) = 4; + x(23) = 7; y(23) = 4; + x(24) = 8; y(24) = 4; + + % Scale + x = x * 1.1; + y = y * 2; +end diff --git a/code/nnv/examples/NNV3.0/GNNV/generate_latex_table.m b/code/nnv/examples/NNV3.0/GNNV/generate_latex_table.m new file mode 100644 index 000000000..429dcd5e7 --- /dev/null +++ b/code/nnv/examples/NNV3.0/GNNV/generate_latex_table.m @@ -0,0 +1,85 @@ +function generate_latex_table(results, figuresDir) +% generate_latex_table - Generate LaTeX table with verification percentages and timing +% +% Creates a publication-ready LaTeX table showing verification percentages +% and average verification time across all models and epsilon values. +% Uses booktabs style for professional appearance. +% +% Usage: +% generate_latex_table(results, figuresDir) +% +% Inputs: +% results - Results struct from run_gnn_experiments +% figuresDir - Output directory for the .tex file +% +% Output: +% figures/results_table.tex +% +% Author: Anne Tumlin +% Date: 01/21/2026 + +models = results.config.models; +epsilons = results.config.epsilons; +num_scenarios = results.config.num_scenarios; + +% Total nodes for percentage calculation +total_nodes = results.data{1,1,1}.verified + results.data{1,1,1}.unknown + results.data{1,1,1}.violated; +total_possible = total_nodes * num_scenarios; % 13 * 10 = 130 + +% Calculate total percentages and average times +pct_total = zeros(length(models), length(epsilons)); +avg_time = zeros(length(models), length(epsilons)); + +for m = 1:length(models) + for e = 1:length(epsilons) + total_verified = 0; + total_time = 0; + for s = 1:num_scenarios + total_verified = total_verified + results.data{m, e, s}.verified; + total_time = total_time + results.data{m, e, s}.time; + end + pct_total(m, e) = (total_verified / total_possible) * 100; + avg_time(m, e) = total_time / num_scenarios; + end +end + +% Build LaTeX table with booktabs style +fid = fopen(fullfile(figuresDir, 'results_table.tex'), 'w'); + +fprintf(fid, '\\begin{table}[h]\n'); +fprintf(fid, '\\centering\n'); +fprintf(fid, '\\caption{Verification results for GNN-based power flow prediction on the IEEE 24-bus system. '); +fprintf(fid, 'Percentage of voltage nodes verified safe (out of 130 total across 10 scenarios) '); +fprintf(fid, 'and average time to verify all 13 voltage nodes per graph.}\n'); +fprintf(fid, '\\label{tab:gnn-results}\n'); +fprintf(fid, '\\begin{tabular}{l @{\\hspace{0.8em}} cc @{\\hspace{0.8em}} cc @{\\hspace{0.8em}} cc}\n'); +fprintf(fid, '\\toprule\n'); + +% Header row 1: epsilon values spanning two columns each +fprintf(fid, '& \\multicolumn{2}{c}{$\\epsilon=%.3f$} & \\multicolumn{2}{c}{$\\epsilon=%.3f$} & \\multicolumn{2}{c}{$\\epsilon=%.2f$} \\\\\n', ... + epsilons(1), epsilons(2), epsilons(3)); + +% Add cmidrule for visual separation under epsilon headers +fprintf(fid, '\\cmidrule(lr){2-3} \\cmidrule(lr){4-5} \\cmidrule(lr){6-7}\n'); + +% Header row 2: % and Time labels +fprintf(fid, 'Model & Verified (\\%%) & Time (s) & Verified (\\%%) & Time (s) & Verified (\\%%) & Time (s) \\\\\n'); +fprintf(fid, '\\midrule\n'); + +% Data rows +for m = 1:length(models) + fprintf(fid, '%s', models{m}); + for e = 1:length(epsilons) + fprintf(fid, ' & %.1f & %.2f', pct_total(m, e), avg_time(m, e)); + end + fprintf(fid, ' \\\\\n'); +end + +fprintf(fid, '\\bottomrule\n'); +fprintf(fid, '\\end{tabular}\n'); +fprintf(fid, '\\end{table}\n'); + +fclose(fid); + +fprintf('LaTeX table saved to: %s\n', fullfile(figuresDir, 'results_table.tex')); +end diff --git a/code/nnv/examples/NNV3.0/GNNV/models/gcn_ieee24.mat b/code/nnv/examples/NNV3.0/GNNV/models/gcn_ieee24.mat new file mode 100644 index 000000000..16d70bef5 Binary files /dev/null and b/code/nnv/examples/NNV3.0/GNNV/models/gcn_ieee24.mat differ diff --git a/code/nnv/examples/NNV3.0/GNNV/models/gine_ieee24.mat b/code/nnv/examples/NNV3.0/GNNV/models/gine_ieee24.mat new file mode 100644 index 000000000..b4ca38dc2 Binary files /dev/null and b/code/nnv/examples/NNV3.0/GNNV/models/gine_ieee24.mat differ diff --git a/code/nnv/examples/NNV3.0/GNNV/regenerate_dashboard.m b/code/nnv/examples/NNV3.0/GNNV/regenerate_dashboard.m new file mode 100644 index 000000000..4f91a3855 --- /dev/null +++ b/code/nnv/examples/NNV3.0/GNNV/regenerate_dashboard.m @@ -0,0 +1,14 @@ +% regenerate_dashboard - Regenerate dashboard and table from saved results +% Useful for updating figures without re-running verification experiments + +% Load saved results +load('results/gnn_results.mat', 'results'); +load('models/gine_ieee24.mat', 'src', 'dst'); +model_data = struct('src', src, 'dst', dst); +figuresDir = 'figures'; + +% Regenerate dashboard and table +generate_cav26_dashboard(results, model_data, figuresDir); +generate_latex_table(results, figuresDir); + +fprintf('Dashboard regenerated from saved results!\n'); diff --git a/code/nnv/examples/NNV3.0/GNNV/results/gnn_results.mat b/code/nnv/examples/NNV3.0/GNNV/results/gnn_results.mat new file mode 100644 index 000000000..98be63ecf Binary files /dev/null and b/code/nnv/examples/NNV3.0/GNNV/results/gnn_results.mat differ diff --git a/code/nnv/examples/NNV3.0/GNNV/run_gnn_experiments.m b/code/nnv/examples/NNV3.0/GNNV/run_gnn_experiments.m new file mode 100644 index 000000000..97d9a6695 --- /dev/null +++ b/code/nnv/examples/NNV3.0/GNNV/run_gnn_experiments.m @@ -0,0 +1,557 @@ +function results = run_gnn_experiments(varargin) +% run_gnn_experiments - GNN verification experiments for CAV26 NNV3.0 +% +% This script demonstrates GNN verification capabilities on the IEEE 24-bus +% Power Flow prediction task using three model architectures: +% - GCN: Graph Convolutional Network +% - GINE: Graph Isomorphism Network with Edge features (node perturbation) +% - GINE+Edge: GINE with both node and edge perturbations +% +% Experiments sweep epsilon values [0.001, 0.005, 0.01] and generate +% publication-ready figures for the CAV26 repeatability package. +% +% Usage: +% run_gnn_experiments() % Run all experiments, generate figures +% run_gnn_experiments('no_figures') % Skip figure generation +% run_gnn_experiments('quiet') % Minimal output, log to file +% run_gnn_experiments('quiet', 'no_figures') % Quiet mode, no figures +% results = run_gnn_experiments() % Return results struct +% +% Outputs: +% results - Struct containing all experiment data and verification results +% +% Author: Anne Tumlin +% Date: 01/15/2026 + +%% Parse arguments +generate_figures = true; +verbose = true; + +for i = 1:nargin + if strcmpi(varargin{i}, 'no_figures') + generate_figures = false; + elseif strcmpi(varargin{i}, 'quiet') + verbose = false; + end +end + +%% Configuration +models = {'GCN', 'GINE', 'GINE+Edge'}; +epsilons = [0.001, 0.005, 0.01]; +perturb_features = [1, 2]; % Power injections only (matches GNNV) +v_min = 0.95; % Voltage spec lower bound (p.u.) +v_max = 1.05; % Voltage spec upper bound (p.u.) + +% Scenario configuration for repeatability experiments +% Note: GINE model has 1000 samples, GCN has 1500 - use minimum +num_scenarios = 10; +scenario_indices = 1:100:1000; % Evenly spaced: 1, 101, 201, ..., 901 + +% Paths (self-contained - all files in this folder) +scriptDir = fileparts(mfilename('fullpath')); +modelDir = fullfile(scriptDir, 'models'); +resultsDir = fullfile(scriptDir, 'results'); +figuresDir = fullfile(scriptDir, 'figures'); + +%% Setup logging (quiet mode writes to log file) +log_file = ''; +if ~verbose + log_file = fullfile(resultsDir, sprintf('experiment_log_%s.txt', datestr(now, 'yyyy-mm-dd_HH-MM-SS'))); + diary(log_file); +end + +%% Initialize results structure +results = struct(); +results.config = struct('models', {models}, 'epsilons', epsilons, ... + 'perturb_features', perturb_features, 'v_min', v_min, 'v_max', v_max, ... + 'num_scenarios', num_scenarios, 'scenario_indices', scenario_indices); +results.data = cell(length(models), length(epsilons), num_scenarios); + +%% Print header +if verbose + fprintf('\n'); + fprintf('================================================================\n'); + fprintf(' CAV26 GNN Verification Experiments (NNV 3.0)\n'); + fprintf('================================================================\n'); + fprintf('System: IEEE 24-bus Power Flow\n'); + fprintf('Models: %s\n', strjoin(models, ', ')); + fprintf('Node epsilon: %s\n', mat2str(epsilons)); + fprintf('Edge epsilon: 0.001 (fixed, GINE+Edge only)\n'); + fprintf('Voltage spec: [%.2f, %.2f] p.u.\n', v_min, v_max); + fprintf('Scenarios: %d (indices: %s)\n', num_scenarios, mat2str(scenario_indices)); + fprintf('Total experiments: %d\n', length(models) * length(epsilons) * num_scenarios); + fprintf('================================================================\n\n'); +end + +total_start = tic; + +%% Load models once +if verbose, fprintf('Loading models...\n'); end + +% Load GINE model +gine_path = fullfile(modelDir, 'gine_ieee24.mat'); +gine_model = load(gine_path); + +% Load GCN model +gcn_path = fullfile(modelDir, 'gcn_ieee24.mat'); +gcn_model = load(gcn_path); + +if verbose, fprintf('Models loaded successfully.\n\n'); end + +%% Run experiments +exp_count = 0; +total_experiments = length(models) * length(epsilons) * num_scenarios; + +for s = 1:num_scenarios + scenario_idx = scenario_indices(s); + if verbose, fprintf('=== Scenario %d/%d (sample index: %d) ===\n', s, num_scenarios, scenario_idx); end + + for m = 1:length(models) + model_name = models{m}; + + for e = 1:length(epsilons) + epsilon = epsilons(e); + exp_count = exp_count + 1; + + % Print experiment header (compact format) + if verbose + if strcmp(model_name, 'GINE+Edge') + fprintf('[%d/%d] %s, eps=%.3f, edge_eps=0.001: ', exp_count, total_experiments, model_name, epsilon); + else + fprintf('[%d/%d] %s, eps=%.3f: ', exp_count, total_experiments, model_name, epsilon); + end + end + exp_start = tic; + + % Run experiment based on model type + switch model_name + case 'GCN' + exp_result = run_gcn_experiment(gcn_model, epsilon, perturb_features, v_min, v_max, scenario_idx); + case 'GINE' + exp_result = run_gine_experiment(gine_model, epsilon, perturb_features, v_min, v_max, scenario_idx); + case 'GINE+Edge' + exp_result = run_gine_edge_experiment(gine_model, epsilon, perturb_features, v_min, v_max, scenario_idx); + end + + exp_result.time = toc(exp_start); + exp_result.scenario_idx = scenario_idx; + results.data{m, e, s} = exp_result; + + % Print compact summary + if verbose + fprintf('V=%d, X=%d, U=%d (%.2fs)\n', ... + exp_result.verified, exp_result.violated, exp_result.unknown, exp_result.time); + end + end + end + if verbose, fprintf('\n'); end +end + +total_time = toc(total_start); +if verbose + fprintf('================================================================\n'); + fprintf('Total time: %.2f seconds\n', total_time); + fprintf('================================================================\n\n'); +end + +%% Save results +results.total_time = total_time; +results_file = fullfile(resultsDir, 'gnn_results.mat'); +save(results_file, 'results'); +fprintf('Results saved to: %s\n', results_file); + +%% Generate figures and LaTeX table +if generate_figures + if verbose, fprintf('\nGenerating dashboard and LaTeX table...\n'); end + + % Generate combined dashboard (topology + sensitivity) + generate_cav26_dashboard(results, gine_model, figuresDir, 'layout', 'force'); + + % Generate LaTeX results table (percentages) + generate_latex_table(results, figuresDir); + + if verbose, fprintf('Outputs saved to: %s\n', figuresDir); end +end + +%% Print summary table with mean ± std across scenarios +fprintf('\n'); +fprintf('================================================================\n'); +fprintf(' RESULTS SUMMARY (mean ± std over %d scenarios)\n', num_scenarios); +fprintf('================================================================\n'); +fprintf('%-12s | ', 'Model'); +for e = 1:length(epsilons) + fprintf(' eps=%.3f | ', epsilons(e)); +end +fprintf('\n'); +fprintf('%-12s-+-', repmat('-', 1, 12)); +for e = 1:length(epsilons) + fprintf('-------------+-'); +end +fprintf('\n'); + +for m = 1:length(models) + fprintf('%-12s | ', models{m}); + for e = 1:length(epsilons) + % Collect verified counts across all scenarios + verified_counts = zeros(1, num_scenarios); + for s = 1:num_scenarios + verified_counts(s) = results.data{m, e, s}.verified; + end + mean_v = mean(verified_counts); + std_v = std(verified_counts); + fprintf('%5.1f ± %4.1f | ', mean_v, std_v); + end + fprintf('\n'); +end +fprintf('================================================================\n'); + +% Also print total nodes for reference +fprintf('Note: Total voltage-output nodes per scenario: %d\n', ... + results.data{1,1,1}.verified + results.data{1,1,1}.unknown + results.data{1,1,1}.violated); + +%% Close logging +if ~verbose + diary off; + fprintf('Log saved to: %s\n', log_file); +end + +end + + +%% ========================================================================= +% EXPERIMENT FUNCTIONS +% ========================================================================= + +function result = run_gcn_experiment(model, epsilon, perturb_features, v_min, v_max, scenario_idx) +% Run GCN verification experiment + + % Extract weights + params = model.best_params; + W1 = double(gather(params.mult1.Weights)); + W2 = double(gather(params.mult2.Weights)); + W3 = double(gather(params.mult3.Weights)); + + % Extract bias from model (if present), otherwise use zeros + if isfield(params.mult1, 'Bias') + b1 = double(extractdata(gather(params.mult1.Bias))); + b2 = double(extractdata(gather(params.mult2.Bias))); + b3 = double(extractdata(gather(params.mult3.Bias))); + else + b1 = zeros(size(W1, 2), 1); + b2 = zeros(size(W2, 2), 1); + b3 = zeros(size(W3, 2), 1); + end + + % Create layers with ReLU activations + L1 = GCNLayer('gcn1', W1, b1); + R1 = ReluLayer(); + L2 = GCNLayer('gcn2', W2, b2); + R2 = ReluLayer(); + L3 = GCNLayer('gcn3', W3, b3); + R3 = ReluLayer(); + + % Graph structure + A_norm = double(model.ANorm_g); + X = double(model.X_test_g{scenario_idx}); + numNodes = size(X, 1); + + % Create GNN + gnn = GNN({L1, R1, L2, R2, L3, R3}, A_norm); + + % Create input perturbation + GS_in = create_node_perturbation(X, epsilon, perturb_features); + + % Compute reachability (quiet mode) + reachOpts = struct('reachMethod', 'approx-star'); + t_reach = tic; + GS_out = gnn.reach(GS_in, reachOpts); + reach_time = toc(t_reach); + + % Get bounds + [lb_out, ub_out] = GS_out.getRanges(); + + % Verify voltage spec + verif_results = verify_voltage_spec(GS_out, model, v_min, v_max, scenario_idx); + + % Extract voltage-specific bounds for figures + voltage_idx = 3; % Voltage magnitude index in output + voltage_lb = lb_out(:, voltage_idx); + voltage_ub = ub_out(:, voltage_idx); + + % Convert to physical units for visualization + voltage_lb_phys = voltage_lb * model.global_std_labels(voltage_idx) + model.global_mean_labels(voltage_idx); + voltage_ub_phys = voltage_ub * model.global_std_labels(voltage_idx) + model.global_mean_labels(voltage_idx); + + % Package results + result = struct(); + result.reach_time = reach_time; + result.verified = sum(verif_results == 1); + result.violated = sum(verif_results == 0); + result.unknown_boundary = sum(verif_results == 2); + result.unknown_timeout = sum(verif_results == 3); + result.unknown = result.unknown_boundary + result.unknown_timeout; + result.mean_width = mean(ub_out(:) - lb_out(:)); + result.max_width = max(ub_out(:) - lb_out(:)); + + % Store per-node data for figures + result.verif_per_node = verif_results; + result.voltage_bounds = [voltage_lb_phys, voltage_ub_phys]; + result.bound_widths = ub_out(:, voltage_idx) - lb_out(:, voltage_idx); +end + + +function result = run_gine_experiment(model, epsilon, perturb_features, v_min, v_max, scenario_idx) +% Run GINE verification experiment (node perturbation only) + + % Extract weights + params = model.best_params; + W_node1 = double(gather(params.mult1.Weights)); + W_node2 = double(gather(params.mult2.Weights)); + W_node3 = double(gather(params.mult3.Weights)); + W_edge1 = double(gather(params.edge1.Weights)); + W_edge2 = double(gather(params.edge2.Weights)); + W_edge3 = double(gather(params.edge3.Weights)); + + b_node1 = zeros(size(W_node1, 2), 1); + b_node2 = zeros(size(W_node2, 2), 1); + b_node3 = zeros(size(W_node3, 2), 1); + b_edge1 = zeros(size(W_edge1, 2), 1); + b_edge2 = zeros(size(W_edge2, 2), 1); + b_edge3 = zeros(size(W_edge3, 2), 1); + + % Create layers + L1 = GINELayer('gine1', W_node1, b_node1, W_edge1, b_edge1); + L2 = GINELayer('gine2', W_node2, b_node2, W_edge2, b_edge2); + L3 = GINELayer('gine3', W_node3, b_node3, W_edge3, b_edge3); + + % Graph structure + src = double(model.src); + dst = double(model.dst); + adj_list = [src, dst]; + E = double(model.E_edge); + edge_weights = double(model.a); + X = double(model.X_test_g{scenario_idx}); + + % Create GNN + gnn = GNN({L1, L2, L3}, [], adj_list, E, edge_weights); + + % Create input perturbation + GS_in = create_node_perturbation(X, epsilon, perturb_features); + + % Compute reachability (quiet mode) + reachOpts = struct('reachMethod', 'approx-star'); + t_reach = tic; + GS_out = gnn.reach(GS_in, reachOpts); + reach_time = toc(t_reach); + + % Get bounds + [lb_out, ub_out] = GS_out.getRanges(); + + % Verify voltage spec + verif_results = verify_voltage_spec(GS_out, model, v_min, v_max, scenario_idx); + + % Extract voltage-specific bounds for figures + voltage_idx = 3; % Voltage magnitude index in output + voltage_lb = lb_out(:, voltage_idx); + voltage_ub = ub_out(:, voltage_idx); + + % Convert to physical units for visualization + voltage_lb_phys = voltage_lb * model.global_std_labels(voltage_idx) + model.global_mean_labels(voltage_idx); + voltage_ub_phys = voltage_ub * model.global_std_labels(voltage_idx) + model.global_mean_labels(voltage_idx); + + % Package results + result = struct(); + result.reach_time = reach_time; + result.verified = sum(verif_results == 1); + result.violated = sum(verif_results == 0); + result.unknown_boundary = sum(verif_results == 2); + result.unknown_timeout = sum(verif_results == 3); + result.unknown = result.unknown_boundary + result.unknown_timeout; + result.mean_width = mean(ub_out(:) - lb_out(:)); + result.max_width = max(ub_out(:) - lb_out(:)); + + % Store per-node data for figures + result.verif_per_node = verif_results; + result.voltage_bounds = [voltage_lb_phys, voltage_ub_phys]; + result.bound_widths = ub_out(:, voltage_idx) - lb_out(:, voltage_idx); +end + + +function result = run_gine_edge_experiment(model, epsilon, perturb_features, v_min, v_max, scenario_idx) +% Run GINE verification experiment (node + edge perturbation) + + % Extract weights + params = model.best_params; + W_node1 = double(gather(params.mult1.Weights)); + W_node2 = double(gather(params.mult2.Weights)); + W_node3 = double(gather(params.mult3.Weights)); + W_edge1 = double(gather(params.edge1.Weights)); + W_edge2 = double(gather(params.edge2.Weights)); + W_edge3 = double(gather(params.edge3.Weights)); + + b_node1 = zeros(size(W_node1, 2), 1); + b_node2 = zeros(size(W_node2, 2), 1); + b_node3 = zeros(size(W_node3, 2), 1); + b_edge1 = zeros(size(W_edge1, 2), 1); + b_edge2 = zeros(size(W_edge2, 2), 1); + b_edge3 = zeros(size(W_edge3, 2), 1); + + % Create layers + L1 = GINELayer('gine1', W_node1, b_node1, W_edge1, b_edge1); + L2 = GINELayer('gine2', W_node2, b_node2, W_edge2, b_edge2); + L3 = GINELayer('gine3', W_node3, b_node3, W_edge3, b_edge3); + + % Graph structure + src = double(model.src); + dst = double(model.dst); + adj_list = [src, dst]; + E = double(model.E_edge); + edge_weights = double(model.a); + X = double(model.X_test_g{scenario_idx}); + numEdges = size(adj_list, 1); + + % Create node perturbation + GS_in = create_node_perturbation(X, epsilon, perturb_features); + + % Create edge perturbation (fixed at 0.001, independent of node epsilon) + epsilon_edge = 0.001; % Fixed edge perturbation + perturb_edge_features = [1]; % First edge feature (impedance) + range_per_edge_col = max(E) - min(E); + eps_matrix_edge = zeros(numEdges, size(E, 2)); + for f = perturb_edge_features + if f <= size(E, 2) + eps_matrix_edge(:, f) = range_per_edge_col(f) * epsilon_edge; + end + end + E_star = GraphStar(E, -eps_matrix_edge, eps_matrix_edge); + + % Create GNN with edge perturbation + gnn = GNN({L1, L2, L3}, [], adj_list, E_star, edge_weights); + + % Compute reachability (quiet mode) + reachOpts = struct('reachMethod', 'approx-star'); + t_reach = tic; + GS_out = gnn.reach(GS_in, reachOpts); + reach_time = toc(t_reach); + + % Get bounds + [lb_out, ub_out] = GS_out.getRanges(); + + % Verify voltage spec + verif_results = verify_voltage_spec(GS_out, model, v_min, v_max, scenario_idx); + + % Extract voltage-specific bounds for figures + voltage_idx = 3; % Voltage magnitude index in output + voltage_lb = lb_out(:, voltage_idx); + voltage_ub = ub_out(:, voltage_idx); + + % Convert to physical units for visualization + voltage_lb_phys = voltage_lb * model.global_std_labels(voltage_idx) + model.global_mean_labels(voltage_idx); + voltage_ub_phys = voltage_ub * model.global_std_labels(voltage_idx) + model.global_mean_labels(voltage_idx); + + % Package results + result = struct(); + result.reach_time = reach_time; + result.verified = sum(verif_results == 1); + result.violated = sum(verif_results == 0); + result.unknown_boundary = sum(verif_results == 2); + result.unknown_timeout = sum(verif_results == 3); + result.unknown = result.unknown_boundary + result.unknown_timeout; + result.mean_width = mean(ub_out(:) - lb_out(:)); + result.max_width = max(ub_out(:) - lb_out(:)); + + % Store per-node data for figures + result.verif_per_node = verif_results; + result.voltage_bounds = [voltage_lb_phys, voltage_ub_phys]; + result.bound_widths = ub_out(:, voltage_idx) - lb_out(:, voltage_idx); +end + + +%% ========================================================================= +% HELPER FUNCTIONS +% ========================================================================= + +function GS = create_node_perturbation(X, epsilon, perturb_features) +% Create GraphStar with selective feature perturbation + + numNodes = size(X, 1); + range_per_col = max(X) - min(X); + eps_matrix = zeros(numNodes, size(X, 2)); + + for f = perturb_features + if f <= size(X, 2) + eps_matrix(:, f) = range_per_col(f) * epsilon; + end + end + + GS = GraphStar(X, -eps_matrix, eps_matrix); +end + + +%% ========================================================================= +% VERIFICATION FUNCTION (embedded for self-containment) +% ========================================================================= + +function results = verify_voltage_spec(GS_out, model_data, v_min, v_max, scenario_idx) +% verify_voltage_spec - Verify voltage magnitude bounds on GNN output +% +% Uses LP-based verification (verify_specification) for precise results, +% with fallback to interval bounds when LP returns unknown. + + voltage_idx = 3; % Index of voltage magnitude in output features + bus_type_idx = 4; % Index of bus_type in input features + + % Normalize physical voltage bounds to model space + v_min_norm = (v_min - model_data.global_mean_labels(voltage_idx)) / ... + model_data.global_std_labels(voltage_idx); + v_max_norm = (v_max - model_data.global_mean_labels(voltage_idx)) / ... + model_data.global_std_labels(voltage_idx); + + % Identify voltage-output nodes (bus_type == 1) + X_physical = model_data.X_test_g{scenario_idx} .* model_data.global_std + model_data.global_mean; + voltage_mask = (X_physical(:, bus_type_idx) == 1); + + numNodes = size(GS_out.V, 1); + numFeatures = size(GS_out.V, 2); + results = zeros(numNodes, 1); + + % Convert GraphStar to Star for verification + Y_star = GS_out.toStar(); + + for i = 1:numNodes + if ~voltage_mask(i) + results(i) = -1; % Not applicable (not a voltage-output node) + continue; + end + + % Extract the i-th node's features as a Star set + matIdx = zeros(1, numNodes * numFeatures); + flat_idx = (voltage_idx - 1) * numNodes + i; + matIdx(flat_idx) = 1; + + % Extract 1D Star for this node's voltage feature + Y_node = Y_star.affineMap(matIdx, []); + + % Create halfspace constraints for voltage bounds + G = [1; -1]; + g = [v_max_norm; -v_min_norm]; + Hs = [HalfSpace(G(1,:), g(1)); HalfSpace(G(2,:), g(2))]; + + % LP-based verification + res = verify_specification(Y_node, Hs); + + % Fallback to interval bounds if LP returns unknown + if res == 2 + [lb, ub] = Y_node.getRanges; + if lb(1) >= v_min_norm && ub(1) <= v_max_norm + res = 1; % Verified safe - bounds fully within spec + elseif ub(1) < v_min_norm || lb(1) > v_max_norm + res = 0; % Violated - bounds fully outside spec + else + res = 2; % Unknown - bounds cross spec boundary + end + end + + results(i) = res; + end +end diff --git a/code/nnv/examples/NNV3.0/ProbVer/run_probver.m b/code/nnv/examples/NNV3.0/ProbVer/run_probver.m new file mode 100644 index 000000000..3a0917cc9 --- /dev/null +++ b/code/nnv/examples/NNV3.0/ProbVer/run_probver.m @@ -0,0 +1,426 @@ +%% run_probver.m - YOLO Benchmark Verification Script +% Standalone script for running probabilistic verification on the yolo_2023 benchmark +% using the cp-star reachability method. +% +% PREREQUISITES: Run startup_nnv.m from the NNV root directory first, or +% this script will attempt to do it automatically. + +%% ========== CONFIGURATION ========== +numSamples = 3; % Number of instances to verify +randomSeed = 42; % Seed for reproducibility +nRand = 100; % Number of random samples for falsification + +%% ========== SETUP PATHS ========== +scriptDir = fileparts(mfilename('fullpath')); +benchmarkDir = fullfile(scriptDir, 'yolo_2023'); +onnxDir = fullfile(benchmarkDir, 'onnx'); +vnnlibDir = fullfile(benchmarkDir, 'vnnlib'); +instancesFile = fullfile(benchmarkDir, 'instances.csv'); +resultsFile = fullfile(scriptDir, 'results_summary.csv'); + +%% ========== DECOMPRESS FILES IF NEEDED ========== +disp('Checking for compressed files...'); + +% Decompress ONNX model if needed +onnxFile = fullfile(onnxDir, 'TinyYOLO.onnx'); +onnxGzFile = fullfile(onnxDir, 'TinyYOLO.onnx.gz'); +if ~isfile(onnxFile) && isfile(onnxGzFile) + disp('Decompressing TinyYOLO.onnx.gz...'); + gunzip(onnxGzFile, onnxDir); +end + +% Decompress all vnnlib files if needed +vnnlibGzFiles = dir(fullfile(vnnlibDir, '*.vnnlib.gz')); +for i = 1:length(vnnlibGzFiles) + gzFile = fullfile(vnnlibDir, vnnlibGzFiles(i).name); + uncompressedFile = fullfile(vnnlibDir, erase(vnnlibGzFiles(i).name, '.gz')); + if ~isfile(uncompressedFile) + disp(['Decompressing ' vnnlibGzFiles(i).name '...']); + gunzip(gzFile, vnnlibDir); + end +end + +%% ========== PARSE INSTANCES.CSV ========== +disp('Reading instances.csv...'); +fid = fopen(instancesFile, 'r'); +instances = {}; +while ~feof(fid) + line = fgetl(fid); + if ischar(line) && ~isempty(strtrim(line)) + parts = strsplit(line, ','); + if length(parts) >= 3 + instances{end+1} = struct(... + 'onnx', strtrim(parts{1}), ... + 'vnnlib', strtrim(parts{2}), ... + 'timeout', str2double(parts{3})); + end + end +end +fclose(fid); + +totalInstances = length(instances); +disp(['Found ' num2str(totalInstances) ' instances']); + +% Randomly select instances with seeded RNG for reproducibility +rng(randomSeed); +numSamples = min(numSamples, totalInstances); +selectedIndices = randperm(totalInstances, numSamples); +selectedIndices = sort(selectedIndices); % Sort for cleaner output +disp(['Randomly selected instances (seed=' num2str(randomSeed) '): ' mat2str(selectedIndices)]); + +%% ========== LOAD NETWORK (once for all instances) ========== +disp('Loading TinyYOLO network...'); +onnxPath = fullfile(benchmarkDir, 'onnx', 'TinyYOLO.onnx'); +net = importNetworkFromONNX(onnxPath, "InputDataFormats", "BCSS"); + +try + nnvnet = matlab2nnv(net); +catch + nnvnet = ""; +end + +inputSize = net.Layers(1, 1).InputSize; +inputFormat = "default"; +needReshape = 2; + +% YOLO-specific reachability options (cp-star) +reachOptions = struct; +reachOptions.train_epochs = 200; +reachOptions.train_lr = 0.0001; +reachOptions.coverage = 0.999; +reachOptions.confidence = 0.999; +reachOptions.train_mode = 'Linear'; +reachOptions.surrogate_dim = [-1, -1]; +reachOptions.threshold_normal = 1e-5; +reachOptions.reachMethod = 'cp-star'; +reachOptionsList{1} = reachOptions; + +disp('Network loaded successfully.'); +disp(['Input size: ' mat2str(inputSize)]); + +%% ========== MAIN VERIFICATION LOOP ========== +results = cell(numSamples, 1); +totalStartTime = tic; + +for i = 1:numSamples + idx = selectedIndices(i); + instance = instances{idx}; + + disp(' '); + disp(['========== Instance ' num2str(idx) '/' num2str(totalInstances) ' (' num2str(i) '/' num2str(numSamples) ') ==========']); + disp(['VNNLIB: ' instance.vnnlib]); + + result = struct(); + result.index = idx; + result.onnx = instance.onnx; + result.vnnlib = instance.vnnlib; + result.status = 'unknown'; + result.statusCode = 2; % 0=sat, 1=unsat, 2=unknown, -1=error + result.time = 0; + result.error = ''; + + try + t = tic; + status = 2; % unknown + + % Load property to verify + vnnlibPath = fullfile(benchmarkDir, instance.vnnlib); + property = load_vnnlib(vnnlibPath); + lb = property.lb; + ub = property.ub; + prop = property.prop; + + %% Falsification (SAT check) + counterEx = nan; + if ~isa(lb, "cell") && length(prop) == 1 + counterEx = falsify_single(net, lb, ub, inputSize, nRand, prop{1}.Hg, needReshape, inputFormat); + elseif isa(lb, "cell") && length(lb) == length(prop) + for spc = 1:length(lb) + counterEx = falsify_single(net, lb{spc}, ub{spc}, inputSize, nRand, prop{spc}.Hg, needReshape, inputFormat); + if iscell(counterEx) + break + end + end + elseif isa(lb, "cell") && length(prop) == 1 + for arr = 1:length(lb) + counterEx = falsify_single(net, lb{arr}, ub{arr}, inputSize, nRand, prop{1}.Hg, needReshape, inputFormat); + if iscell(counterEx) + break + end + end + end + + cEX_time = toc(t); + + if iscell(counterEx) + status = 0; % SAT (property violated) + disp(['Counterexample found in ' num2str(cEX_time) 's']); + else + %% Reachability (UNSAT check) + vT = tic; + + if ~isa(lb, "cell") && length(prop) == 1 + if ~nnz(lb-ub) + status = 1; % verified (point input) + else + IS = create_input_set(lb, ub, inputSize, needReshape); + ySet = Prob_reach(net, IS, reachOptions); + status = verify_specification(ySet, prop); + end + elseif isa(lb, "cell") && length(lb) == length(prop) + local_status = 2*ones(length(lb), 1); + for spc = 1:length(lb) + lb_spc = lb{spc}; + ub_spc = ub{spc}; + if ~nnz(lb_spc - ub_spc) + local_status(spc) = 1; + else + IS = create_input_set(lb_spc, ub_spc, inputSize, needReshape); + ySet = Prob_reach(net, IS, reachOptions); + if isempty(ySet.C) + dd = ySet.V; DD = ySet.V; + ySet = Star(dd, DD); + end + local_status(spc) = verify_specification(ySet, prop(spc)); + end + end + if all(local_status == 1) + status = 1; + else + status = 2; + end + elseif isa(lb, "cell") && length(prop) == 1 + local_status = 2*ones(length(lb), 1); + for spc = 1:length(lb) + lb_spc = lb{spc}; + ub_spc = ub{spc}; + if ~nnz(lb_spc - ub_spc) + local_status(spc) = 1; + else + IS = create_input_set(lb_spc, ub_spc, inputSize, needReshape); + ySet = Prob_reach(net, IS, reachOptions); + tempStatus = verify_specification(ySet, prop(spc)); + local_status(spc) = tempStatus; + end + end + if all(local_status == 1) + status = 1; + else + status = 2; + end + end + + vT = toc(vT); + disp(['Reachability time: ' num2str(vT) 's']); + end + + tTime = toc(t); + + % Update result + result.statusCode = status; + if status == 0 + result.status = 'sat'; + elseif status == 1 + result.status = 'unsat'; + else + result.status = 'unknown'; + end + result.time = tTime; + + disp(['Result: ' result.status ' (' num2str(tTime) 's)']); + + catch ME + result.statusCode = -1; + result.status = 'error'; + result.error = ME.message; + result.time = toc(t); + disp(['ERROR: ' ME.message]); + end + + results{i} = result; +end + +totalTime = toc(totalStartTime); + +%% ========== SAVE AND DISPLAY RESULTS ========== +disp(' '); +disp('========== RESULTS SUMMARY =========='); + +% Count results +satCount = 0; +unsatCount = 0; +unknownCount = 0; +errorCount = 0; + +for i = 1:length(results) + r = results{i}; + switch r.status + case 'sat' + satCount = satCount + 1; + case 'unsat' + unsatCount = unsatCount + 1; + case 'unknown' + unknownCount = unknownCount + 1; + case 'error' + errorCount = errorCount + 1; + end +end + +disp(['Total instances: ' num2str(length(results))]); +disp([' SAT (violated): ' num2str(satCount)]); +disp([' UNSAT (verified): ' num2str(unsatCount)]); +disp([' Unknown: ' num2str(unknownCount)]); +disp([' Errors: ' num2str(errorCount)]); +disp(['Total time: ' num2str(totalTime) 's']); + +% Save to CSV +disp(' '); +disp(['Saving results to ' resultsFile '...']); +fid = fopen(resultsFile, 'w'); +fprintf(fid, 'index,onnx,vnnlib,status,time,error\n'); +for i = 1:length(results) + r = results{i}; + % Escape any commas in error message + errorMsg = strrep(r.error, ',', ';'); + errorMsg = strrep(errorMsg, newline, ' '); + fprintf(fid, '%d,%s,%s,%s,%.4f,%s\n', r.index, r.onnx, r.vnnlib, r.status, r.time, errorMsg); +end +fclose(fid); +disp('Results saved.'); + +% Display errors if any +if errorCount > 0 + disp(' '); + disp('========== ERRORS =========='); + for i = 1:length(results) + r = results{i}; + if strcmp(r.status, 'error') + disp(['Instance ' num2str(r.index) ': ' r.error]); + end + end +end + +%% ========== HELPER FUNCTIONS ========== + +function IS = create_input_set(lb, ub, inputSize, needReshape) + % Get input bounds + if ~isscalar(inputSize) + lb = reshape(lb, inputSize); + ub = reshape(ub, inputSize); + end + + % Format bounds into correct dimensions + if needReshape == 1 + lb = permute(lb, [2 1 3]); + ub = permute(ub, [2 1 3]); + elseif needReshape == 2 + newSize = [inputSize(2) inputSize(1) inputSize(3:end)]; + lb = reshape(lb, newSize); + lb = permute(lb, [2 1 3 4]); + ub = reshape(ub, newSize); + ub = permute(ub, [2 1 3 4]); + end + + % Create input set + IS = ImageStar(lb, ub); + + % Delete constraints for non-interval dimensions + try + xxx = find((lb-ub)); + xxx = reshape(xxx, [], 1); + if numel(lb) ~= length(xxx) + IS.C = IS.C(:,xxx); + IS.pred_lb = IS.pred_lb(xxx); + IS.pred_ub = IS.pred_ub(xxx); + xxx = xxx + 1; + IS.V = IS.V(:,:,:,[1;xxx]); + IS.numPred = length(xxx); + end + end +end + +function xRand = create_random_examples(net, lb, ub, nR, inputSize, needReshape, inputFormat) + xB = Box(lb, ub); + xRand = xB.sample(nR-2); + xRand = [lb, ub, xRand]; + if needReshape + if needReshape == 2 + newSize = [inputSize(2) inputSize(1) inputSize(3:end)]; + xRand = reshape(xRand, [newSize nR]); + xRand = permute(xRand, [2 1 3 4]); + else + xRand = reshape(xRand, [inputSize nR]); + xRand = permute(xRand, [2 1 3 4]); + end + else + xRand = reshape(xRand, [inputSize nR]); + end + if isa(net, 'dlnetwork') + if strcmp(inputFormat, "default") + if isa(net.Layers(1, 1), 'nnet.cnn.layer.ImageInputLayer') + xRand = dlarray(xRand, "SSCB"); + elseif isa(net.Layers(1, 1), 'nnet.cnn.layer.FeatureInputLayer') || isa(net.Layers(1, 1), 'nnet.onnx.layer.FeatureInputLayer') + xRand = dlarray(xRand, "CB"); + else + disp(net.Layers(1,1)); + error("Unknown input format"); + end + else + if contains(inputFormat, "U") + xRand = dlarray(xRand, inputFormat+"U"); + else + xRand = dlarray(xRand, inputFormat); + end + end + end +end + +function counterEx = falsify_single(net, lb, ub, inputSize, nRand, Hs, needReshape, inputFormat) + counterEx = nan; + xRand = create_random_examples(net, lb, ub, nRand, inputSize, needReshape, inputFormat); + s = size(xRand); + n = length(s); + for i = 1:s(n) + x = get_example(xRand, i); + try + yPred = predict(net, x); + if isa(x, 'dlarray') + x = extractdata(x); + yPred = extractdata(yPred); + end + yPred = reshape(yPred, [], 1); + for h = 1:length(Hs) + if Hs(h).contains(double(yPred)) + n = numel(x); + if needReshape == 2 + x = permute(x, [2 1 3]); + elseif needReshape == 1 + if ndims(x) == 3 + x = permute(x, [2 1 3]); + end + end + counterEx = {x; yPred}; + return; + end + end + end + end +end + +function x = get_example(xRand, i) + s = size(xRand); + n = length(s); + if n == 4 + x = xRand(:,:,:,i); + elseif n == 3 + x = xRand(:,:,i); + elseif n == 2 + x = xRand(:,i); + xsize = size(x); + if xsize(1) ~= 1 && ~isa(x, "dlarray") + x = x'; + end + else + error("InputSize = " + string(s)); + end +end diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/instances.csv b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/instances.csv new file mode 100644 index 000000000..9703fb841 --- /dev/null +++ b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/instances.csv @@ -0,0 +1,72 @@ +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000005_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000459_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000290_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000257_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000367_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000039_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000082_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000296_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000034_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000448_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000221_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000040_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000118_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000359_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000006_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000004_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000316_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000080_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000161_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000081_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000425_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000324_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000439_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000306_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000302_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000220_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000101_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000420_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000036_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000447_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000103_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000266_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000047_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000015_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000284_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000201_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000323_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000395_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000450_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000308_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000159_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000370_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000217_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000299_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000401_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000046_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000139_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000024_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000249_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000148_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000196_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000277_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000262_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000298_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000336_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000453_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000405_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000062_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000165_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000357_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000037_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000341_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000271_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000144_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000170_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000060_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000129_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000356_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000261_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000225_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000181_eps_1_255.vnnlib,300 +onnx/TinyYOLO.onnx,vnnlib/TinyYOLO_prop_000312_eps_1_255.vnnlib,300 diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/onnx/TinyYOLO.onnx.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/onnx/TinyYOLO.onnx.gz new file mode 100644 index 000000000..c566cc2b5 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/onnx/TinyYOLO.onnx.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000004_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000004_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..d7b4daf5d Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000004_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000005_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000005_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..35684527f Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000005_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000006_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000006_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..a4f260b4d Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000006_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000015_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000015_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..fe81abde3 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000015_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000024_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000024_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..ab19a02f4 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000024_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000034_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000034_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..25815cf5c Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000034_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000036_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000036_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..381f1357c Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000036_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000037_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000037_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..a518cc114 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000037_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000039_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000039_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..d9484231f Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000039_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000040_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000040_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..9a5441ee9 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000040_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000046_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000046_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..9ac7b45eb Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000046_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000047_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000047_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..cfb8a60a9 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000047_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000060_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000060_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..12e76134c Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000060_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000062_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000062_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..3b92ce18b Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000062_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000080_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000080_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..d47fda558 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000080_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000081_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000081_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..81ae95ab8 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000081_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000082_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000082_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..6f6a101c5 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000082_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000101_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000101_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..a205d9935 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000101_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000103_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000103_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..d7d11199b Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000103_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000118_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000118_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..34127dd87 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000118_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000129_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000129_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..25e3da54d Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000129_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000139_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000139_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..4797b535b Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000139_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000144_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000144_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..26ff3464a Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000144_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000148_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000148_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..f18480382 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000148_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000159_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000159_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..360fe9ad7 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000159_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000161_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000161_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..bf578d6b9 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000161_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000165_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000165_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..e81101770 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000165_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000170_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000170_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..f8016b12a Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000170_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000181_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000181_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..127f4b047 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000181_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000196_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000196_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..0f066aabf Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000196_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000201_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000201_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..18a99e318 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000201_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000217_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000217_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..e030c05e3 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000217_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000220_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000220_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..032dbb6c5 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000220_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000221_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000221_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..e39ac8f34 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000221_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000225_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000225_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..b6e8dba87 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000225_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000249_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000249_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..f57807bad Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000249_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000257_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000257_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..64886c0bb Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000257_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000261_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000261_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..5aa197b52 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000261_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000262_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000262_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..886d6dc74 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000262_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000266_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000266_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..b1c6f51a1 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000266_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000271_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000271_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..0edc39ea6 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000271_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000277_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000277_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..aaad6c8e8 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000277_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000284_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000284_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..20e0db7c0 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000284_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000290_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000290_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..abe777273 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000290_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000296_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000296_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..ae9335207 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000296_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000298_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000298_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..4c13c69d2 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000298_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000299_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000299_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..6c55fdb2c Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000299_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000302_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000302_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..cf5b873e4 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000302_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000306_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000306_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..514563094 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000306_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000308_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000308_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..a7b88cf6b Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000308_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000312_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000312_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..bcb128aab Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000312_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000316_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000316_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..5a4be9a6a Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000316_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000323_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000323_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..aae8b95d6 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000323_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000324_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000324_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..117a727d9 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000324_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000336_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000336_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..d3ed3982a Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000336_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000341_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000341_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..144a25160 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000341_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000356_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000356_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..9c6dd1b77 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000356_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000357_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000357_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..2e1fff95b Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000357_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000359_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000359_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..1f90dc21a Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000359_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000367_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000367_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..0fa410620 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000367_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000370_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000370_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..be14176d1 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000370_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000395_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000395_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..b50e43f1e Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000395_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000401_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000401_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..b22fe7ea8 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000401_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000405_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000405_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..f83ef74fb Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000405_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000420_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000420_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..dd6bf6a8c Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000420_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000425_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000425_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..0636a2c02 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000425_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000439_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000439_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..d4e638bc1 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000439_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000447_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000447_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..59fd33d8d Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000447_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000448_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000448_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..3749ce551 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000448_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000450_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000450_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..4a186e2dd Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000450_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000453_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000453_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..5d8b6de76 Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000453_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000459_eps_1_255.vnnlib.gz b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000459_eps_1_255.vnnlib.gz new file mode 100644 index 000000000..12208707e Binary files /dev/null and b/code/nnv/examples/NNV3.0/ProbVer/yolo_2023/vnnlib/TinyYOLO_prop_000459_eps_1_255.vnnlib.gz differ diff --git a/code/nnv/examples/NNV3.0/README.md b/code/nnv/examples/NNV3.0/README.md new file mode 100644 index 000000000..af3963d6f --- /dev/null +++ b/code/nnv/examples/NNV3.0/README.md @@ -0,0 +1,154 @@ +# Instructions + +When building the docker image, we are copying the local NNV files into the container. The result of this is that +the files are not in an editable state. So, if we make a change locally to the files, the changes will not show +up within the container. We will have to rebuild the container if we want the files to be updated. + +Additionally, we need to run the `docker build` command from NNV's root so that all of the code gets copied into the +docker container correctly. We can do this with +``` +cd /home/sasakis/v/tools/nnv +docker build -t nnv3.0 -f code/nnv/examples/NNV3.0/Dockerfile . +``` +Then access the container with +``` +docker run --gpus all -it nnv3.0 +``` +We need the `--gpus all` flag for the probabilistic verification which uses GPU. + +# FairNNV +Make sure to run the scripts after having already run +``` +cd /path/to/NNV3.0/FairNNV +``` +i.e., make sure you are in the FairNNV directory before running the scripts with MATLAB headless. + +After this, we can run the experiments with +``` +matlab -nodisplay -r "run('run_fm26_fairnnv.m'); exit()" +``` +Once the experiments run, we can copy them from the docker container onto the local filesystem by opening +a new terminal, finding the container id with `docker ps -a` and then running +``` +docker cp :/path/to/fm26_fairnnv_results /target/destination/for/fm26_fairnnv_results +``` +The first path is the path to the results directory within the container and the second will be the path to the +target destination of the directory on the local file system. + +# Probabilistic Verification +After building the container and running it like in the earlier instructions, we can run the following to run the probabilistic +verification: +``` +cd /path/to/NNV3.0/ProbVer +matlab -nodisplay -r "run('run_probver.m'); exit()" +``` + +# ModelStar + +All of the code for running the examples for ModelStar are contained elsewhere within the tool (see `nnv/code/nnv/examples/Tutorial/NN/MNIST/weightPerturb`). + +In this repository, run the `run_expt_for_compute.m` script to run the experiments and then produce the plot shown in the paper by running the `EXPT.m` script. + +# VideoStar + +The VideoStar experiments run verification on video classification neural networks using the ZoomIn dataset. +The full experiments are in `nnv/code/nnv/examples/Submission/FORMALISE2025`, and this directory contains +scripts for running a subset of those experiments (ZoomIn-4f). + +## Prerequisites + +The VideoStar experiments require the ONNX models and data files to be placed in the FORMALISE2025 directory structure. + +### Data Setup + +If you have data files in `VideoStar/data/`, copy them to the FORMALISE2025 data directory: +```bash +cp -r code/nnv/examples/NNV3.0/VideoStar/data/* code/nnv/examples/Submission/FORMALISE2025/data/ +``` + +The expected directory structure in `FORMALISE2025/data/` is: +``` +data/ +└── ZoomIn/ + ├── mnistvideo_zoom_in_4f_test_data_seq.npy + └── mnistvideo_zoom_in_test_labels_seq.npy +``` + +The ONNX models (e.g., `zoomin_4f.onnx`) should be in `FORMALISE2025/models/`. + +## Running VideoStar ZoomIn-4f (Subset) + +After building the container and running it, navigate to the VideoStar directory and run: + +```bash +cd /home/matlab/nnv/code/nnv/examples/NNV3.0/VideoStar +matlab -nodisplay -r "run('run_zoomin_4f.m'); exit()" +``` + +Alternatively, you can use the shell script: +```bash +cd /home/matlab/nnv/code/nnv/examples/NNV3.0/VideoStar +./run_videostar_zoomin4f.sh +``` + +Or use the Python interface: +```bash +cd /home/matlab/nnv/code/nnv/examples/NNV3.0/VideoStar +python run_zoomin_4f.py --algorithm relax --num-samples 10 +``` + +## Configuration + +The `run_zoomin_4f.m` script can be configured by editing the CONFIGURATION section: +- `config.sampleIndices`: Which samples to verify (default: 1:10) +- `config.verAlgorithm`: Either 'relax' or 'approx' (default: 'relax') +- `config.timeout`: Timeout per sample in seconds (default: 1800) + +## Results + +Results are saved to `/tmp/results/VideoStar/ZoomIn/4/` with CSV files for each epsilon value: +- `eps=1_255.csv`: Results with epsilon = 1/255 +- `eps=2_255.csv`: Results with epsilon = 2/255 +- `eps=3_255.csv`: Results with epsilon = 3/255 + +To copy results from the container to your local filesystem: +```bash +docker cp :/tmp/results/VideoStar ./videostar_results +``` + +# GNNV (Graph Neural Network Verification) + +Demonstrates GNN verification for power flow prediction on the IEEE 24-bus system, comparing GCN, GINE, and GINE+Edge architectures. + +## Running GNNV + +```bash +cd /home/matlab/nnv/code/nnv/examples/NNV3.0/GNNV +matlab -nodisplay -r "run('run_gnn_experiments.m'); exit()" +``` + +**Options:** +- `run_gnn_experiments('quiet')` - Minimal output, logs to file +- `run_gnn_experiments('no_figures')` - Skip figure generation +- `run_gnn_experiments('quiet', 'no_figures')` - Both + +**Configuration:** + +The experiments verify voltage magnitude bounds on GNN outputs with: +- **Models**: GCN, GINE, GINE+Edge +- **Perturbation levels (ε)**: 0.001, 0.005, 0.01 +- **Test scenarios**: 10 (evenly sampled from test set) +- **Voltage specification**: [0.95, 1.05] p.u. + +**Expected runtime:** ~5 minutes + +## Results + +- `figures/dashboard.png`, `dashboard.pdf` - Visualization +- `figures/results_table.tex` - LaTeX table +- `results/gnn_results.mat` - Raw data + +To copy results from the container: +```bash +docker cp :/home/matlab/nnv/code/nnv/examples/NNV3.0/GNNV/figures ./gnnv_figures +``` diff --git a/code/nnv/examples/NNV3.0/VideoStar/data/mnistvideo_zoom_in_4f_test_data_seq.npy b/code/nnv/examples/NNV3.0/VideoStar/data/mnistvideo_zoom_in_4f_test_data_seq.npy new file mode 100644 index 000000000..ea7415424 Binary files /dev/null and b/code/nnv/examples/NNV3.0/VideoStar/data/mnistvideo_zoom_in_4f_test_data_seq.npy differ diff --git a/code/nnv/examples/NNV3.0/VideoStar/data/mnistvideo_zoom_in_test_labels_seq.npy b/code/nnv/examples/NNV3.0/VideoStar/data/mnistvideo_zoom_in_test_labels_seq.npy new file mode 100644 index 000000000..765f2ca1b Binary files /dev/null and b/code/nnv/examples/NNV3.0/VideoStar/data/mnistvideo_zoom_in_test_labels_seq.npy differ diff --git a/code/nnv/examples/NNV3.0/VideoStar/run_videostar_zoomin4f.sh b/code/nnv/examples/NNV3.0/VideoStar/run_videostar_zoomin4f.sh new file mode 100755 index 000000000..4598eabca --- /dev/null +++ b/code/nnv/examples/NNV3.0/VideoStar/run_videostar_zoomin4f.sh @@ -0,0 +1,46 @@ +#!/bin/bash +# VideoStar ZoomIn-4f Verification Script +# +# This script runs a subset of the ZoomIn-4f verification experiments +# for VideoStar. It is designed to be run inside the NNV Docker container. +# +# Usage (inside Docker container): +# cd /home/matlab/nnv/code/nnv/examples/NNV3.0/VideoStar +# ./run_videostar_zoomin4f.sh +# +# Or with MATLAB headless: +# cd /home/matlab/nnv/code/nnv/examples/NNV3.0/VideoStar +# matlab -nodisplay -r "run('run_zoomin_4f.m'); exit()" +# +# Or with Python: +# cd /home/matlab/nnv/code/nnv/examples/NNV3.0/VideoStar +# python run_zoomin_4f.py --algorithm relax --num-samples 10 + +echo "==============================================" +echo "VideoStar ZoomIn-4f Verification" +echo "==============================================" +echo "" + +# Check if we're in the right directory +if [ ! -f "run_zoomin_4f.m" ]; then + echo "Error: run_zoomin_4f.m not found." + echo "Please run this script from the VideoStar directory:" + echo " cd /home/matlab/nnv/code/nnv/examples/NNV3.0/VideoStar" + exit 1 +fi + +echo "Running ZoomIn-4f verification with MATLAB..." +echo "" + +# Run the MATLAB script +matlab -nodisplay -r "run('run_zoomin_4f.m'); exit()" + +echo "" +echo "==============================================" +echo "VideoStar ZoomIn-4f Verification Complete" +echo "==============================================" +echo "" +echo "Results saved to: /tmp/results/VideoStar/ZoomIn/4/" +echo "" +echo "To copy results from the container:" +echo " docker cp :/tmp/results/VideoStar ./videostar_results" diff --git a/code/nnv/examples/NNV3.0/VideoStar/run_zoomin_4f.m b/code/nnv/examples/NNV3.0/VideoStar/run_zoomin_4f.m new file mode 100644 index 000000000..7cec50866 --- /dev/null +++ b/code/nnv/examples/NNV3.0/VideoStar/run_zoomin_4f.m @@ -0,0 +1,252 @@ +%% VideoStar ZoomIn-4f - Main Runner Script +% This script runs a subset of the ZoomIn-4f verification experiments. +% +% INSTRUCTIONS: +% 1. Set the paths in the CONFIGURATION section below +% 2. Run this script from the VideoStar directory +% 3. Results will be saved to the specified output folder +% +% OUTPUTS: +% - CSV files with verification results for each epsilon value +% +% REQUIREMENTS: +% - NNV toolbox must be installed +% - ONNX models from FORMALISE2025/models/ +% - Data files from FORMALISE2025/data/ +% - npy-matlab for reading .npy files + +%% ================== CONFIGURATION ================== +% Set these paths before running + +% Path to NNV root folder (contains startup_nnv.m) +% NOTE: these paths are for the docker container +config.nnvDir = '/home/matlab/nnv/code/nnv'; + +% Path to FORMALISE2025 submission directory +config.formalise2025Dir = '/home/matlab/nnv/code/nnv/examples/Submission/FORMALISE2025'; + +% Path to folder containing ONNX models (e.g., zoomin_4f.onnx) +config.modelsDir = '/home/matlab/nnv/code/nnv/examples/Submission/FORMALISE2025/models'; + +% Path to folder containing data files +config.dataDir = '/home/matlab/nnv/code/nnv/examples/Submission/FORMALISE2025/data'; + +% Path to npy-matlab for reading .npy files +config.npyMatlabDir = '/home/matlab/nnv/code/nnv/examples/Submission/FORMALISE2025/npy-matlab/npy-matlab'; + +% Path to output folder for results (will be created if it doesn't exist) +config.outputDir = '/tmp/results/VideoStar/ZoomIn/4'; + +% Verification settings +config.dsType = 'zoom_in'; % Dataset type: 'zoom_in' or 'zoom_out' +config.sampleLen = 4; % Number of frames: 4, 8, or 16 +config.verAlgorithm = 'relax'; % Verification algorithm: 'relax' or 'approx' + +% Number of classes +config.numClasses = 10; + +% Epsilon values for verification (perturbation sizes) +config.epsilon = [1/255; 2/255; 3/255]; + +% Timeout per sample in seconds (default: 1800 = 30 minutes) +config.timeout = 1800; + +% Sample indices to verify (subset for quick testing) +% Using first 10 samples for a subset run +config.sampleIndices = 1:10; + +%% ================== END CONFIGURATION ================== + +%% Initialize NNV +disp("======= VideoStar ZoomIn-4f Verification =========="); +disp(" "); +disp("Initializing NNV toolbox..."); + +% Check if NNV directory exists +if ~exist(config.nnvDir, 'dir') + error("NNV directory not found: %s", config.nnvDir); +end + +% Add NNV to path +addpath(genpath(config.nnvDir)); +disp("NNV paths added successfully."); + +% Add npy-matlab to path for reading .npy files +if ~exist(config.npyMatlabDir, 'dir') + error("npy-matlab directory not found: %s", config.npyMatlabDir); +end +addpath(config.npyMatlabDir); +disp("npy-matlab paths added successfully."); + +% Add FORMALISE2025 src directory to path (for verifyvideo.m) +addpath(fullfile(config.formalise2025Dir, 'src', 'vvn')); +disp("FORMALISE2025 verification functions added to path."); + +disp(" "); + +%% Validate Configuration +disp("Validating configuration..."); + +% Check if models directory exists +if ~exist(config.modelsDir, 'dir') + error("Models directory not found: %s", config.modelsDir); +end + +% Check if data directory exists +if ~exist(config.dataDir, 'dir') + error("Data directory not found: %s", config.dataDir); +end + +% Check if model exists +modelName = sprintf("zoomin_%df.onnx", config.sampleLen); +modelPath = fullfile(config.modelsDir, modelName); +if ~exist(modelPath, 'file') + error("Model not found: %s", modelPath); +end +disp(" Found model: " + modelName); + +% Create output directory if it doesn't exist +if ~exist(config.outputDir, 'dir') + mkdir(config.outputDir); + disp(" Created output directory: " + config.outputDir); +else + disp(" Output directory: " + config.outputDir); +end + +disp(" "); +disp("Configuration validated successfully."); +disp(" "); + +%% Change to FORMALISE2025 directory (required for data loading paths) +currentDir = pwd; +cd(config.formalise2025Dir); +disp("Changed to FORMALISE2025 directory for data loading."); +disp(" "); + +%% Run Verification +disp("======= Running ZoomIn-4f Verification =========="); +disp(" "); +disp(sprintf("Dataset: %s", config.dsType)); +disp(sprintf("Sample Length: %d frames", config.sampleLen)); +disp(sprintf("Verification Algorithm: %s", config.verAlgorithm)); +disp(sprintf("Number of samples: %d", length(config.sampleIndices))); +disp(sprintf("Epsilon values: [1/255, 2/255, 3/255]")); +disp(sprintf("Timeout: %d seconds", config.timeout)); +disp(" "); + +% Initialize results storage +numSamples = length(config.sampleIndices); +numEpsilons = length(config.epsilon); +results = cell(numSamples, numEpsilons); +times = cell(numSamples, numEpsilons); +methods = cell(numSamples, numEpsilons); + +% Run verification for each sample and epsilon +for sampleIdx = 1:numSamples + sampleNum = config.sampleIndices(sampleIdx); + disp(sprintf("Processing sample %d (%d/%d)...", sampleNum, sampleIdx, numSamples)); + + for epsIdx = 1:numEpsilons + eps = config.epsilon(epsIdx); + disp(sprintf(" Epsilon = %d/255...", epsIdx)); + + try + % Call the verification function from FORMALISE2025 + [res, t, met] = verifyvideo(config.dsType, config.sampleLen, ... + config.verAlgorithm, sampleNum, epsIdx); + + results{sampleIdx, epsIdx} = res; + times{sampleIdx, epsIdx} = t; + methods{sampleIdx, epsIdx} = met; + + disp(sprintf(" Result: %d, Time: %.2f s", res, t)); + + catch ME + disp(sprintf(" Error: %s", ME.message)); + results{sampleIdx, epsIdx} = -1; + times{sampleIdx, epsIdx} = -1; + methods{sampleIdx, epsIdx} = ME.message; + end + end +end + +%% Save Results +disp(" "); +disp("======= Saving Results =========="); + +% Save results for each epsilon value +for epsIdx = 1:numEpsilons + outputFile = fullfile(config.outputDir, sprintf('eps=%d_255.csv', epsIdx)); + + % Open file and write header + fid = fopen(outputFile, 'w'); + fprintf(fid, 'Sample Number,Result,Time,Method\n'); + + % Write results + for sampleIdx = 1:numSamples + sampleNum = config.sampleIndices(sampleIdx); + res = results{sampleIdx, epsIdx}; + t = times{sampleIdx, epsIdx}; + met = methods{sampleIdx, epsIdx}; + + if isnumeric(t) + fprintf(fid, '%d,%d,%.6f,%s\n', sampleNum, res, t, met); + else + fprintf(fid, '%d,%d,%s,%s\n', sampleNum, res, t, met); + end + end + + fclose(fid); + disp(sprintf(" Saved: %s", outputFile)); +end + +%% Display Summary +disp(" "); +disp("======= Verification Summary =========="); +disp(" "); + +for epsIdx = 1:numEpsilons + verified = 0; + unknown = 0; + violated = 0; + timeout = 0; + totalTime = 0; + validTimes = 0; + + for sampleIdx = 1:numSamples + res = results{sampleIdx, epsIdx}; + t = times{sampleIdx, epsIdx}; + + if res == 1 + verified = verified + 1; + elseif res == 0 + violated = violated + 1; + elseif res == 2 + unknown = unknown + 1; + elseif res == 3 + timeout = timeout + 1; + end + + if isnumeric(t) && t > 0 + totalTime = totalTime + t; + validTimes = validTimes + 1; + end + end + + avgTime = totalTime / max(validTimes, 1); + + disp(sprintf("Epsilon = %d/255:", epsIdx)); + disp(sprintf(" Verified (robust): %d", verified)); + disp(sprintf(" Violated: %d", violated)); + disp(sprintf(" Unknown: %d", unknown)); + disp(sprintf(" Timeout: %d", timeout)); + disp(sprintf(" Average time: %.2f s", avgTime)); + disp(" "); +end + +%% Cleanup +cd(currentDir); + +disp("======= VideoStar ZoomIn-4f Complete =========="); +disp(" "); +disp(sprintf("Results saved to: %s", config.outputDir)); diff --git a/code/nnv/examples/NNV3.0/VideoStar/run_zoomin_4f.py b/code/nnv/examples/NNV3.0/VideoStar/run_zoomin_4f.py new file mode 100644 index 000000000..e5c3b1f73 --- /dev/null +++ b/code/nnv/examples/NNV3.0/VideoStar/run_zoomin_4f.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +""" +VideoStar ZoomIn-4f Verification Script + +This script runs a subset of the ZoomIn-4f verification experiments using +the MATLAB engine for Python. It is designed to run inside the NNV Docker +container. + +Usage: + python run_zoomin_4f.py [--algorithm {relax,approx,both}] [--num-samples N] + +Requirements: + - MATLAB with Python engine installed + - NNV toolbox + - Environment variables: NNV_PATH, NPY_MATLAB_PATH +""" + +import argparse +import csv +import io +import os +import sys +from typing import Tuple + +# Add FORMALISE2025 src to path for importing modules +FORMALISE2025_DIR = '/home/matlab/nnv/code/nnv/examples/Submission/FORMALISE2025' +sys.path.insert(0, os.path.join(FORMALISE2025_DIR, 'src')) + +import matlab.engine + + +# Configuration +NNV_PATH = '/home/matlab/nnv/code/nnv' +NPY_MATLAB_PATH = '/home/matlab/nnv/code/nnv/examples/Submission/FORMALISE2025/npy-matlab/npy-matlab' +RESULTS_DIR = '/tmp/results/VideoStar' + + +def parse_args(): + parser = argparse.ArgumentParser( + description='Run ZoomIn-4f verification experiments for VideoStar' + ) + parser.add_argument( + '--algorithm', + type=str, + choices=['relax', 'approx', 'both'], + default='relax', + help='Verification algorithm to use (default: relax)' + ) + parser.add_argument( + '--num-samples', + type=int, + default=10, + help='Number of samples to verify (default: 10)' + ) + parser.add_argument( + '--timeout', + type=int, + default=1800, + help='Timeout per sample in seconds (default: 1800)' + ) + return parser.parse_args() + + +def prepare_engine(nnv_path: str, npy_matlab_path: str): + """Start MATLAB engine and add required paths.""" + if not nnv_path or not npy_matlab_path: + raise Exception( + 'One of nnv_path or npy_matlab_path is not defined. ' + 'Please ensure these have been set before running.' + ) + + # Start MATLAB engine + eng = matlab.engine.start_matlab() + print('Started MATLAB engine!') + + # Add paths + eng.addpath(FORMALISE2025_DIR) + eng.addpath(os.path.join(FORMALISE2025_DIR, 'src', 'vvn')) + eng.addpath(eng.genpath(nnv_path)) + eng.addpath(eng.genpath(npy_matlab_path)) + + # Change to FORMALISE2025 directory for data loading + eng.cd(FORMALISE2025_DIR) + + return eng + + +def verify( + ds_type: str, + sample_len: int, + ver_algorithm: str, + eng, + index: int, + eps_index: int, + timeout: int +) -> Tuple[int, float, str]: + """Run verification on a single sample.""" + if not eng: + raise Exception( + 'MATLAB Engine was not correctly started. ' + 'Please make sure to run `prepare_engine`.' + ) + + # Call MATLAB script to run verification + future = eng.verifyvideo( + ds_type, + sample_len, + ver_algorithm, + index, + eps_index, + nargout=3, + background=True, + stdout=io.StringIO() + ) + + try: + [res, t, met] = future.result(timeout=float(timeout)) + except matlab.engine.TimeoutError: + print(' Timeout') + res = 3 + t = 'timeout' + met = 'timeout' + + future.cancel() + + return res, t, met + + +def write_results(output_file: str, sample_num: int, res: int, t, met: str): + """Append results to CSV file.""" + # Create directory if it doesn't exist + os.makedirs(os.path.dirname(output_file), exist_ok=True) + + # Write header if file doesn't exist + if not os.path.exists(output_file): + with open(output_file, 'w', newline='') as f: + writer = csv.writer(f) + writer.writerow(['Sample Number', 'Result', 'Time', 'Method']) + + # Append results + with open(output_file, 'a', newline='') as f: + writer = csv.writer(f) + writer.writerow([sample_num, res, t, met]) + + +def run_zoomin_4f(algorithm: str, num_samples: int, timeout: int): + """Run ZoomIn-4f verification experiments.""" + # Configuration + ds_type = 'zoom_in' + sample_len = 4 + epsilon_indices = [1, 2, 3] # 1/255, 2/255, 3/255 + + # Sample indices to verify (1-indexed for MATLAB) + sample_indices = list(range(1, num_samples + 1)) + + # Output directory + output_dir = os.path.join(RESULTS_DIR, 'ZoomIn', str(sample_len)) + os.makedirs(output_dir, exist_ok=True) + + print("=" * 50) + print(f"Running ZoomIn-4f verification") + print("=" * 50) + print(f" Algorithm: {algorithm}") + print(f" Dataset: {ds_type}") + print(f" Sample length: {sample_len} frames") + print(f" Number of samples: {num_samples}") + print(f" Timeout: {timeout} seconds") + print(f" Output directory: {output_dir}") + print() + + # Start MATLAB engine + eng = prepare_engine(NNV_PATH, NPY_MATLAB_PATH) + + # Run verification + for sample_idx, index in enumerate(sample_indices): + print(f'Sample {index} ({sample_idx + 1}/{num_samples})') + + for eps_index in epsilon_indices: + output_file = os.path.join(output_dir, f'eps={eps_index}_255.csv') + + # Verify the sample + res, t, met = verify( + ds_type, sample_len, algorithm, eng, index, eps_index, timeout + ) + + # Write results + write_results(output_file, index, res, t, met) + + # Print result + if isinstance(t, (int, float)): + print(f' eps={eps_index}/255: Result={res}, Time={t:.2f}s') + else: + print(f' eps={eps_index}/255: Result={res}, Time={t}') + + # Close MATLAB engine + eng.quit() + + print() + print("=" * 50) + print("Verification complete.") + print(f"Results saved to: {output_dir}") + print("=" * 50) + + +def main(): + args = parse_args() + + # Determine which algorithms to run + algorithms = [] + if args.algorithm in ['relax', 'both']: + algorithms.append('relax') + if args.algorithm in ['approx', 'both']: + algorithms.append('approx') + + for algorithm in algorithms: + run_zoomin_4f(algorithm, args.num_samples, args.timeout) + + +if __name__ == "__main__": + main()