|
13 | 13 |
|
14 | 14 | % Load networks |
15 | 15 |
|
16 | | -[net, nnvnet, needReshape, reachOptionsList, inputSize, inputFormat] = load_vnncomp_network(category, onnx, vnnlib); |
| 16 | +[net, nnvnet, needReshape, reachOptionsList, inputSize, inputFormat, nRand] = load_vnncomp_network(category, onnx, vnnlib); |
17 | 17 |
|
18 | 18 | if isempty(inputSize) |
19 | 19 | inputSize = net.Layers(1, 1).InputSize; |
|
32 | 32 |
|
33 | 33 | %% 2) SAT? |
34 | 34 |
|
35 | | -nRand = 100; % number of random inputs (this can be changed) |
| 35 | +% nRand = 100; % number of random inputs (this can be changed) |
36 | 36 | % We got some penalties last year, why? |
37 | 37 | % Wrong vnnlib parsing? Wrong counterrexample writing? Do we need to reshape it? |
38 | 38 | % Let's test last years properties and make sure those errors/bugs are |
|
317 | 317 |
|
318 | 318 | end |
319 | 319 |
|
320 | | -function [net,nnvnet,needReshape,reachOptionsList,inputSize,inputFormat] = load_vnncomp_network(category, onnx, vnnlib) |
| 320 | +function [net,nnvnet,needReshape,reachOptionsList,inputSize,inputFormat,nRand] = load_vnncomp_network(category, onnx, vnnlib) |
321 | 321 | % load participating vnncomp 2025 benchmark NNs |
322 | 322 | % Not yet supported: |
323 | 323 | % - cctsdb (some errrors when forward propagating) |
324 | 324 | % - lsnc_relu |
325 | 325 | % - ml4acopf |
326 | | -% - traffic_signs_recognition |
| 326 | +% - traffic_signs_recognition (last year all instances were sat, maybe we are not wrong?) |
327 | 327 |
|
328 | 328 |
|
329 | 329 | needReshape = 0; % default is to use MATLAB reshape, otherwise use the python reshape |
|
332 | 332 | numCores = feature('numcores'); % in case we select exact method |
333 | 333 | inputSize = []; |
334 | 334 | inputFormat = "default"; % no need to change for most of them, but needed for some ("UU") |
| 335 | + nRand = 100; % default from previous competitions |
335 | 336 |
|
336 | 337 | if contains(category, "acasxu") |
337 | 338 | % acasxu: onnx to nnv |
|
341 | 342 | reachOptions.reachMethod = 'exact-star'; |
342 | 343 | reachOptions.numCores = numCores; |
343 | 344 | reachOptionsList{1} = reachOptions; |
| 345 | + nRand = 500; |
344 | 346 | else |
345 | 347 | reachOptions = struct; |
346 | 348 | reachOptions.reachMethod = 'approx-star'; % default parameters |
|
349 | 351 | reachOptions.numCores = numCores; |
350 | 352 | reachOptionsList{2} = reachOptions; |
351 | 353 | end |
| 354 | + |
352 | 355 |
|
353 | 356 | elseif contains(category, "cctsdb_yolo") |
354 | 357 | % net = importNetworkFromONNX(onnx); |
|
438 | 441 | reachOptions.relaxFactor = 0.7; |
439 | 442 | reachOptionsList{1} = reachOptions; |
440 | 443 | end |
| 444 | + nRand = 500; |
441 | 445 |
|
442 | 446 | elseif contains(category, "dist_shift") |
443 | 447 | % dist_shift: onnx to matlab, , matlab to nnv? |
|
609 | 613 | reachOptions.reachMethod = 'exact-star'; % default parameters |
610 | 614 | reachOptions.numCores = numCores; |
611 | 615 | reachOptionsList{2} = reachOptions; |
| 616 | + nRand = 500; |
612 | 617 |
|
613 | 618 | elseif contains(category, "sat_relu") |
614 | 619 | net = importNetworkFromONNX(onnx, "InputDataFormats", "BC"); |
|
634 | 639 | net = importNetworkFromONNX(onnx, "InputDataFormats","BCSS", "OutputDataFormats","BC"); |
635 | 640 | nnvnet = matlab2nnv(net); |
636 | 641 | reachOptions = struct; |
637 | | - reachOptions.reachMethod = 'relax-star-area'; % default parameters |
638 | | - reachOptions.relaxFactor = 1; |
| 642 | + % reachOptions.reachMethod = 'relax-star-area'; % default parameters |
| 643 | + % reachOptions.relaxFactor = 1; |
| 644 | + % reachOptionsList{1} = reachOptions; |
| 645 | + % reachOptions = struct; |
| 646 | + % reachOptions.reachMethod = 'relax-star-area'; % default parameters |
| 647 | + % reachOptions.relaxFactor = 0.8; |
| 648 | + % reachOptionsList{2} = reachOptions; |
| 649 | + reachOptions.reachMethod = "cp-star"; |
639 | 650 | reachOptionsList{1} = reachOptions; |
640 | | - reachOptions = struct; |
641 | | - reachOptions.reachMethod = 'relax-star-area'; % default parameters |
642 | | - reachOptions.relaxFactor = 0.8; |
643 | | - reachOptionsList{2} = reachOptions; |
644 | 651 | needReshape = 1; |
| 652 | + nRand = 500; |
645 | 653 |
|
646 | 654 | elseif contains(category, "tllverify") |
647 | 655 | % tllverify: onnx to nnv |
|
0 commit comments