  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.
