Solving DNN with dreal

[Krayn]

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).

mnist_6_250_0.zip

[scungao]

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.

[Krayn]

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

[soonhokong]

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?

[Krayn]

currently only iSAT3 and iSAT (technically iSAT2 - weird naming scheme)

i still want to check out marabou

[soonhokong]

@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.

[Krayn]

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

mnist_tests.zip

[soonhokong]

Thanks for sharing the benchmark. I think I can run them over this weekend.

[Krayn]

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?)

[soonhokong]

@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?

[Krayn]

@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? :)

[soonhokong]

@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?

[Krayn]

nice, those values seem way more in line with what i expected :)

i have sent him an email