In the quickstart, we used the default parameters for find_adversarial_example
. Using the same example from the quickstart, we explore how to get more out of the function.
using MIPVerify
using Gurobi
using JuMP
using Images
mnist = MIPVerify.read_datasets("MNIST")
n1 = MIPVerify.get_example_network_params("MNIST.n1")
sample_image = MIPVerify.get_image(mnist.test.images, 1);
function print_summary(d::Dict)
# Helper function to print out output
obj_val = getobjectivevalue(d[:Model])
solve_time = getsolvetime(d[:Model])
println("Objective Value: $(@sprintf("%.6f", obj_val)), Solve Time: $(@sprintf("%.2f", solve_time))")
end
function view_diff(diff::Array{<:Real, 2})
n = 1001
colormap("RdBu", n)[ceil.(Int, (diff+1)/2*n)]
end;
find_adversarial_example
¶find_adversarial_example
takes four positional arguments
find_adversarial_example(nn, input, target_selection, main_solver)
It also takes named arguments, each with the default value specified.
norm_order = 1
tolerance = 0
rebuild = false
invert_target_selection = false
pp = MIPVerify.UnrestrictedPerturbationFamily()
tightening_algorithm = mip
tightening_solver: same as main solver, but with output suppressed and a time limit of 20s per solve.
We explore what each of these options allow us to do.
target_selection
and invert_target_selection
control what the category we want the adversarial example to be classified in.
Specification: target_selection
accepts either a single integer or a list of integers.
For example, if I wanted the original image (which is the digit 7) to be classified as the digit 8 or 9, I could run two separate solves with target_selection=9
and target_selection=10
(Julia is 1-indexed), finding closest adversarial examples at distance 13.763
and 4.642
...
d = MIPVerify.find_adversarial_example(n1, sample_image, 9, GurobiSolver(OutputFlag=0))
# OutputFlag=0 prevents any output from being printed out
print_summary(d)
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [9] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Objective Value: 13.762581, Solve Time: 177.25
d = MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0));
print_summary(d)
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Objective Value: 4.641859, Solve Time: 55.27
Or I can can pass the targets as target_selection = [9, 10]
, where the same optimal value of 4.642
is found.
Solve times for multiple target labels are typically on par with or faster than the aggregate solve times when solving with each target label in sequence.
d = MIPVerify.find_adversarial_example(n1, sample_image, [9, 10], GurobiSolver(OutputFlag=0));
print_summary(d)
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [9, 10] [notice | MIPVerify]: Loading model from cache.
Calculating upper bounds: 50%|████████████ | ETA: 0:00:00
Academic license - for non-commercial use only
Calculating upper bounds: 100%|███████████████████████| Time: 0:00:19
Academic license - for non-commercial use only Objective Value: 4.641859, Solve Time: 77.31
A common use case is to have the adversarial example being in any category but the original:
d = MIPVerify.find_adversarial_example(n1, sample_image, [1, 2, 3, 4, 5, 6, 7, 9, 10], GurobiSolver(OutputFlag=0))
print_summary(d)
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [1, 2, 3, 4, 5, 6, 7, 9, 10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only
Calculating upper bounds: 100%|███████████████████████| Time: 0:02:37 Calculating lower bounds: 100%|███████████████████████| Time: 0:01:47
Academic license - for non-commercial use only Objective Value: 4.641859, Solve Time: 325.92
Rather than typing the full list of other categories, we can set target_selection = 8
, and invert_target_selection = true
.
d = MIPVerify.find_adversarial_example(n1, sample_image, 8, GurobiSolver(OutputFlag=0),
invert_target_selection=true)
print_summary(d)
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [1, 2, 3, 4, 5, 6, 7, 9, 10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only
Calculating upper bounds: 100%|███████████████████████| Time: 0:02:36 Calculating lower bounds: 100%|███████████████████████| Time: 0:01:47
Academic license - for non-commercial use only Objective Value: 4.641859, Solve Time: 278.47
The default option for tolerance
is 0. This means that the activations in the softmax layer will take its maximum value for the target label (or at least one of them if more than one is specified), but that this maximum may not be unique.
In the example below, notice how the activations y[8]
and y[10]
(corresponding to labels 7 and 9) are equal, at 4.56707.
d = MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0))
print_summary(d)
perturbed_sample_image = getvalue(d[:PerturbedInput])
y = perturbed_sample_image |> n1
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Objective Value: 4.641859, Solve Time: 52.90
10-element Array{Float64,1}: 1.05198 0.785344 0.313807 0.427011 0.369729 0.256145 0.66623 4.56707 -0.147984 4.56707
If we want to ensure that the maximum is unique, we can add a small tolerance. This is the minimum difference between the activation of the target label (or the maximum activation of any of the target labels) and any non-target label. In the example below, with a tolerance of 0.001, notice how y[8] = 4.5683 = 0.0010 + 4.5673 = tolerance + y[10]
.
This increases the objective value slightly (since the closest adversarial example with the required tolerance must be slightly further away.)
d = MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0),
tolerance = 0.001)
print_summary(d)
perturbed_sample_image = getvalue(d[:PerturbedInput])
y = perturbed_sample_image |> n1
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Objective Value: 4.643283, Solve Time: 63.39
10-element Array{Float64,1}: 1.05292 0.785758 0.313776 0.427317 0.370021 0.256382 0.666551 4.5673 -0.14813 4.5683
d = @time MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0));
perturbed_sample_image = getvalue(d[:PerturbedInput])
colorview(Gray, perturbed_sample_image[1, :, :, 1])
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only 53.041781 seconds (331.52 k allocations: 17.399 MiB, 0.03% gc time)
We can bound the $L_\infty$-norm of the perturbation.
As long as the size of the $L_\infty$-norm bound we choose is larger than the actual ($L_\infty$-)minimal perturbation, we will find the same result, and often more quickly.
d = @time MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0),
norm_order=Inf);
perturbed_sample_image = getvalue(d[:PerturbedInput])
colorview(Gray, perturbed_sample_image[1, :, :, 1])
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only 55.975023 seconds (370.78 k allocations: 19.352 MiB, 0.02% gc time)
d = @time MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0),
pp = MIPVerify.LInfNormBoundedPerturbationFamily(0.05), norm_order=Inf);
perturbed_sample_image = getvalue(d[:PerturbedInput])
colorview(Gray, perturbed_sample_image[1, :, :, 1])
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only 3.161656 seconds (304.00 k allocations: 17.236 MiB)
If the $L_\infty$-norm bound you choose is smaller than the actual minimal perturbation, the problem is Infeasible, with a status code of either :Infeasible
or :InfeasibleOrUnbounded
. (Make sure you cover both cases!)
d = @time MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0),
pp = MIPVerify.LInfNormBoundedPerturbationFamily(0.03), norm_order=Inf);
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only 0.401018 seconds (287.74 k allocations: 16.295 MiB, 3.33% gc time)
WARNING: Gurobi reported infeasible or unbounded. Set InfUnbdInfo=1 for more specific status. WARNING: Not solved to optimality, status: InfeasibleOrUnbounded
d[:SolveStatus]
:InfeasibleOrUnbounded
We can restrict the perturbations to a blur with a 5x5 kernel instead. (We are still minimizing over the norm of the perturbation.)
d = @time MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0),
pp = MIPVerify.BlurringPerturbationFamily((5, 5)));
perturbed_sample_image = getvalue(d[:PerturbedInput])
colorview(Gray, perturbed_sample_image[1, :, :, 1])
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only 1.801206 seconds (479.47 k allocations: 27.147 MiB, 1.31% gc time)
diff = getvalue(d[:Perturbation])
view_diff(diff[1, :, :, 1])
d = MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0));
print_summary(d)
perturbed_sample_image = getvalue(d[:PerturbedInput])
colorview(Gray, perturbed_sample_image[1, :, :, 1])
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Objective Value: 4.641859, Solve Time: 53.11
We also show the difference between the perturbed image and the original image. Red is areas of decreased brightness and blue is areas of increased brightness.
diff = getvalue(d[:Perturbation])
view_diff(diff[1, :, :, 1])
We can also minimize over the $l_\infty$ norm. This generally results in large patches of the image being changed.
In this case, the minimum $l_\infty$ norm perturbation required for the image to be classified as a 9
is 0.046085.
d = MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0),
norm_order=Inf);
print_summary(d)
perturbed_sample_image = getvalue(d[:PerturbedInput])
colorview(Gray, perturbed_sample_image[1, :, :, 1])
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Objective Value: 0.046085, Solve Time: 56.44
diff = getvalue(d[:Perturbation])
view_diff(diff[1, :, :, 1])
With solvers that can handle MIQPs (like Gurobi), we can minimize over the $l_2$ norm. This generally takes a bit more time.
In this case, the minimum $l_2$ norm perturbation required for the image to be classified as a 9
is 0.705367 = sqrt(0.497542).
d = MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0),
norm_order=2);
print_summary(d)
perturbed_sample_image = getvalue(d[:PerturbedInput])
colorview(Gray, perturbed_sample_image[1, :, :, 1])
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Objective Value: 0.497542, Solve Time: 197.97
diff = getvalue(d[:Perturbation])
view_diff(diff[1, :, :, 1])
Finding adversarial examples consists of two steps:
The first time we verify a neural net, we must do step 1, which can take a long time.
d = @time MIPVerify.find_adversarial_example(n1, sample_image, 1, GurobiSolver(OutputFlag=0), rebuild=true);
print_summary(d)
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [1] [notice | MIPVerify]: Rebuilding model from scratch. This may take some time as we determine upper and lower bounds for the input to each non-linear unit. Academic license - for non-commercial use only
Calculating upper bounds: 100%|███████████████████████| Time: 0:00:00 Calculating lower bounds: 100%|███████████████████████| Time: 0:00:00 Imposing relu constraint: 100%|███████████████████████| Time: 0:00:00 Calculating upper bounds: 100%|███████████████████████| Time: 0:01:45 Calculating lower bounds: 100%|███████████████████████| Time: 0:02:24
[notice | MIPVerify]: The model built will be cached and re-used for future solves, unless you explicitly set rebuild=true.
Academic license - for non-commercial use only
487.657528 seconds (1.95 M allocations: 148.187 MiB, 0.02% gc time)
Objective Value: 13.821871, Solve Time: 226.85
When re-running the solve (with the rebuild
parameter defaulting to false
), we load the model from cache and skip ahead straight to step 2; finding the adversarial example takes much less time.
d = @time MIPVerify.find_adversarial_example(n1, sample_image, 1, GurobiSolver(OutputFlag=0));
print_summary(d)
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [1] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only 211.359899 seconds (331.46 k allocations: 17.398 MiB, 0.01% gc time) Objective Value: 13.821871, Solve Time: 211.27
By setting rebuild=true
, you force the MIP model to be rebuilt even if one exists; this is useful if you want to use a different tightening_algorithm
(or use different parameters for the tightening solver
).
If you find that your cached models are taking up too much space, you can remove them with remove_cached_models()
.
We use two different solvers for the two steps of finding adversarial examples:
tightening_solver
, used only to determine upper and lower bounds on intermediate values when expressing the input-output constraints in the neural net (i.e. if no cached model exists, or if rebuild=true
), andmain_solver
, used to determine the minimal adversarial example for the loaded model.tightening_algorithm
¶By default, we tighten the bounds on each intermediate value by solving an MIP using the tightening_solver
. Compare total solve times for three different tightening algorithms:
@time MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0), rebuild=true,
tightening_algorithm=interval_arithmetic);
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Rebuilding model from scratch. This may take some time as we determine upper and lower bounds for the input to each non-linear unit. [notice | MIPVerify]: The model built will be cached and re-used for future solves, unless you explicitly set rebuild=true. Academic license - for non-commercial use only 172.541745 seconds (465.05 k allocations: 39.319 MiB, 0.02% gc time)
@time MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0), rebuild=true,
tightening_algorithm=lp, tightening_solver = GurobiSolver(Gurobi.Env(), OutputFlag=0));
Academic license - for non-commercial use only [notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Rebuilding model from scratch. This may take some time as we determine upper and lower bounds for the input to each non-linear unit.
Calculating upper bounds: 100%|███████████████████████| Time: 0:00:00 Calculating lower bounds: 75%|█████████████████ | ETA: 0:00:00
[notice | MIPVerify]: The model built will be cached and re-used for future solves, unless you explicitly set rebuild=true.
Calculating lower bounds: 100%|███████████████████████| Time: 0:00:00
Academic license - for non-commercial use only 47.955957 seconds (496.37 k allocations: 72.376 MiB, 0.06% gc time)
MIPVerify.setloglevel!("notice")
@time MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0), rebuild=true,
tightening_algorithm=mip);
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Rebuilding model from scratch. This may take some time as we determine upper and lower bounds for the input to each non-linear unit. Academic license - for non-commercial use only
Calculating upper bounds: 100%|███████████████████████| Time: 0:01:46 Calculating lower bounds: 100%|███████████████████████| Time: 0:02:21
[notice | MIPVerify]: The model built will be cached and re-used for future solves, unless you explicitly set rebuild=true.
Academic license - for non-commercial use only
327.380706 seconds (517.02 k allocations: 72.765 MiB, 0.01% gc time)
We can also modify many of the parameters of the solver to change behavior:
We will be focusing on the parameters available via Gurobi (http://www.gurobi.com/documentation/7.5/refman/parameters.html), but other solvers often have similar options.
d = MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver());
print_summary(d)
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Optimize a model with 3385 rows, 3256 columns and 71132 nonzeros Variable types: 3196 continuous, 60 integer (60 binary) Coefficient statistics: Matrix range [2e-05, 7e+02] Objective range [1e+00, 1e+00] Bounds range [1e+00, 1e+02] RHS range [4e-03, 7e+02] MIP start did not produce a new incumbent solution MIP start violates constraint R1024 by 1.000000000 Presolve removed 2956 rows and 2227 columns Presolve time: 0.18s Presolved: 429 rows, 1029 columns, 61365 nonzeros Variable types: 969 continuous, 60 integer (60 binary) Root relaxation: objective 0.000000e+00, 212 iterations, 0.02 seconds Nodes | Current Node | Objective Bounds | Work Expl Unexpl | Obj Depth IntInf | Incumbent BestBd Gap | It/Node Time 0 0 0.00000 0 3 - 0.00000 - - 0s Another try with MIP start H 0 0 36.9304736 0.00000 100% - 0s H 0 0 32.4680084 0.00000 100% - 0s 0 0 0.00000 0 7 32.46801 0.00000 100% - 0s 0 0 0.00000 0 7 32.46801 0.00000 100% - 0s 0 2 0.00000 0 7 32.46801 0.00000 100% - 0s H 106 61 16.8778596 0.00000 100% 61.7 1s H 150 81 6.3285068 0.00000 100% 64.0 1s * 339 202 50 6.0319541 0.00000 100% 52.1 1s 932 456 0.00000 19 4 6.03195 0.00000 100% 61.5 5s * 2259 525 48 6.0319390 0.00000 100% 57.9 9s 2395 584 3.94423 24 13 6.03194 0.02050 100% 57.8 10s * 2576 643 49 6.0194767 0.02050 100% 55.8 10s * 2869 720 54 5.7675028 0.02050 100% 56.0 11s * 2870 634 54 5.3566208 0.02050 100% 56.0 11s 4121 990 2.27182 33 13 5.35662 0.33754 93.7% 56.4 15s * 4325 895 51 4.6601251 0.33754 92.8% 56.6 15s 6063 1290 4.28290 32 12 4.66013 0.55686 88.1% 55.6 20s 7212 1539 2.82894 35 3 4.66013 0.66630 85.7% 59.4 25s 8732 1771 2.74110 30 15 4.66013 0.97990 79.0% 60.5 30s 10883 1869 cutoff 40 4.66013 1.71949 63.1% 55.8 35s *12282 1982 48 4.6418593 1.94632 58.1% 55.3 39s 12699 2020 3.65375 29 6 4.64186 1.98370 57.3% 55.0 40s 14316 1989 2.45456 34 8 4.64186 2.25731 51.4% 55.3 45s 15785 1845 2.53334 33 9 4.64186 2.53334 45.4% 55.0 50s 16512 1851 2.61060 26 8 4.64186 2.61060 43.8% 55.1 55s 18081 1492 cutoff 20 4.64186 3.21152 30.8% 54.3 60s 19746 1183 3.71451 44 7 4.64186 3.63004 21.8% 53.3 65s 21069 522 cutoff 27 4.64186 3.95299 14.8% 53.6 70s Cutting planes: Gomory: 1 Projected implied bound: 33 MIR: 17 Flow cover: 10 Explored 22057 nodes (1174039 simplex iterations) in 73.00 seconds Thread count was 4 (of 4 available processors) Solution count 10: 4.64186 4.66013 5.35662 ... 32.468 Optimal solution found (tolerance 1.00e-04) Best objective 4.641859316319e+00, best bound 4.641859316319e+00, gap 0.0000% Objective Value: 4.641859, Solve Time: 73.00
MIPVerify.find_adversarial_example(n1, sample_image, 10, GurobiSolver(OutputFlag=0));
print_summary(d)
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [10] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Objective Value: 4.641859, Solve Time: 73.00
Sometimes, finding an adversarial example takes a long time:
MIPVerify.find_adversarial_example(n1, sample_image, 9, GurobiSolver(),
norm_order=Inf);
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [9] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Optimize a model with 4169 rows, 3257 columns and 72700 nonzeros Variable types: 3197 continuous, 60 integer (60 binary) Coefficient statistics: Matrix range [2e-05, 7e+02] Objective range [1e+00, 1e+00] Bounds range [1e+00, 1e+02] RHS range [4e-03, 7e+02] MIP start did not produce a new incumbent solution MIP start violates constraint R1024 by 1.000000000 Presolve removed 2956 rows and 2227 columns Presolve time: 0.25s Presolved: 1213 rows, 1030 columns, 62933 nonzeros Variable types: 970 continuous, 60 integer (60 binary) Root relaxation: objective 0.000000e+00, 879 iterations, 0.08 seconds Nodes | Current Node | Objective Bounds | Work Expl Unexpl | Obj Depth IntInf | Incumbent BestBd Gap | It/Node Time 0 0 0.00000 0 3 - 0.00000 - - 0s Another try with MIP start H 0 0 0.2251479 0.00000 100% - 0s 0 0 0.00000 0 8 0.22515 0.00000 100% - 0s 0 0 0.00000 0 6 0.22515 0.00000 100% - 0s 0 0 0.00000 0 1 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 1s 0 0 0.00000 0 2 0.22515 0.00000 100% - 1s 0 0 0.00000 0 2 0.22515 0.00000 100% - 1s 0 0 0.00000 0 2 0.22515 0.00000 100% - 1s 0 0 0.00000 0 2 0.22515 0.00000 100% - 1s 0 2 0.00000 0 2 0.22515 0.00000 100% - 1s * 91 66 27 0.1185735 0.00000 100% 231 4s 98 70 0.00138 7 13 0.11857 0.00000 100% 242 5s H 136 72 0.1097069 0.00000 100% 255 6s * 155 74 22 0.1059174 0.00000 100% 241 6s * 156 74 22 0.1054467 0.00000 100% 239 6s * 171 83 21 0.1053747 0.00000 100% 225 7s * 205 84 18 0.1042007 0.00000 100% 221 7s * 206 84 18 0.1040731 0.00000 100% 220 7s 269 116 0.00762 8 11 0.10407 0.00000 100% 241 10s 436 148 infeasible 11 0.10407 0.00000 100% 253 15s 548 168 0.02436 8 7 0.10407 0.00000 100% 263 20s 728 183 0.08459 15 7 0.10407 0.00000 100% 264 25s 825 190 0.02433 8 7 0.10407 0.00000 100% 276 30s 1001 237 0.03296 9 11 0.10407 0.00021 100% 272 36s 1131 251 infeasible 9 0.10407 0.01205 88.4% 269 40s 1316 250 0.02321 5 8 0.10407 0.02321 77.7% 262 45s 1499 277 cutoff 10 0.10407 0.02321 77.7% 259 50s 1713 268 0.07814 14 8 0.10407 0.02830 72.8% 257 56s 1868 272 0.09631 14 8 0.10407 0.03441 66.9% 256 61s 2042 269 infeasible 14 0.10407 0.04175 59.9% 255 65s 2210 264 0.07882 14 8 0.10407 0.04673 55.1% 255 70s 2454 288 0.07419 14 6 0.10407 0.05023 51.7% 251 76s 2725 296 0.05622 13 9 0.10407 0.05375 48.4% 246 81s 2859 292 infeasible 14 0.10407 0.05566 46.5% 244 85s 3097 292 infeasible 12 0.10407 0.06116 41.2% 244 91s 3225 328 0.10222 11 4 0.10407 0.06116 41.2% 243 95s 3466 320 infeasible 13 0.10407 0.06118 41.2% 245 103s 3599 312 0.09837 14 8 0.10407 0.06409 38.4% 245 107s 3745 295 infeasible 15 0.10407 0.06503 37.5% 245 111s 3908 280 0.09088 14 9 0.10407 0.06830 34.4% 244 115s 4235 234 infeasible 14 0.10407 0.07122 31.6% 245 124s 4483 254 0.07122 12 3 0.10407 0.07122 31.6% 241 129s 4714 226 0.10284 13 8 0.10407 0.07472 28.2% 239 133s 4911 191 0.07480 9 10 0.10407 0.07480 28.1% 236 137s 5070 151 infeasible 13 0.10407 0.08313 20.1% 236 141s 5368 81 0.09204 8 7 0.10407 0.09204 11.6% 235 147s 5637 10 0.10347 15 6 0.10407 0.09880 5.06% 232 150s Cutting planes: Gomory: 1 Cover: 7 Implied bound: 28 MIR: 9 Flow cover: 13 Inf proof: 11 Explored 5734 nodes (1323607 simplex iterations) in 150.87 seconds Thread count was 4 (of 4 available processors) Solution count 8: 0.104073 0.104201 0.105375 ... 0.225148 Optimal solution found (tolerance 1.00e-04) Best objective 1.040731274903e-01, best bound 1.040731274903e-01, gap 0.0000%
You may want to terminate early when a particular condition is satisfied. Common reasons are:
BestBd
increases above a pre-determined threshold)Incumbent
adversarial image found that is closer to the original image than expected).Incumbent
and BestBd
falls below a pre-determined threshold.Fortunately, Gurobi has a parameter for all of these cases.
Set TimeLimit
:
MIPVerify.find_adversarial_example(n1, sample_image, 9, GurobiSolver(TimeLimit=30),
norm_order=Inf);
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [9] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Optimize a model with 4169 rows, 3257 columns and 72700 nonzeros Variable types: 3197 continuous, 60 integer (60 binary) Coefficient statistics: Matrix range [2e-05, 7e+02] Objective range [1e+00, 1e+00] Bounds range [1e+00, 1e+02] RHS range [4e-03, 7e+02] MIP start did not produce a new incumbent solution MIP start violates constraint R1024 by 1.000000000 Presolve removed 2956 rows and 2227 columns Presolve time: 0.17s Presolved: 1213 rows, 1030 columns, 62933 nonzeros Variable types: 970 continuous, 60 integer (60 binary) Root relaxation: objective 0.000000e+00, 879 iterations, 0.06 seconds Nodes | Current Node | Objective Bounds | Work Expl Unexpl | Obj Depth IntInf | Incumbent BestBd Gap | It/Node Time 0 0 0.00000 0 3 - 0.00000 - - 0s Another try with MIP start H 0 0 0.2251479 0.00000 100% - 0s 0 0 0.00000 0 8 0.22515 0.00000 100% - 0s 0 0 0.00000 0 6 0.22515 0.00000 100% - 0s 0 0 0.00000 0 1 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 1s 0 2 0.00000 0 2 0.22515 0.00000 100% - 1s * 91 66 27 0.1185735 0.00000 100% 231 4s 102 65 infeasible 8 0.11857 0.00000 100% 255 5s H 136 72 0.1097069 0.00000 100% 255 6s * 155 74 22 0.1059174 0.00000 100% 241 6s * 156 74 22 0.1054467 0.00000 100% 239 6s * 171 83 21 0.1053747 0.00000 100% 225 6s * 205 84 18 0.1042007 0.00000 100% 221 7s * 206 84 18 0.1040731 0.00000 100% 220 7s 269 116 0.00762 8 11 0.10407 0.00000 100% 241 10s 436 148 infeasible 11 0.10407 0.00000 100% 253 15s 583 172 0.08712 10 5 0.10407 0.00000 100% 262 20s 728 183 0.08459 15 7 0.10407 0.00000 100% 264 25s 855 194 0.01180 10 7 0.10407 0.00021 100% 274 30s Cutting planes: Gomory: 1 Implied bound: 21 MIR: 9 Flow cover: 11 Inf proof: 2 Explored 856 nodes (236345 simplex iterations) in 30.01 seconds Thread count was 4 (of 4 available processors) Solution count 8: 0.104073 0.104201 0.105375 ... 0.225148 Time limit reached Best objective 1.040731274903e-01, best bound 2.118627167182e-04, gap 99.7964%
WARNING: Not solved to optimality, status: UserLimit
Set BestBdStop
or Cutoff
.
(Cutoff
gives a different error message that is not currently processed correctly by the latest release of Gurobi.jl
).
MIPVerify.find_adversarial_example(n1, sample_image, 9, GurobiSolver(BestBdStop=0.05),
norm_order=Inf);
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [9] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Optimize a model with 4169 rows, 3257 columns and 72700 nonzeros Variable types: 3197 continuous, 60 integer (60 binary) Coefficient statistics: Matrix range [2e-05, 7e+02] Objective range [1e+00, 1e+00] Bounds range [1e+00, 1e+02] RHS range [4e-03, 7e+02] MIP start did not produce a new incumbent solution MIP start violates constraint R1024 by 1.000000000 Presolve removed 2956 rows and 2227 columns Presolve time: 0.17s Presolved: 1213 rows, 1030 columns, 62933 nonzeros Variable types: 970 continuous, 60 integer (60 binary) Root relaxation: objective 0.000000e+00, 879 iterations, 0.05 seconds Nodes | Current Node | Objective Bounds | Work Expl Unexpl | Obj Depth IntInf | Incumbent BestBd Gap | It/Node Time 0 0 0.00000 0 3 - 0.00000 - - 0s Another try with MIP start H 0 0 0.2251479 0.00000 100% - 0s 0 0 0.00000 0 8 0.22515 0.00000 100% - 0s 0 0 0.00000 0 6 0.22515 0.00000 100% - 0s 0 0 0.00000 0 1 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 2 0.00000 0 2 0.22515 0.00000 100% - 1s * 91 66 27 0.1185735 0.00000 100% 231 4s 102 65 infeasible 8 0.11857 0.00000 100% 255 5s H 136 72 0.1097069 0.00000 100% 255 6s * 155 74 22 0.1059174 0.00000 100% 241 6s * 156 74 22 0.1054467 0.00000 100% 239 6s * 171 83 21 0.1053747 0.00000 100% 225 7s * 205 84 18 0.1042007 0.00000 100% 221 7s * 206 84 18 0.1040731 0.00000 100% 220 7s 269 116 0.00762 8 11 0.10407 0.00000 100% 241 10s 436 148 infeasible 11 0.10407 0.00000 100% 253 15s 548 168 0.02436 8 7 0.10407 0.00000 100% 263 20s 728 183 0.08459 15 7 0.10407 0.00000 100% 264 25s 825 190 0.02433 8 7 0.10407 0.00000 100% 276 30s 967 230 cutoff 16 0.10407 0.00021 100% 270 35s 1131 251 infeasible 9 0.10407 0.01205 88.4% 269 40s 1316 250 0.02321 5 8 0.10407 0.02321 77.7% 262 45s 1499 277 cutoff 10 0.10407 0.02321 77.7% 259 50s 1713 268 0.07814 14 8 0.10407 0.02830 72.8% 257 56s 1868 272 0.09631 14 8 0.10407 0.03441 66.9% 256 61s 2042 269 infeasible 14 0.10407 0.04175 59.9% 255 66s 2210 264 0.07882 14 8 0.10407 0.04673 55.1% 255 71s Cutting planes: Gomory: 1 Cover: 3 Implied bound: 25 MIR: 9 Flow cover: 13 Inf proof: 2 Explored 2454 nodes (616806 simplex iterations) in 74.00 seconds Thread count was 4 (of 4 available processors) Solution count 8: 0.104073 0.104201 0.105375 ... 0.225148 Optimization achieved user objective limit Best objective 1.040731274903e-01, best bound 5.023143684607e-02, gap 51.7345%
WARNING: Not solved to optimality, status: UserObjLimit
Set BestObjStop
.
MIPVerify.find_adversarial_example(n1, sample_image, 9, GurobiSolver(BestObjStop=0.2),
norm_order=Inf);
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [9] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Optimize a model with 4169 rows, 3257 columns and 72700 nonzeros Variable types: 3197 continuous, 60 integer (60 binary) Coefficient statistics: Matrix range [2e-05, 7e+02] Objective range [1e+00, 1e+00] Bounds range [1e+00, 1e+02] RHS range [4e-03, 7e+02] MIP start did not produce a new incumbent solution MIP start violates constraint R1024 by 1.000000000 Presolve removed 2956 rows and 2227 columns Presolve time: 0.17s Presolved: 1213 rows, 1030 columns, 62933 nonzeros Variable types: 970 continuous, 60 integer (60 binary) Root relaxation: objective 0.000000e+00, 879 iterations, 0.05 seconds Nodes | Current Node | Objective Bounds | Work Expl Unexpl | Obj Depth IntInf | Incumbent BestBd Gap | It/Node Time 0 0 0.00000 0 3 - 0.00000 - - 0s Another try with MIP start H 0 0 0.2251479 0.00000 100% - 0s 0 0 0.00000 0 8 0.22515 0.00000 100% - 0s 0 0 0.00000 0 6 0.22515 0.00000 100% - 0s 0 0 0.00000 0 1 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 1s 0 0 0.00000 0 2 0.22515 0.00000 100% - 1s 0 0 0.00000 0 2 0.22515 0.00000 100% - 1s 0 2 0.00000 0 2 0.22515 0.00000 100% - 1s * 91 66 27 0.1185735 0.00000 100% 231 4s Cutting planes: Gomory: 1 Implied bound: 3 MIR: 6 Flow cover: 6 Explored 98 nodes (24534 simplex iterations) in 4.10 seconds Thread count was 4 (of 4 available processors) Solution count 2: 0.118574 0.225148 Optimization achieved user objective limit Best objective 1.185735336641e-01, best bound 0.000000000000e+00, gap 100.0000%
WARNING: Not solved to optimality, status: UserObjLimit
Incumbent
and BestBd
is below threshold¶Set MIPGap
.
MIPVerify.find_adversarial_example(n1, sample_image, 9, GurobiSolver(MIPGap=0.4),
norm_order=Inf);
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [9] [notice | MIPVerify]: Loading model from cache. Academic license - for non-commercial use only Optimize a model with 4169 rows, 3257 columns and 72700 nonzeros Variable types: 3197 continuous, 60 integer (60 binary) Coefficient statistics: Matrix range [2e-05, 7e+02] Objective range [1e+00, 1e+00] Bounds range [1e+00, 1e+02] RHS range [4e-03, 7e+02] MIP start did not produce a new incumbent solution MIP start violates constraint R1024 by 1.000000000 Presolve removed 2956 rows and 2227 columns Presolve time: 0.17s Presolved: 1213 rows, 1030 columns, 62933 nonzeros Variable types: 970 continuous, 60 integer (60 binary) Root relaxation: objective 0.000000e+00, 879 iterations, 0.05 seconds Nodes | Current Node | Objective Bounds | Work Expl Unexpl | Obj Depth IntInf | Incumbent BestBd Gap | It/Node Time 0 0 0.00000 0 3 - 0.00000 - - 0s Another try with MIP start H 0 0 0.2251479 0.00000 100% - 0s 0 0 0.00000 0 8 0.22515 0.00000 100% - 0s 0 0 0.00000 0 6 0.22515 0.00000 100% - 0s 0 0 0.00000 0 1 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 0s 0 0 0.00000 0 2 0.22515 0.00000 100% - 1s 0 2 0.00000 0 2 0.22515 0.00000 100% - 1s * 91 66 27 0.1185735 0.00000 100% 231 4s 102 65 infeasible 8 0.11857 0.00000 100% 255 5s H 136 72 0.1097069 0.00000 100% 255 6s * 155 74 22 0.1059174 0.00000 100% 241 6s * 156 74 22 0.1054467 0.00000 100% 239 6s * 171 83 21 0.1053747 0.00000 100% 225 6s * 205 84 18 0.1042007 0.00000 100% 221 7s * 206 84 18 0.1040731 0.00000 100% 220 7s 297 127 infeasible 13 0.10407 0.00000 100% 237 10s 436 148 infeasible 11 0.10407 0.00000 100% 253 15s 583 172 0.08712 10 5 0.10407 0.00000 100% 262 20s 728 183 0.08459 15 7 0.10407 0.00000 100% 264 25s 855 192 0.01125 8 14 0.10407 0.00021 100% 275 30s 1001 237 0.03296 9 11 0.10407 0.00021 100% 272 35s 1180 257 infeasible 13 0.10407 0.01832 82.4% 269 41s 1373 282 0.03916 9 12 0.10407 0.02321 77.7% 261 46s 1499 277 cutoff 10 0.10407 0.02321 77.7% 259 50s 1713 268 0.07814 14 8 0.10407 0.02830 72.8% 257 55s 1868 272 0.09631 14 8 0.10407 0.03441 66.9% 256 60s 2042 269 infeasible 14 0.10407 0.04175 59.9% 255 65s 2210 264 0.07882 14 8 0.10407 0.04673 55.1% 255 70s 2454 288 0.07419 14 6 0.10407 0.05023 51.7% 251 75s 2725 296 0.05622 13 9 0.10407 0.05375 48.4% 246 81s 2980 286 cutoff 14 0.10407 0.05968 42.7% 244 88s 3097 292 infeasible 12 0.10407 0.06116 41.2% 244 91s 3225 328 0.10222 11 4 0.10407 0.06116 41.2% 243 95s 3466 320 infeasible 13 0.10407 0.06118 41.2% 245 103s Cutting planes: Gomory: 1 Cover: 4 Implied bound: 26 MIR: 9 Flow cover: 13 Inf proof: 6 Explored 3599 nodes (883040 simplex iterations) in 103.15 seconds Thread count was 4 (of 4 available processors) Solution count 8: 0.104073 0.104201 0.105375 ... 0.225148 Optimal solution found (tolerance 4.00e-01) Best objective 1.040731274903e-01, best bound 6.261060501743e-02, gap 39.8398%
tightening_solver
¶The default model build solver has the same type as the main_solver
, but uses the default settings for that solver type other than 1) muting the output and 2) setting a time limit of 20s per solve (i.e. per upper/lower bound per intermediate value).
The most common reason to pass in your own tightening_solver
to modify the time limit per solve.
Whew! That was a lot. The next tutorial will introduce you to everything you can extract from the results dictionary.