Verification of Sigmoidal Artificial Neural Networks using iSAT

TL;DR

This paper introduces a specialized verification method for sigmoid-based neural networks in safety-critical systems by integrating a dedicated interval constraint propagator into the iSAT solver, outperforming approximation methods.

Contribution

It develops a dedicated interval constraint propagator for sigmoid functions in iSAT, improving verification efficiency over existing approximation techniques.

Findings

Dedicated approach outperforms approximation methods

Dedicated and compositional approaches outperform in benchmarks

Dedicated approach shows equal or better performance than compositional

Abstract

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.