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.