CheckINN: Wide Range Neural Network Verification in Imandra (Extended)

TL;DR

This paper introduces CheckINN, a library within the Imandra theorem prover, enabling comprehensive neural network verification for safety-critical systems by formalizing neural networks in a unified framework.

Contribution

The paper presents a novel library, CheckINN, integrated into Imandra, to facilitate holistic neural network verification across diverse properties.

Findings

CheckINN effectively formalizes neural networks in Imandra.

It supports verification of various neural network properties.

The approach integrates neural network verification into existing formal methods.

Abstract

Neural networks are increasingly relied upon as components of complex safety-critical systems such as autonomous vehicles. There is high demand for tools and methods that embed neural network verification in a larger verification cycle. However, neural network verification is difficult due to a wide range of verification properties of interest, each typically only amenable to verification in specialised solvers. In this paper, we show how Imandra, a functional programming language and a theorem prover originally designed for verification, validation and simulation of financial infrastructure can offer a holistic infrastructure for neural network verification. We develop a novel library CheckINN that formalises neural networks in Imandra, and covers different important facets of neural network verification.