Supplementary Material

Then each deterministic NN in {πw,b | (w,b) Wπ}is safe if and only if the system of constraints Φ(π,X0,Xu,) is not satisfiable. We prove the equivalent claim that there exists a weight vector (w,b) Wπ for which πw,b is unsafe if and only if Φ(π,X0,Xu,) is satisfiable. First, suppose that there exists a weight vector (w,b) Wπ for which πw,b is unsafe and we want to show that Φ(π,X0,Xu,) is satisfiable. This direction of the proof is straightforward since values of the network's neurons on the unsafe input give rise to a solution of Φ(π,X0,Xu,). Indeed, by assumption there exists a vector of input neuron values x0 X0 for which the corresponding vector of output neuron values xl = πw,b(x0) is unsafe, i.e. xl Xu.