# Linear encoding of a feed forward neural network

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)

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.