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

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

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.