A Certified Proof Checker for Deep Neural Network Verification in Imandra

TL;DR

This paper introduces a formally verified implementation of DNN certificate checking in Imandra, enhancing trustworthiness and facilitating integration of DNN verification in theorem proving environments.

Contribution

It presents a new Imandra-based implementation of Marabou certificate checking, providing full proof of correctness and stronger independent verification guarantees.

Findings

Full proof of certificate correctness achieved in Imandra

Enhanced trust in DNN verification results

Potential for wider adoption in theorem proving environments

Abstract

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 are themselves complex programs that have been shown to be susceptible to errors and numerical imprecision; this, in turn, has raised the question of trust in DNN verifiers. One prominent attempt to address this issue is enhancing DNN verifiers with the capability of producing certificates of their results that are subject to independent algorithmic checking. While formulations of Marabou certificate checking already exist on top of the state-of-the-art DNN verifier Marabou, they are implemented in C++, and that code itself raises the question of trust (e.g., in the precision of floating point calculations or guarantees for implementation soundness). Here, we present an alternative implementation of the Marabou certificate checking in Imandra -- an industrial functional programming language and an interactive theorem prover (ITP) -- that allows us to obtain full proof of certificate correctness. The significance of the result is two-fold. Firstly, it gives stronger independent guarantees for Marabou proofs. Secondly, it opens the way for the wider adoption of DNN verifiers in interactive theorem proving in the same way as many ITPs already incorporate SMT solvers.