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

NSF-BSF：SHF：小型：神经网络验证：抽象、组合验证和标准化

• 批准号: 2211505
• 负责人: Clark Barrett
• 金额: $ 50万
• 依托单位: Stanford University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2211505&HistoricalAwards=false
• 关键词: NSF; BSF; SHF; Small; Neural

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.

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

项目成果

DNN Verification, Reachability, and the Exponential Function Problem

DNN 验证、可达性和指数函数问题

• DOI: 10.48550/arxiv.2305.06064
• 发表时间: 2023-05-10
• 期刊: ArXiv
• 作者: Omri Isac;Yoni Zohar;Clark W. Barrett;Guy Katz
• 通讯作者: Guy Katz

Toward Certified Robustness Against Real-World Distribution Shifts

针对现实世界的分布变化实现经过认证的稳健性

• DOI: 10.1109/satml54575.2023.00042
• 发表时间: 2023-02
• 期刊: 2023 IEEE Conference on Secure and Trustworthy Machine Learning (SaTML
• 作者: Wu, Haoze;Tagomori, Teruhiro;Robey, Alexander;Yang, Fengjun;Matni, Nikolai;Pappas, George;Hassani, Hamed;Pasareanu, Corina;Barrett, Clark
• 通讯作者: Barrett, Clark

Convex Bounds on the Softmax Function with Applications to Robustness Verification

• DOI: 10.48550/arxiv.2303.01713
• 发表时间: 2023-03-03
• 期刊: IEEE Transactions on Control Systems Technology
• 影响因子: 4.8
• 作者: Dennis L. Wei;Haoze Wu;Min Wu;Pin;Clark W. Barrett;E. Farchi
• 通讯作者: E. Farchi

Tighter Abstract Queries in Neural Network Verification

神经网络验证中更严格的抽象查询

• DOI: 10.48550/arxiv.2210.12871
• 发表时间: 2022-10-23
• 期刊: e-Finanse
• 作者: Elazar Cohen;Y. Elboher;Clark W. Barrett;Guy Katz
• 通讯作者: Guy Katz