Verifying the example neural net was all well and good, but you probably want to verify your own neural net now. In this tutorial, we show you how to import the parameters for a feed-forward neural net with an architecture of your choice.
using MIPVerify
using Gurobi
using MAT
We'll download a .mat
file containing the parameters of a sample neural net containing three layers (exported from tensorflow
).
param_dict = Base.download("https://github.com/vtjeng/MIPVerify_data/raw/master/weights/mnist/n2.mat") |> matread
Dict{String,Any} with 26 entries: "fc1/weight" => Float32[0.000222324 6.78186f-6 … 0.00111799 -0.0005… "fc3/weight/Adam_1" => Float32[4.4054f-5 7.04086f-5 … 2.05744f-5 1.5445f-5… "logits/bias/Adam_1" => Float32[9.47849f-6 1.14659f-5 … 2.12202f-5 2.5675f-… "fc1/bias" => Float32[0.675125 -0.372304 … 0.540256 -0.468334] "fc3/bias" => Float32[0.239015 1.05777 … 1.87256 1.10636] "logits/weight/Adam_1" => Float32[9.73416f-5 7.37292f-5 … 0.000153108 0.00013… "fc2/weight/Adam_1" => Float32[0.000456424 0.000191762 … 9.0507f-5 5.83681… "fc2/bias" => Float32[1.89861 1.58582 … -0.54874 1.00736] "fc3/bias/Adam_1" => Float32[3.96812f-6 6.44411f-6 … 4.03203f-6 1.96784f… "logits/bias/Adam" => Float32[-0.00108494 0.000629807 … 0.000172997 0.001… "beta1_power" => 0.0 "fc2/bias/Adam" => Float32[0.00093958 0.000148308 … -0.000481088 -0.00… "logits/bias" => Float32[-0.167159 0.670988 … -0.163606 0.0620176] "fc1/weight/Adam" => Float32[2.61229f-9 2.50404f-8 … 9.15141f-9 -1.26372… "fc3/weight/Adam" => Float32[0.000514265 0.00114447 … 6.09192f-5 0.00064… "fc2/weight" => Float32[-0.243556 -0.232867 … 0.23907 -0.82437; 0.1… "fc3/bias/Adam" => Float32[0.000412472 7.06436f-5 … -2.81073f-5 0.0001… "logits/weight" => Float32[0.106404 0.587075 … 0.310872 0.152626; 0.02… "fc1/weight/Adam_1" => Float32[5.76757f-14 2.20114f-14 … 2.44297f-14 4.312… "fc2/weight/Adam" => Float32[0.0121755 0.00166487 … -0.00550308 -0.00305… "beta2_power" => 0.0 "fc3/weight" => Float32[0.18034 -0.119679 … -0.0579543 0.0819598; -… "fc1/bias/Adam" => Float32[-9.24088f-6 0.000377022 … -0.000173221 -0.0… "fc1/bias/Adam_1" => Float32[2.21867f-5 9.82018f-6 … 1.34117f-5 2.2821f-… "logits/weight/Adam" => Float32[-0.00350437 0.000921413 … 0.000551378 0.002… ⋮ => ⋮
Let's begin by importing the parameters for the first fully connected layer, which has 784 inputs (corresponding to a flattened 28x28 image) and 24 outputs.
We begin with a basic approach where we extract the weights and the biases of the fully connected layer seperately.
fc1_weight = param_dict["fc1/weight"]
784×24 Array{Float32,2}: 0.000222324 6.78186f-6 0.000211635 … 0.00111799 -0.00055723 0.000270549 -0.000155775 0.000345145 0.0011448 -0.000638638 0.00157308 0.00294467 0.00133911 -0.00275523 0.00436651 0.00124757 -4.55079f-5 0.000364477 0.000844778 0.00030634 0.000181523 7.54999f-5 0.000184328 0.000718589 -0.000354625 0.00100992 -0.00056507 0.000376461 … 0.00108511 -2.14134f-5 0.0011267 0.00277671 0.00199021 -0.00308363 0.0037927 0.00172865 0.00107658 0.000331343 -0.000169128 0.00168143 -0.00152659 -0.0020568 0.000401156 0.00151572 -0.000661888 0.000884574 -0.000527718 0.000382487 0.00106229 -4.86445f-5 0.00147657 0.00275898 0.00151834 … -0.00248229 0.00379858 -3.01078f-5 0.000446275 0.000935425 -0.00300283 0.00124241 2.6066f-5 0.000116717 3.48966f-6 -0.000166195 0.000101932 ⋮ ⋱ -0.0616022 -0.00453137 0.0187155 -0.0498921 -0.0245561 0.0195578 0.00215033 -0.0438484 -0.0184708 -0.0380633 0.0591205 0.0328315 -0.0641472 -0.0294263 -0.0802063 0.10835 0.00218356 0.00843114 … -0.0408395 -0.0159919 0.0664918 -0.0229892 0.0143863 0.0794955 0.0215239 -0.00811535 0.0067625 0.00549217 0.0318993 0.0041776 -0.0132527 -0.110216 0.0162308 -0.00244502 0.0169465 5.43133f-5 -3.70874f-5 9.81464f-5 0.000183623 0.000160505 0.00131112 6.32279f-5 0.000345392 … 0.000886682 0.000304327 5.60821f-6 0.000752103 0.00101124 -0.00320989 0.0014562 0.000598289 0.00211266 0.00166339 -0.00337056 0.00261424 -0.00185165 -0.00284901 0.00128107 0.00113743 -0.00045202
fc1_bias = param_dict["fc1/bias"]
1×24 Array{Float32,2}: 0.675125 -0.372304 -0.202615 … -0.0190356 0.540256 -0.468334
We group the weights and biases in a Linear
.
(NB: We have to flatten the bias layer using squeeze
since Linear
expects a 1-D array for the bias.)
fc1_manual = Linear(fc1_weight, squeeze(fc1_bias, 1))
Linear(784 -> 24)
That was a lot to remember. Wouldn't it be nice if there was a helper function to take care of all that?
fc1 = get_matrix_params(param_dict, "fc1", (784, 24))
Linear(784 -> 24)
get_matrix_params
requires that 1) you specify the expected size of the layer, and 2) your weight and bias arrays following the naming convention outlined in the [documentation](https://vtjeng.github.io/MIPVerify.jl/stable/utils/import_weights.html#MIPVerify.get_matrix_params-Tuple%7BDict%7BString,V%7D where V,String,Tuple{Int64,Int64}}).
As a sanity check, you can verify that the parameters we get from both methods are equal.
fc1_manual == fc1
true
Since we followed the naming convention required by get_matrix_params
when exporting our neural net parameters as a .mat
file, importing the rest of the neural net is relatively straightforward.
fc2 = get_matrix_params(param_dict, "fc2", (24, 24))
Linear(24 -> 24)
fc3 = get_matrix_params(param_dict, "fc3", (24, 24))
Linear(24 -> 24)
logits = get_matrix_params(param_dict, "logits", (24, 10))
Linear(24 -> 10)
We now put the entire network together. We need to flatten the input since the input images are provided as a 4-dimensional tensor. (Note that there is no ReLU
after the softmax layers).
nn = Sequential([
Flatten(4),
fc1,
ReLU(),
fc2,
ReLU(),
fc3,
ReLU(),
logits
], "MNIST.n2")
sequential net MNIST.n2 (1) Flatten(): flattens 4 dimensional input, with dimensions permuted according to the order [4, 3, 2, 1] (2) Linear(784 -> 24) (3) ReLU() (4) Linear(24 -> 24) (5) ReLU() (6) Linear(24 -> 24) (7) ReLU() (8) Linear(24 -> 10)
It's important to make sure that you imported the network correctly. We do this by passing in images from the test set.
mnist = read_datasets("MNIST")
MIPVerify.frac_correct(nn, mnist.test, 10000)
Computing fraction correct...100%|██████████████████████| Time: 0:00:04
0.9706
Finally, we find an adversarial example for a sample input.
sample_image = MIPVerify.get_image(mnist.test.images, 1);
MIPVerify.find_adversarial_example(nn, sample_image, 4, GurobiSolver())
[notice | MIPVerify]: Attempting to find adversarial example. Neural net predicted label is 8, target labels are [4] [notice | MIPVerify]: Loading model from cache.
Dict{Any,Any} with 10 entries: :PerturbationFamily => unrestricted :TargetIndexes => [4] :SolveStatus => :Optimal :TotalTime => 453.259 :TighteningApproach => "loaded_from_cache" :Output => JuMP.GenericAffExpr{Float64,JuMP.Variable}[0.106403902… :PredictedIndex => 8 :Model => Minimization problem with:… :Perturbation => JuMP.Variable[__anon__ __anon__ __anon__ __anon__ __an… :PerturbedInput => JuMP.Variable[__anon__ __anon__ __anon__ __anon__ __an…
Academic license - for non-commercial use only Optimize a model with 3433 rows, 3280 columns and 46856 nonzeros Variable types: 3208 continuous, 72 integer (72 binary) Coefficient statistics: Matrix range [2e-07, 6e+02] Objective range [1e+00, 1e+00] Bounds range [1e+00, 2e+02] RHS range [4e-03, 6e+02] MIP start did not produce a new incumbent solution MIP start violates constraint R1072 by 2.000000000 Presolve removed 2978 rows and 2237 columns Presolve time: 0.12s Presolved: 455 rows, 1043 columns, 40972 nonzeros Variable types: 971 continuous, 72 integer (72 binary) Root relaxation: objective 0.000000e+00, 266 iterations, 0.00 seconds Nodes | Current Node | Objective Bounds | Work Expl Unexpl | Obj Depth IntInf | Incumbent BestBd Gap | It/Node Time 0 0 0.00000 0 8 - 0.00000 - - 0s Another try with MIP start 0 0 0.00000 0 7 - 0.00000 - - 0s 0 0 0.00000 0 7 - 0.00000 - - 0s 0 0 0.00000 0 7 - 0.00000 - - 0s 0 0 0.00000 0 7 - 0.00000 - - 0s 0 0 0.00000 0 7 - 0.00000 - - 0s 0 2 0.00000 0 7 - 0.00000 - - 0s * 133 114 43 14.4415669 0.00000 100% 84.3 1s * 134 114 43 14.3849444 0.00000 100% 83.7 1s * 319 198 47 12.5446268 0.00000 100% 73.4 2s * 710 191 42 5.1341983 0.00000 100% 58.3 3s 800 249 0.00000 19 14 5.13420 0.00000 100% 60.0 5s 2008 442 3.09206 44 10 5.13420 0.00000 100% 70.5 10s 3137 739 cutoff 41 5.13420 0.00000 100% 70.5 15s 4397 945 5.01483 37 16 5.13420 0.00000 100% 78.1 20s 5622 1130 cutoff 41 5.13420 0.00000 100% 83.7 25s 7078 1379 0.00000 32 8 5.13420 0.00000 100% 85.0 30s 8417 1570 0.11702 37 8 5.13420 0.00000 100% 84.2 35s 9959 1762 cutoff 37 5.13420 0.00000 100% 84.0 41s 11285 2021 3.62406 46 10 5.13420 0.00000 100% 82.8 45s 12409 2125 cutoff 35 5.13420 0.09879 98.1% 82.8 50s 13388 2184 cutoff 27 5.13420 0.09879 98.1% 83.4 55s 14471 2360 2.44113 37 10 5.13420 0.09879 98.1% 82.7 60s 14738 2360 cutoff 39 5.13420 0.09879 98.1% 82.6 67s 15592 2539 cutoff 35 5.13420 0.09879 98.1% 81.4 70s 16550 2694 2.97794 35 14 5.13420 0.24907 95.1% 81.1 75s 17872 2929 0.45926 53 15 5.13420 0.25148 95.1% 80.3 80s 19005 2983 cutoff 49 5.13420 0.28042 94.5% 80.3 85s 20558 3106 cutoff 34 5.13420 1.03419 79.9% 78.8 90s 22258 3419 3.99255 43 8 5.13420 1.03419 79.9% 77.6 95s 23426 3551 2.31137 22 13 5.13420 1.14615 77.7% 77.6 100s 24747 3829 cutoff 47 5.13420 1.15887 77.4% 77.3 105s 26427 4038 cutoff 42 5.13420 1.31157 74.5% 77.1 110s 27757 4338 cutoff 33 5.13420 1.39205 72.9% 76.6 115s 29783 4782 cutoff 31 5.13420 1.39205 72.9% 75.5 120s 31093 4878 4.78511 42 11 5.13420 1.47824 71.2% 75.2 125s 32781 4909 cutoff 45 5.13420 1.67023 67.5% 74.6 130s 34518 5166 1.78849 30 9 5.13420 1.78849 65.2% 74.0 135s 36269 5183 cutoff 35 5.13420 2.00518 60.9% 73.3 140s 37892 5278 cutoff 33 5.13420 2.17270 57.7% 72.4 145s 39199 5449 3.19121 45 5 5.13420 2.30521 55.1% 72.1 150s 40923 5770 cutoff 42 5.13420 2.40072 53.2% 71.4 155s 42647 5931 cutoff 50 5.13420 2.58550 49.6% 70.5 160s 44180 6140 4.56141 42 13 5.13420 2.61536 49.1% 70.2 165s 45421 6226 cutoff 44 5.13420 2.66845 48.0% 70.0 170s H45423 6209 5.1055740 2.66845 47.7% 70.0 170s 46692 6186 cutoff 33 5.10557 2.74915 46.2% 69.6 175s 48246 6233 4.46384 26 8 5.10557 2.79321 45.3% 69.5 180s 49747 6276 cutoff 49 5.10557 2.80482 45.1% 69.3 185s 50765 6348 cutoff 32 5.10557 2.89587 43.3% 68.9 190s 52291 6494 3.09436 45 4 5.10557 2.95194 42.2% 68.7 195s 53995 6704 cutoff 41 5.10557 2.96690 41.9% 68.5 200s 55581 6700 cutoff 29 5.10557 3.02969 40.7% 68.3 205s 57209 6867 cutoff 24 5.10557 3.07073 39.9% 68.4 210s 58798 7014 cutoff 47 5.10557 3.07176 39.8% 68.3 215s 60388 7170 3.10431 45 11 5.10557 3.10431 39.2% 68.1 220s 62105 7165 cutoff 43 5.10557 3.16047 38.1% 67.7 225s 63614 7203 cutoff 40 5.10557 3.19121 37.5% 67.8 230s 65257 7277 3.72395 38 9 5.10557 3.24856 36.4% 67.6 235s 66976 7205 cutoff 45 5.10557 3.33423 34.7% 67.2 240s 68454 7146 4.64629 42 11 5.10557 3.39981 33.4% 67.1 245s 70297 7196 cutoff 39 5.10557 3.45059 32.4% 66.7 250s 72123 7234 cutoff 44 5.10557 3.49544 31.5% 66.4 255s 73596 7234 cutoff 40 5.10557 3.51543 31.1% 66.3 260s 75138 7192 cutoff 40 5.10557 3.56993 30.1% 66.2 265s 76691 7141 cutoff 48 5.10557 3.60170 29.5% 66.1 270s 78323 7118 4.39089 44 10 5.10557 3.64162 28.7% 65.9 275s 79696 7170 cutoff 53 5.10557 3.66398 28.2% 65.9 280s 81311 7128 3.79648 49 8 5.10557 3.67904 27.9% 65.7 285s 83091 7021 cutoff 37 5.10557 3.72884 27.0% 65.5 290s 84883 6877 3.77694 42 10 5.10557 3.77694 26.0% 65.3 295s 86595 6918 cutoff 46 5.10557 3.79744 25.6% 65.0 300s 88254 7037 cutoff 44 5.10557 3.80989 25.4% 64.8 305s 89791 6956 cutoff 44 5.10557 3.82785 25.0% 64.8 310s 91563 6737 cutoff 51 5.10557 3.88723 23.9% 64.7 315s 93363 6550 4.01903 48 9 5.10557 3.95118 22.6% 64.4 320s 94130 6479 cutoff 42 5.10557 3.95947 22.4% 64.3 325s 96036 6300 4.01363 43 8 5.10557 4.01363 21.4% 64.1 330s 97820 6147 4.83081 43 8 5.10557 4.06843 20.3% 63.8 335s 99448 5928 cutoff 42 5.10557 4.12342 19.2% 63.6 340s 101179 5760 cutoff 45 5.10557 4.16595 18.4% 63.4 345s 103033 5613 4.18795 49 7 5.10557 4.18795 18.0% 63.2 350s 104684 5464 cutoff 40 5.10557 4.22171 17.3% 63.1 355s 106484 5277 cutoff 43 5.10557 4.26588 16.4% 62.9 360s 108332 5063 4.30721 46 13 5.10557 4.30721 15.6% 62.6 365s 110218 4803 4.37518 45 7 5.10557 4.36627 14.5% 62.3 370s 112155 4558 cutoff 33 5.10557 4.41341 13.6% 62.1 375s 113981 4419 4.62845 45 10 5.10557 4.45049 12.8% 61.9 380s 115757 4050 cutoff 46 5.10557 4.51171 11.6% 61.7 385s 117176 3970 4.53926 44 4 5.10557 4.52701 11.3% 61.8 390s 119200 3572 4.67046 49 8 5.10557 4.60931 9.72% 61.5 395s 120997 3355 cutoff 37 5.10557 4.64912 8.94% 61.3 400s 122556 3243 4.85377 44 12 5.10557 4.67485 8.44% 61.2 405s 124483 3048 cutoff 40 5.10557 4.72871 7.38% 61.0 410s 125890 2768 cutoff 45 5.10557 4.76106 6.75% 60.9 415s 127607 2401 cutoff 39 5.10557 4.82487 5.50% 60.7 420s 129287 2163 4.91553 49 10 5.10557 4.85019 5.00% 60.7 425s 131183 1711 cutoff 42 5.10557 4.89693 4.09% 60.4 430s 133149 1146 cutoff 45 5.10557 4.94941 3.06% 60.1 435s 134855 675 5.00584 42 5 5.10557 5.00584 1.95% 59.9 440s 136122 285 5.05498 44 8 5.10557 5.05498 0.99% 59.9 445s Cutting planes: Gomory: 1 Cover: 1 Projected implied bound: 63 MIR: 19 Flow cover: 15 Explored 137313 nodes (8224081 simplex iterations) in 449.03 seconds Thread count was 4 (of 4 available processors) Solution count 5: 5.10557 5.1342 12.5446 ... 14.4416 Optimal solution found (tolerance 1.00e-04) Best objective 5.105574049955e+00, best bound 5.105574049955e+00, gap 0.0000%
There we go! Now it's your turn to try to verify your own neural network.