SHF: Medium: Rearchitecting Neural Networks for Verification

机器学习有可能对整个社会的系统产生积极影响，例如，在农业、交通、医疗、能源和教育领域。然而，为了实现这一潜力，需要确保这些系统安全运行的方法。该项目解决了这一紧迫需求。考虑到汽车中越来越多的自动驾驶功能。当汽车漂移到车道外时，他们会发出警告，并可以启动纠正的转向行动。为了做到这一点，他们使用神经网络来分析来自前置摄像头的图像，以检测例如划分车道边界的线。例如，这种神经网络中的一个缺陷可能会在错误的方向上启动转向操作，从而导致车辆损坏或乘客受伤。这个项目开发了一些技术，以确保机器学习产生的神经网络对它们的行为有保证。反过来，在确定整个系统将安全运行时，可以依赖这些保证。为了实现可验证的安全机器学习，该项目利用了越来越多的神经网络符号验证算法方面的工作。当应用于现有的神经网络时，这些算法的成本令人望而却步。该项目采用的办法是寻找并自动生成一个替代神经网络结构，以便在网络的准确性和核查的可控性之间取得适当的平衡。一旦它找到了这样的体系结构，它就会使用迭代反例指导的精化方法来训练该体系结构，从而产生满足基本安全保证的神经网络。该项目将为在正式方法、软件工程和机器学习方面工作的代表不足的学者组织为期一天的年度“新星”论坛。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.