Neural Network Verification with Proof Production

TL;DR

This paper introduces a proof production mechanism for DNN verifiers to generate easily checkable witnesses of correctness, enhancing trust in verification results for safety-critical systems.

Contribution

It presents a novel method to produce verifiable proofs of DNN correctness using an adaptation of Farkas' lemma, integrated into the Marabou verifier.

Findings

Proof production succeeds in almost all cases

Minimal overhead introduced by the proof generation

Enhances trustworthiness of DNN verification in safety-critical applications

Abstract

Deep neural networks (DNNs) are increasingly being employed in safety-critical systems, and there is an urgent need to guarantee their correctness. Consequently, the verification community has devised multiple techniques and tools for verifying DNNs. When DNN verifiers discover an input that triggers an error, that is easy to confirm; but when they report that no error exists, there is no way to ensure that the verification tool itself is not flawed. As multiple errors have already been observed in DNN verification tools, this calls the applicability of DNN verification into question. In this work, we present a novel mechanism for enhancing Simplex-based DNN verifiers with proof production capabilities: the generation of an easy-to-check witness of unsatisfiability, which attests to the absence of errors. Our proof production is based on an efficient adaptation of the well-known Farkas' lemma, combined with mechanisms for handling piecewise-linear functions and numerical precision errors. As a proof of concept, we implemented our technique on top of the Marabou DNN verifier. Our evaluation on a safety-critical system for airborne collision avoidance shows that proof production succeeds in almost all cases and requires only minimal overhead.