CheckINN: Wide Range Neural Network Verification in Imandra (Extended)
This provides a tool for verifying neural networks in safety-critical domains like autonomous vehicles, though it appears incremental as it adapts an existing theorem prover to neural networks.
The authors tackled the challenge of verifying neural networks in safety-critical systems by developing CheckINN, a library in Imandra that formalizes neural networks and covers multiple verification facets, enabling holistic verification infrastructure.
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.