wenkokke/amethyst

Agda library for verifying neural networks.

amethyst's Issues

Exponential blow-up when translating networks into SMT constraints

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.

Unexpected SAT solver conclusions

At the moment I can't seem to get z3 to fail. For example if in AND-Gate-2-Sigmoid-1 we have the following code which type checks fine:

script : Script [] (Reals 2 ++ Reals 1) (SAT ∷ [])
script = withReflectedNetworkAsScript model $ λ where
  -- give names to input and output nodes
  iv@(i₀ ∷ i₁ ∷ []) ov@(o₀ ∷ [])
  -- give remainder of the smt-lib script
    → assert (i₀ == 0·0f ∧ i₁ == 0·0f ⇒ o₀ == 0·0f)
    ∷ assert (i₀ == 0·0f ∧ i₁ == 1·0f ⇒ o₀ == 0·0f)
    ∷ assert (i₀ == 1·0f ∧ i₁ == 0·0f ⇒ o₀ == 0·0f)
    ∷ assert (i₀ == 1·0f ∧ i₁ == 1·0f ⇒ o₀ == 1·0f)
    ∷ check-sat
    ∷ []

_ : z3 script ≡ sat ∷ []
_ = refl

However changing the first assertion to:

assert (i₀ == 0·0f ∧ i₁ == 0·0f ⇒ o₀ == 1·0f)

also appears to type-check which is more than a little worrying....