Neural Network Verification with Proof Production

“Neural Network Verification with Proof Production” by Omri Isac, Clark Barrett, Min Zhang, and Guy Katz. In Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), (Alberto Griggio and Neha Rungta, eds.), Oct. 2022, pp. 38-48.

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.

BibTeX entry:

@inproceedings{IBZ+22,
   author = {Omri Isac and Clark Barrett and Min Zhang and Guy Katz},
   editor = {Alberto Griggio and Neha Rungta},
   title = {Neural Network Verification with Proof Production},
   booktitle = {Proceedings of the {\it 22^{nd}} International Conference
	on Formal Methods In Computer-Aided Design (FMCAD '22)},
   pages = {38--48},
   publisher = {TU Wien Academic Press},
   month = oct,
   year = {2022},
   doi = {10.34727/2022/isbn.978-3-85448-053-2_9},
   url = {http://theory.stanford.edu/~barrett/pubs/IBZ+22.pdf}
}

(This webpage was created with bibtex2web.)