Neural Networks in Imandra: Matrix Representation as a Verification Choice

TL;DR

This paper explores how the functional programming language Imandra can be used to formalize neural network verification, focusing on how different matrix representations affect automation and effectiveness.

Contribution

It demonstrates the application of Imandra's functional and theorem-proving features to neural network verification, emphasizing the impact of matrix implementation choices.

Findings

Matrix representation choices influence verification automation.

Imandra enables formal reasoning about neural networks.

Different matrix implementations can improve verification efficiency.

Abstract

The demand for formal verification tools for neural networks has increased as neural networks have been deployed in a growing number of safety-critical applications. Matrices are a data structure essential to formalising neural networks. Functional programming languages encourage diverse approaches to matrix definitions. This feature has already been successfully exploited in different applications. The question we ask is whether, and how, these ideas can be applied in neural network verification. A functional programming language Imandra combines the syntax of a functional programming language and the power of an automated theorem prover. Using these two key features of Imandra, we explore how different implementations of matrices can influence automation of neural network verification.