Solving DNN with dreal
Opened this issue · 12 comments
i trained some feed forward neural networks using the mnist dataset with the sigmoid activation and converted them into the smt2 format.
now i want to test specific records of the mnist dataset to see if dreal agrees that when i assign values from a record of a number 7 to the input the output for class 7 is above a certain threshold. i do this with a counter example so i test that the output is below the threshold and expect unsat.
(with a timeout of 12 hours) dreal seems to be only able to solve the smallest networks i trained and it takes at least 5 hours. Other SMT solvers i have tried are able to solve the same tests within a few seconds. Which made me wonder if there is a problem with how i encoded the network in smt2.
Since the other solvers require me to supply intervals for each variable i also tried to add assertions setting the same intervals for each variable in smt2 - which caused dreal to be unable to find a solution within 12 hours (for the test it previously took 5 hours to gain a unsatisfiable result). (i also tested with tight boundaries based on the input i am testing but then i supply directly contradictory assertions and i trivially gain unsat)
With my hope that constraining the variable would help being wrong i thought you guys might have some tips how i can improve the solving time. i attached both smt2 files of the network that took around 5 hours (the one ending in "_ub" is without constrained variables).
Thank you, we'll take a look at the files. It's interesting that adding bounds makes it slower. I suspect that the bounds changed the branching order with negative effects here. FYI in dReal we focus on solving problems with functions that are not piecewise-linear, for instance if your networks use tanh or other transcendental functions then dReal may work better. For linear SMT problems the Simplex-based approach in many SMT solvers can often perform well, which dReal does not implement.
quick update: my first run with bounded variables might have had some other issue. i restarted the file before i opened this "issue" and it just returned unsat (like expected) after 5h20m. Though with other solvers (e.g. iSAT3) taking a few seconds for the same problem i still suspect some issue in my encoding
There is a known issue that can cause inefficiency when there are a lot of variables (>200). I will push a fix soon.
What other solvers have you tested?
currently only iSAT3 and iSAT (technically iSAT2 - weird naming scheme)
i still want to check out marabou
@Krayn , I have a version of dReal which can solve both instances (with and without _ub) in 20sec (on Intel(R) Xeon(R) CPU E5-2686 v4 @ 2.30GHz).
Can you send more instances and also some numbers from other solvers? It might take some time for me to export these commits to the public dReal. I can ping you here when they are ready for export.
i intended to use dreal as a comparable SMT solver for the evaluation of my master thesis. With the deadline when i need to be done with all testruns approaching (2 weeks from now) is there any way i could perhaps get my hands on a preview version with your changes? ;)
my tests were done on a Intel Xeon CPU E5-2650 v4 @ 2.2GHz
mnist_<layers>_<neurons>_0_<options>
<layers>: layers (besides the output layer) the network uses.
<neurons>: total amount of neurons distributed to the layers (+10 for the output layer)
<options>:
- b: boundary optimization 1 or 2 (1=boundaries based on full range of inputs, 2= tight boundaries based on the target i am testing)
- f: for the target irrelevant formula were omitted
mnist_1_250_0_fb1: in my first test this network took 11h20m with dreal. solver times: isat3= 13s | isat2=10.6s
mnist_6_250_0_b1: basically the same as the previous file but with less optimization to the expressions i export. interested in this one cause the presence of the other output neurons causes iSAT3 to find a candidate solution. solver times: isat3=228s | isat2=5.415s
mnist_6_1000_0_fb2: this one expects a candidate solution but i provide very tight boundaries. solver times: isat3=220s | isat2=27s
mnist_6_1500_0_b1: isat3=(running at the moment with 2h+) | isat2=66s
Thanks for sharing the benchmark. I think I can run them over this weekend.
Hey,
did you get a chance to run the 4 files yet? how did they evaluate with your updated version?
is there a estimate on when those changes will be public? (or perhaps it would be possible to get a preview version?)
@Krayn , can you rewrite y = sigmoid(\sum_i c_i x_i) into z = \sum_i c_i x_i and y = sigmoid(z) by introducing an intermediate variable z?
@soonhokong, so instead of (assert (= n_o_7 (sigmoid (+ (* n_6_0 w_0) ... (* n_6_n w_n) b)))) i would encode it like this?
(assert (= n_o_7_h0 (+ (* n_6_0 w_0) ... (* n_6_n w_n) b)))
(assert (= n_o_7 (sigmoid n_o_7_h0)))
i changed the encoding for the 4 files i previously send: smt2.zip
i really hate to be "that guy" constantly asking for a version with your changes, but i need to run ~5000 tests with dReal over this weekend (using the best version i can get my hands on) - thankfully i can run a lot of them in parallel on a cluster so its not unrealistic just yet. How are the chances we can make that happen? :)
@Krayn ,
smt2/mnist_6_1000_0_fb2.smt2 delta-sat 48.241 sec
dreal smt2/mnist_6_1500_0_b1.smt2 unsat 175.84 sec
CPU: Intel(R) Xeon(R) CPU E5-2686 v4 @ 2.30GHz
Can you send an email to Prof. Sicun Gao?
nice, those values seem way more in line with what i expected :)
i have sent him an email