权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

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

基本信息

批准号：
2033851
负责人：
Swarat Chaudhuri
金额：
$ 50万
依托单位：
University of Texas at Austin
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2020
资助国家：
美国
起止时间：
2020-01-16 至 2024-06-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2033851&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.

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