Modified verify_MNIST.jl to use Cbc solver, not sure if results make sense

[gwding]

Thanks for making the code available!

I wonder if we can use opensource solvers other than gurobi? I tried to modify verify_MNIST.jl to work with the Cbc solver. I changed a few lines as below

diff --git a/verification/verify_MNIST.jl b/verification/verify_MNIST.jl
index ec41496..4229f02 100644
--- a/verification/verify_MNIST.jl
+++ b/verification/verify_MNIST.jl
@@ -1,5 +1,6 @@
 using MIPVerify
-using Gurobi
+using Cbc
 using Memento
 using MAT

@@ -64,13 +65,15 @@ MIPVerify.batch_find_untargeted_attack(
     nnparams, 
     mnist.test, 
     target_indexes, 
-    GurobiSolver(Gurobi.Env(), BestObjStop=eps, TimeLimit=120),
+    CbcSolver(logLevel=0, seconds=120),
     save_path="./verification/results/",
     norm_order=Inf, 
     tightening_algorithm=lp,
     rebuild=false,
     cache_model=false,
-    tightening_solver=GurobiSolver(Gurobi.Env(), TimeLimit=5, OutputFlag=0),
+    tightening_solver=CbcSolver(logLevel=0, seconds=5),
     pp = MIPVerify.LInfNormBoundedPerturbationFamily(eps),
     solve_rerun_option = MIPVerify.resolve_ambiguous_cases
 )

It seems working fine, and the output summary.csv file is

SampleNumber,ResultRelativePath,PredictedIndex,TargetIndexes,SolveTime,SolveStatus,IsInfeasible,ObjectiveValue,ObjectiveBound,TighteningApproach,TotalTime
1,run_results/2019-05-02T19.52.59.739.mat,8,"[1, 2, 3, 4, 5, 6, 7, 9, 10]",0.086352886,Infeasible,true,NaN,3.1866333261728703e10,lp,6.521129269
2,run_results/2019-05-02T19.53.03.653.mat,3,"[1, 2, 4, 5, 6, 7, 8, 9, 10]",0.061749633,Infeasible,true,NaN,6.693452020132845e11,lp,2.682452528
3,run_results/2019-05-02T19.53.06.270.mat,2,"[1, 3, 4, 5, 6, 7, 8, 9, 10]",0.288297754,Infeasible,true,NaN,6.554542371807954e17,lp,2.615799405
4,run_results/2019-05-02T19.53.09.420.mat,1,"[2, 3, 4, 5, 6, 7, 8, 9, 10]",0.045987198,Infeasible,true,NaN,1.1491818044076746e9,lp,3.149084084
5,run_results/2019-05-02T19.53.12.644.mat,5,"[1, 2, 3, 4, 6, 7, 8, 9, 10]",0.09831834,Infeasible,true,NaN,1.2510179342277254,lp,3.222982773
6,run_results/2019-05-02T19.53.15.106.mat,2,"[1, 3, 4, 5, 6, 7, 8, 9, 10]",0.031642595,Infeasible,true,NaN,1.179591860002203e10,lp,2.460858959
7,run_results/2019-05-02T19.53.18.079.mat,5,"[1, 2, 3, 4, 6, 7, 8, 9, 10]",0.066266113,Infeasible,true,NaN,2.590479130869372e11,lp,2.972294522
8,run_results/2019-05-02T19.55.20.897.mat,10,"[1, 2, 3, 4, 5, 6, 7, 8, 9]",120.007724715,UserLimit,false,1.0e50,0.0034081529708412436,lp,122.774540739
9,run_results/2019-05-02T19.57.24.077.mat,6,"[1, 2, 3, 4, 5, 7, 8, 9, 10]",120.364612323,UserLimit,false,1.0e50,0.0023767065588710342,lp,123.147846327
10,run_results/2019-05-02T19.57.35.653.mat,10,"[1, 2, 3, 4, 5, 6, 7, 8, 9]",8.264824407,Infeasible,true,NaN,1.0e50,lp,11.575389875

Could you help verify if this is working as expected? Thanks!

[kaixiao]

Hi,

This output looks fine to me, and should be the same as (or at least similar to) what using Gurobi will give you. Gurobi may be a bit faster in certain cases though, which could decrease the number of samples the verifier times out on.

[gwding]

@kaixiao That's great! thx! Having another question: for Gurobi, there's a parameter BestObjStop=eps. I cannot find the same parameter in Cbc. Is this just an "early stopping" criterion?