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

手工制作复杂的软件是一项困难且容易出错的任务。为了减轻这一困难，工程师们已经开始使用机器学习技术来自动训练深度神经网络，这些神经网络是能够执行各种任务的软件工件。神经网络已被证明在图像识别、语音识别、游戏和许多其他任务方面表现出色，最近甚至有将它们纳入安全关键系统的趋势，例如，as controllers控制器in autonomous自动vehicles车辆. 这引起了人们的担忧，因为确定深度神经网络的正确性和可靠性具有挑战性。神经网络是不透明的，因为它们缺乏人类可以理解的逻辑结构。因此，代码审查和重构等行业最佳实践不适用，工程师很难推理神经网络的行为并保证其正确性。 已经提出了一套新的自动推理神经网络的技术，早期的结果是有希望的，但在可用性和可扩展性有限。 在这个项目中，我们的目标是解决这些障碍，从而使神经网络的自动验证更广泛地应用。该项目汇集了来自斯坦福大学和耶路撒冷的神经网络验证专家，以追求以下研究目标：（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.