NSF-BSF: SHF: Small: Neural Network Verification: Abstraction, Compositional Verification and Standardization

Stanford University, Stanford CA

Investigators

Abstract

Manually crafting complex software is a difficult and error-prone task. To mitigate this difficulty, engineers have begun using machine learning techniques to automatically train deep neural networks, which are software artifacts capable of performing a variety of tasks. Neural networks have been shown to excel at image recognition, speech recognition, game playing, and many other tasks, and recently there is even a trend of incorporating them in safety-critical systems, e.g., as controllers in autonomous vehicles. This raises concerns, as determining the correctness and reliability of deep neural networks is challenging. Neural networks are opaque, in the sense that they lack a logical structure that humans can comprehend. Consequently, industry best-practices such as code-reviews and refactoring are inapplicable, and it is highly difficult for engineers to reason about the behavior of neural networks and guarantee their correctness. A new set of techniques for automatically reasoning about neural networks has been proposed, and early results are promising but are limited in usability and scalability. In this project, we aim to address these obstacles and thereby make automatic verification of neural networks more widely applicable. The project brings together experts in neural network verification from Stanford University and from the Hebrew University of Jerusalem in order to pursue the following research goals: (i) develop improved and more scalable neural network verification techniques, using abstraction-refinement and residual reasoning; (ii) further improve scalability by devising hand-crafted and data-driven schemes for the compositional verification of neural networks; and (iii) begin to standardize the field of neural network verification, in order to make the technology and tools accessible to non-experts. These goals will lead to significant advances in the quality and scalability of verification techniques for neural networks and will enable the use of neural networks in many applications that are currently beyond their reach. The project has the potential for substantial impact on education and research across multiple research communities (e.g., verification, machine-learning, artificial intelligence). Also, there will be broader benefits to society as a whole, by allowing the deployment of neural networks in various real-world systems in a safe and reliable way. 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.