Verification of Sigmoidal Artificial Neural Networks using iSAT

Dominik Grundt
(German Aerospace Center e.V.)
Sorin Liviu Jurj
(German Aerospace Center e.V.)
Willem Hagemann
(German Aerospace Center e.V.)
Paul Kröger
(Carl von Ossietzky University Oldenburg)
Martin Fränzle
(Carl von Ossietzky University Oldenburg)

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.

In Anne Remke and Dung Hoang Tran: Proceedings The 7th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR 2021), Online, 23rd August 2021, Electronic Proceedings in Theoretical Computer Science 361, pp. 45–60.
Published: 14th July 2022.

ArXived at: https://dx.doi.org/10.4204/EPTCS.361.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org