Neural Network Verification with Proof Production
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.