SHF: Medium: Collaborative Research: Bridging Automated Formal Reasoning and Continuous Optimization for Provably Safe Deep Learning

SHF：中：协作研究：连接自动形式推理和持续优化以实现可证明安全的深度学习

• 批准号: 1901284
• 负责人: Swarat Chaudhuri
• 金额: $ 50万
• 依托单位: William Marsh Rice University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-07-01 至 2020-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1901284&HistoricalAwards=false
• 关键词: SHF; Medium; Collaborative; Research; Bridging

Deep neural networks have emerged as a transformative computing technology in the last few years. However, as illustrated by recent research on adversarial machine learning, they can behave in obviously erroneous ways on anomalous or adversarial inputs and cannot be debugged using traditional software development methods. Thus, there is an urgent need for developing formal methods techniques that can assure the safety of neural networks, particularly in safety- or security-critical application domains. Motivated by this problem, this project investigates automated formal reasoning techniques for provably safe deep learning. In particular, the investigators explore verification methods for certifying robustness properties of trained networks as well as new verified training methods for finding network parameters that are safe by construction. The technical approach closely couples techniques for automated formal reasoning about systems (in particular abstraction) and continuous optimization. In particular, the project explores the use of automated abstraction techniques, originally developed for reasoning about human-written programs, in the analysis of neural networks. The project investigates the coupling of abstraction and gradient-based optimization in searching for correctness proofs and network parameters. The project introduces undergraduate and high school students from underrepresented groups to research on programming languages and formal methods through outreach programs centered around the topics on artificial intelligence.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.

深度神经网络在过去几年中已成为一种变革性的计算技术。然而，正如最近关于对抗性机器学习的研究所表明的那样，它们可能会在异常或对抗性输入上以明显错误的方式表现，并且无法使用传统的软件开发方法进行调试。 因此，迫切需要开发能够确保神经网络安全的形式化方法技术，特别是在安全或安全关键的应用领域。受这个问题的启发，该项目研究了自动形式推理技术，以实现可证明安全的深度学习。特别是，研究人员探索了用于证明经过训练的网络的鲁棒性属性的验证方法，以及用于寻找构建安全的网络参数的新的经过验证的训练方法。 该技术方法将系统（特别是抽象）的自动形式推理技术与持续优化紧密结合起来。特别是，该项目探索了自动抽象技术在神经网络分析中的使用，该技术最初是为了推理人类编写的程序而开发的。该项目研究了抽象和基于梯度的优化在搜索正确性证明和网络参数中的耦合。该项目通过围绕人工智能主题的推广计划，向来自弱势群体的本科生和高中生介绍编程语言和形式化方法的研究。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值进行评估，被认为值得支持以及更广泛的影响审查标准。