NSF-BSF: SHF: Small: Certifiable Verification of Large Neural Networks

Stanford University, Stanford CA

Investigators

Abstract

Software systems play important roles in almost every area of modern life. In order to reduce the difficulty of developing new software, research in the field of artificial intelligence (AI) has been promoting a new model of programming: instead of having a human engineer design and code algorithms, a set of training examples are used together with machine-learning algorithms to automatically extrapolate software implementations. In classical programing, because such code is written by humans, we can persuade others that it is correct. In machine-learned systems, however, the program amounts to a highly complex mathematical formula for transforming inputs into outputs. The key difficulty, however, is that it is not possible currently to reason about correctness in such systems. This project addresses this issue by developing an algorithm, called Reluplex, capable of proving properties of deep neural networks (DNNs) or providing counter-examples if the properties fail to hold. The project has three main objectives. First, the investigators develop algorithmic techniques to greatly reduce the number of states that need to be explored by a verification tool. Second, they develop a strategy for producing checkable verification proofs. Checkable correctness proofs make it unnecessary to rely on correctness of the verification tool; one can instead rely only on the correctness of a small trusted proof-checker. Finally, the investigators implement this approach in an open-source tool and evaluate it on real-world industrial DNNs. Given that AI components are becoming ubiquitous in safety-critical systems, such as autonomous vehicles, this research will increase trust in these systems. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.