Training Mixed-Monotone Neural Networks for Verification Without Set Propagation

​Most formal verification approaches for neural networks conservatively enclose the output set of the neural network. However, computing a tight output enclosure is in general computationally hard. We sidestep this challenge with a novel neural network architecture that realizes mixed-monotone functions as the difference of monotone subnetworks. By utilizing the theory on mixed-monotone systems, this reduces the computation of a tight output enclosure from complicated set propagation to two simple forward passes of opposite corners of an input interval. Moreover, because the size of resulting enclosure is a closed-form function of the weights of the neural network, we can directly minimize it during training. We prove a lower bound on the size of any such enclosure, given by the monotone variation of the represented function, which makes the tightness of the enclosure measurable against an optimum. Our evaluation uses regression and dynamical-system benchmarks, to demonstrate that our training reaches within $0.5$ of this lower bound at no cost in prediction accuracy. Computing our enclosure is orders of magnitude faster than CROWN and $\alpha$-CROWN and on deep networks it is also tighter than zonotope propagation and CROWN, and stays within $5$ of $\alpha$-CROWN.