1
$\begingroup$

I was reading [1] about reachability analysis of a feed forward neural network (FFNN). The paper encodes a FFNN as a linear programming problem. Suppose $x^{(i)}$ is the vector output of the ith layer, $W^{(i)}$ is the weight matrix corresponding to layer i, and $b^{(i)}$ is the bias vector. So by definition, the output of the ith layer, $x^{(i)}$, should be $x_j^{(i)} = W_j^{(i)}x^{(i-1)} + b_j^{(i)}$.

On page 4, under definition 7, I understand the constraint $x_j^{(i)} \ge W_j^{(i)}x^{(i-1)} + b_j^{(i)}$.

But for the next constraint, I don't get where $\delta^{(i)}$ and M come from? I thought the constraint $x_j^{(i)} \le W_j^{(i)}x^{(i-1)} + b_j^{(i)} + M\delta^{(i)}_j$ was because the FFNN is considered to have a ReLU activation function, so the $M\delta^{(i)}_j$ will bring the value upto 0 in case $W_j^{(i)}x^{(i-1)} + b_j^{(i)}$ is negative. But how are they chosen and why is $x_j^{(i)} \le M(1 - \delta^{(i)}_j$)

References

  1. An approach to reachability analysis for feed-forward ReLU neural networks by Alessio Lomuscio, Lalit Maganti (June 2017)
$\endgroup$
0

1 Answer 1

0
$\begingroup$

The idea is that $\delta_j^{(i)}=1$ means that the input to the ReLU was negative (so its output is zero), and $\delta_j^{(i)}=0$ means that the input to the ReLU was positive (so its output is positive).

You can then verify that both equations make sense. In particular, I suggest you consider separately the case where $\delta_j^{(i)}=0$ (and thus $W_j^{(i)}x^{(i-1)}+b_j^{(i)} \ge 0$ from the case where $\delta_j^{(i)}=1$ (and thus $W_j^{(i)}x^{(i-1)}+b_j^{(i)} \le 0$). You will see that this program correctly captures the constraints for both cases, forcing $x^{(i)}_j = W_j^{(i)}x^{(i-1)}+b_j^{(i)}$ in the former case and forcing $x^{(i)}_j = 0$ in the latter case, which correctly captures the behavior of the neural network and the ReLU unit.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.