# Verification of Sigmoidal Artificial Neural Networks using iSAT

arXiv: https://arxiv.org/abs/2207.06755 · HTML: https://mlsanity.com/paper/2207.06755/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 23 references that are in the map.
- First posted on arXiv 14 Jul 2022.

## Builds on (most cited first, 7 of 7)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Activation Functions: Comparison of trends in Practice and Research for Deep Learning](https://mlsanity.com/paper/1811.03378/) (2018)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [Verification for Machine Learning, Autonomy, and Neural Networks Survey](https://mlsanity.com/paper/1810.01989/) (2018)

## Built on by (most cited first, 1 of 1)

- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)

## Abstract (arXiv)

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.