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

手工制作复杂的软件是一项困难且容易出错的任务。为了缓解这一困难，工程师们已经开始使用机器学习技术来自动训练深度神经网络，深度神经网络是能够执行各种任务的软件制品。神经网络已被证明在图像识别、语音识别、游戏和许多其他任务中表现出色，最近甚至出现了将其整合到安全关键系统中的趋势，例如，作为自动驾驶汽车的控制器。这引发了人们的担忧，因为确定深度神经网络的正确性和可靠性具有挑战性。神经网络是不透明的，因为它们缺乏人类可以理解的逻辑结构。因此，代码审查和重构等行业最佳实践是不适用的，工程师很难对神经网络的行为进行推理并保证其正确性。已经提出了一套关于神经网络的自动推理的新技术，早期的结果是有希望的，但在可用性和可扩展性方面是有限的。在这个项目中，我们的目标是解决这些障碍，从而使神经网络的自动验证得到更广泛的应用。该项目汇集了来自斯坦福大学和耶路撒冷希伯来大学的神经网络验证专家，以追求以下研究目标：(I)利用抽象-精化和残差推理开发改进的、更具可扩展性的神经网络验证技术；(Ii)通过设计手动和数据驱动的神经网络组成验证方案，进一步提高可伸缩性；以及(Iii)开始标准化神经网络验证领域，以便使技术和工具对非专家可用。这些目标将在神经网络验证技术的质量和可扩展性方面取得重大进展，并将使神经网络能够在目前无法实现的许多应用中使用。该项目有可能对多个研究界的教育和研究产生重大影响(例如，验证、机器学习、人工智能)。此外，通过允许以安全可靠的方式在各种真实世界系统中部署神经网络，将给整个社会带来更广泛的好处。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.