Verification of Sigmoidal Artificial Neural Networks using iSAT
This work addresses verification challenges for neural networks in cyber-physical systems, though it appears incremental as it builds on existing solver techniques.
The paper tackles the problem of verifying the behavior of nonlinear artificial neural networks in safety-critical systems by implementing a dedicated interval constraint propagator for the sigmoid function in the SMT solver iSAT, showing that this dedicated approach outperforms or matches compositional and approximating methods in performance across benchmarks.
This paper presents an approach for verifying the behaviour of nonlinear Artificial Neural Networks (ANNs) found in cyber-physical safety-critical systems. We implement a dedicated interval constraint propagator for the sigmoid function into the SMT solver iSAT and compare this approach with a compositional approach encoding the sigmoid function by basic arithmetic features available in iSAT and an approximating approach. Our experimental results show that the dedicated and the compositional approach clearly outperform the approximating approach. Throughout all our benchmarks, the dedicated approach showed an equal or better performance compared to the compositional approach.