diff --git a/code/nnv/examples/Submission/VNN_COMP2024/run_vnncomp2024_instance.m b/code/nnv/examples/Submission/VNN_COMP2024/run_vnncomp2024_instance.m index 96167bb92..62a20ccb2 100644 --- a/code/nnv/examples/Submission/VNN_COMP2024/run_vnncomp2024_instance.m +++ b/code/nnv/examples/Submission/VNN_COMP2024/run_vnncomp2024_instance.m @@ -58,7 +58,7 @@ warning("Working on adding support to other vnnlib properties"); end -cEX_time = toc(t) +cEX_time = toc(t); %% 3) UNSAT? @@ -384,26 +384,37 @@ else error("We don't have those"); end + reachOptions.reachMethod = 'relax-star-area'; + reachOptions.relaxFactor = 0.8; + reachOptionsList{1} = reachOptions; reachOptions = struct; reachOptions.reachMethod = 'approx-star'; % default parameters - reachOptionsList{1} = reachOptions; + reachOptionsList{2} = reachOptions; elseif contains(category, "vggnet16") % vgg16: onnx to matlab net = importNetworkFromONNX(onnx); % flattenlayer nnvnet = ""; needReshape = 1; - reachOptions = struct; - reachOptions.reachMethod = 'approx-star'; % default parameters + reachOptions.reachMethod = 'relax-star-area'; + reachOptions.relaxFactor = 0.9; reachOptionsList{1} = reachOptions; + reachOptions = struct; + reachOptions.reachMethod = 'relax-star-area'; + reachOptions.relaxFactor = 0.5; + reachOptionsList{2} = reachOptions; elseif contains(category, "tllverify") % tllverify: onnx to nnv net = importNetworkFromONNX(onnx,"InputDataFormats", "BC", 'OutputDataFormats',"BC"); nnvnet = matlab2nnv(net); reachOptions = struct; - reachOptions.reachMethod = 'approx-star'; % default parameters + reachOptions.reachMethod = 'relax-star-area'; + reachOptions.relaxFactor = 0.9; reachOptionsList{1} = reachOptions; + reachOptions = struct; + reachOptions.reachMethod = 'approx-star'; % default parameters + reachOptionsList{2} = reachOptions; elseif contains(category, "vit") % vit: onnx to matlab @@ -459,10 +470,10 @@ needReshape = 1; reachOptions = struct; reachOptions.reachMethod = 'relax-star-area'; - reachOptions.relaxFactor = 0.5; + reachOptions.relaxFactor = 1; reachOptionsList{1} = reachOptions; - reachOptions = struct; - reachOptions.reachMethod = 'approx-star'; % default parameters + reachOptions.reachMethod = 'relax-star-area'; + reachOptions.relaxFactor = 0.5; reachOptionsList{2} = reachOptions; elseif contains(category, "tinyimagenet") @@ -502,13 +513,23 @@ % cora benchmark: onnx 2 nnv net = importNetworkFromONNX(onnx, "InputDataFormats","BC", "OutputDataFormats","BC"); nnvnet = matlab2nnv(net); - reachOptions = struct; - reachOptions.reachMethod = 'relax-star-area'; - reachOptions.relaxFactor = 0.5; - reachOptionsList{1} = reachOptions; - reachOptions = struct; - reachOptions.reachMethod = 'approx-star'; % default parameters - reachOptionsList{2} = reachOptions; + if contains(onnx, '-set') + reachOptions = struct; + reachOptions.reachMethod = 'relax-star-area'; + reachOptions.relaxFactor = 0.5; + reachOptionsList{1} = reachOptions; + reachOptions = struct; + reachOptions.reachMethod = 'approx-star'; % default parameters + reachOptionsList{2} = reachOptions; + else + reachOptions = struct; + reachOptions.reachMethod = 'relax-star-area'; + reachOptions.relaxFactor = 0.9; + reachOptionsList{1} = reachOptions; + reachOptions.reachMethod = 'relax-star-area'; + reachOptions.relaxFactor = 0.7; + reachOptionsList{1} = reachOptions; + end elseif contains(category, "lsnc") % lyapunov benchmark: onnx to nnv (barely, some IR and opset version differences)