CheckINN: Wide Range Neural Network Verification in Imandra (Extended)
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Autonomous VehiclesMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
The Imandra Automated Reasoning System (system description)
We describe Imandra, a modern computational logic theorem prover designed to bridge the gap between decision procedures such as SMT, semi-automatic inductive provers of the Boyer-Moore family like ACL2, and interactive p…
A Certified Proof Checker for Deep Neural Network Verification in Imandra
Recent advances in the verification of deep neural networks (DNNs) have opened the way for a broader usage of DNN verification technology in many application areas, including safety-critical ones. However, DNN verifiers …
Automated Theorem ProvingLEMMATowards a Certified Proof Checker for Deep Neural Network Verification
Recent developments in deep neural networks (DNNs) have led to their adoption in safety-critical systems, which in turn has heightened the need for guaranteeing their safety. These safety properties of DNNs can be proven…
Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic
Large Language Models (LLMs) have shown strong performance on code understanding tasks, yet they fundamentally lack the ability to perform precise, exhaustive mathematical reasoning about program behavior. Existing bench…
Mathematical ReasoningSecure access system using signature verification over tablet PC
Low-cost portable devices capable of capturing signature signals are being increasingly used. Additionally, the social and legal acceptance of the written signature for authentication purposes is opening a range of new a…