Verifying Neural Networks with Non-Linear SMT Solvers: a Short Status Report

In the last couple of decades, the popularity of neural networks has soared and they have been successfully utilized in many different domains across computer science. However, their application in safety and security-critical domains has been limited due to concerns regarding their reliability. Traditional methods for verifying neural networks (NNs) often uses linear Satisfiability Modulo Theory (SMT) solvers. These solvers work well for simple and shallow NN architectures but face limitations regarding their inability to handle non-linear activations, pooling layers, and complex activation functions, commonly used in modern deep neural networks.In this paper, we explore the potential of non-linear SMT solvers to verify intricate neural network architectures. By leveraging non-linear SMT solvers, a wider range of activation functions can be considered, leading to more accurate reasoning about the behavior of complex deep neural networks. The focus is on using recent advancements in SMT solver development to verify NNs with non-linear activation functions, particularly in the context of Computer Vision tasks. To test this idea, we conducted an experimental analysis to assess whether current nonlinear SMT solvers can efficiently handle NNs with transcendent activation functions.