Verification of Sigmoidal Artificial Neural Networks using iSAT

In the age of highly automated systems and the development of autonomous systems, a possible application scenario for ANNs is to use them as controllers for safety-critical cyber-physical systems (CPSes) [9]. Such CPSes capture the often complex environment, analyse the data and make control decisions about the future system behaviour. Guarantees on compliance with safety requirements, e.g., that human lives are not endangered, are of utmost importance. Whenever such guarantees are obtained via formal verification of the system behaviour, an ANN being a component of the system under analysis has also to be subject to verification [23]. The underlying weighted summation of the input neurons before application of the activation function can be represented by simple linear combinations and is therefore very appealing for classical verification methods dealing with linear arithmetic. However, this observation is deceptive when nonlinear activation functions are part of the ANN as such nonlinear functions are often hard to analyse in themselves [23]. Apart from restricted decidability results for reachability problems as in [9], the runtime of algorithms for automatic verification suffers from the multiple occurrence of nonlinear activation functions in complex ANNs such that only relatively small networks could be tackled. Depending on the class of activation functions and the underlying possibly necessary abstractions thereof, recent approaches were able to deal with ANNs comprising 20 to 300 nodes [10, 18, 19]. So-called satisfiability modulo theory (SMT) solvers implement algorithms that search for solutions to Boolean combinations of arithmetic constraints or prove the absence thereof.