Neural Network Verification using Polynomial Optimisation

The desire to provide robust guarantees on neural networks has never been more important, as their prevalence in society is increasing. One popular method that has seen a large amount of success is to use bounds on the activation functions within these networks to provide such guarantees. However, due to the large number of possible ways to bound the activation functions, there is a trade-off between conservativeness and complexity. We approach the problem from a different perspective, using polynomial optimisation and real algebraic geometry (the Positivstellensatz) to assert the emptiness of a semi-algebraic set. We show that by using the Positivstellen-satz, bounds on the robustness guarantees can be tightened significantly over other popular methods, at the expense of computational resource. We demonstrate the effectiveness of this approach on networks that use the ReLU, sigmoid and tanh activation functions. This method can be extended to more activation functions, and combined with recent sparsity-exploiting methods can result in a computationally acceptable method for verifying neural networks.