SHF: Medium: Rearchitecting Neural Networks for Verification

点击翻译按钮获取中文摘要

Machine learning has the potential to positively impact systems across society, for example, in agriculture, transportation, medicine, energy, and education. To realize that potential, however, methods for assuring the safe operation of those systems are needed. This project addresses this pressing need. Consider the increasing presence of self-driving capabilities in automobiles. They issue warnings when the car drifts outside of the lane and can initiate corrective steering actions. To do this, they employ a neural network to analyze images from a forward-facing camera to detect, for example, the lines that demark lane boundaries. A flaw in this neural network might, for instance, initiate a steering action in the wrong direction and thereby lead to vehicle damage or passenger injury. This project develops techniques for assuring that machine learning produces neural networks that come with guarantees about their behavior. Those guarantees can, in turn, be relied upon when determining that the overall system will operate safely. To achieve verifiably safe machine learning, this project leverages the growing body of work on symbolic verification algorithms for neural networks. These algorithms are cost-prohibitive when applied to existing neural networks. The approach taken in this project searches for and automatically generates an alternative neural network architecture that allows for an appropriate balance between the accuracy of the network and the tractability of verification. Once it finds such an architecture, it employs an iterative counterexample guided refinement approach to training the architecture which results in neural networks that meet essential safety guarantees. The project will organize an annual day-long "Rising Stars" forum for under-represented scholars working in formal methods, software engineering and machine learning.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.