Exponential blow-up when translating networks into SMT constraints

[MatthewDaggitt]

I'm trying to get an auto-encoder example up and running and to do so I need to refer to the values of the neurons in the hidden layer inside the constraints, rather than just the network inputs and outputs.

While I was investigating how best to do this, I notice that we don't have an SMT variable for each neuron value but instead just define the expression for the ouput of layer $i$ in terms of the expressions for layer $i - 1$. This means fewer variables, but an exponential blow-up in the size of the final expressions generated.

For example, even with a simple 1 hidden layer network

layer1 : Layer Float 2 1
layer1 = record
  { weights    = [ 3.0 ] ∷ [ 2.0 ] ∷ []
  ; biases     = [ 0.2 ]
  ; activation = relu
  }

layer2 : Layer Float 1 2
layer2 = record
  { weights    = (-2.0 ∷ -1.0 ∷ []) ∷ []
  ; biases     = -0.1 ∷ -0.2 ∷ []
  ; activation = relu
  }

we get the expression: (assert (and (= __1 (ite (<= (+ (- 0.1) (+ (* (ite (<= (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0))) 0.0) 0.0 (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0)))) (- 2.0)) 0.0)) 0.0) 0.0 (+ (- 0.1) (+ (* (ite (<= (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0))) 0.0) 0.0 (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0)))) (- 2.0)) 0.0)))) (and (= __0 (ite (<= (+ (- 0.2) (+ (* (ite (<= (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0))) 0.0) 0.0 (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0)))) (- 1.0)) 0.0)) 0.0) 0.0 (+ (- 0.2) (+ (* (ite (<= (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0))) 0.0) 0.0 (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0)))) (- 1.0)) 0.0)))) true)))

which contains the subexpression (+ (* (ite (<= (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0))) 0.0) 0.0 (+ 0.2 (+ (* __3 3.0) (+ (* __2 2.0) 0.0))) no less then four times.

I'm not sure how clever z3 and marabou are, and if they do common subexpression identification, but even so I'm pretty sure that any solver is going to choke if we continue to take this approach for deeper networks. Not to mention that Amethyst may fall over even generating such expressions.

I would recommend that we switch to generating a variable for the output of each neuron in the network. @wenkokke is there any reason why this representation would have drawbacks? Obviously there's an increase in the number of variables, but I feel like this gives the solvers more flexibility as it is presumably much easier for them to eliminate the extra variables if they want to, but much harder for them to recover them.

[wenkokke]

As far as I know, the first thing Z3 does is inline all let-expressions. Hence, regardless of the input, you'll always get this exponential blowup. However, please do an experiment to test this!

[wenkokke]

For readability it's probably better to generate the let bindings anyway, though?

[MatthewDaggitt]

This has taken me down a rabbit hole :smile: Using let bindings involves adding them to Schmitty which involves adding a fiendish property about indices of reversing lists. Getting there, but not as quick as I'd hoped!