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 language | English |
---|---|
Title of host publication | Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming |
Publisher | Association for Computing Machinery |
ISBN (Electronic) | 9781450397032 |
DOIs | |
Publication status | Published - 20 Sept 2022 |
Event | 24th International Symposium on Principles and Practice of Declarative Programming 2022 - Virtual, Online, Georgia Duration: 20 Sept 2022 → 22 Sept 2022 |
Conference
Conference | 24th International Symposium on Principles and Practice of Declarative Programming 2022 |
---|---|
Abbreviated title | PPDP 2022 |
Country/Territory | Georgia |
City | Virtual, Online |
Period | 20/09/22 → 22/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