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

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

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.