CheckINN: Wide Range Neural Network Verification in Imandra

Remi Desmartin, Grant Passmore, Ekaterina Komendantskaya, Matthew Daggit

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish
Title of host publicationProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming
PublisherAssociation for Computing Machinery
ISBN (Electronic)9781450397032
DOIs
Publication statusPublished - 20 Sep 2022
Event24th International Symposium on Principles and Practice of Declarative Programming 2022 - Virtual, Online, Georgia
Duration: 20 Sep 202222 Sep 2022

Conference

Conference24th International Symposium on Principles and Practice of Declarative Programming 2022
Abbreviated titlePPDP 2022
Country/TerritoryGeorgia
CityVirtual, Online
Period20/09/2222/09/22

Keywords

  • Boyer-Moore Provers
  • Neural Networks
  • Robustness
  • Verification

ASJC Scopus subject areas

  • Human-Computer Interaction
  • Computer Networks and Communications
  • Computer Vision and Pattern Recognition
  • Software

Fingerprint

Dive into the research topics of 'CheckINN: Wide Range Neural Network Verification in Imandra'. Together they form a unique fingerprint.

Cite this