CAREER: DeepCertify: Data-driven Formal Approach to Safe Autonomy

随着机器学习（ML）和神经网络（NN）在现实世界的自治系统中执行更多任务，迫切需要为数据驱动方法提供安全性和可靠性保证。然而，基于ML的决策方法在很大程度上缺乏适当的认证方法。与此同时，基于形式化方法、控制和编程语言的严格的基于模型的方法为开发许多可靠的硬件和软件系统做出了根本性的贡献，并可以提供严格的保证。 不幸的是，这些严格的方法不能扩展到今天的复杂的关键系统。这些项目的新颖之处在于将数据驱动方法的有效性和正式方法的严谨性联合收割机结合起来。该项目正在开发一套新的可认证的数据驱动技术，用于高度挑战性的自主系统的控制、设计和风险分析。该项目正在研究这些方法的理论和算法基础，将它们集成到一个统一的设计自动化框架中，并在先进的仿真环境和实际硬件平台上彻底评估它们的能力。该项目的影响是1）解决现有方法的不足和可扩展性差，并使现有方法无法支持的新系统的设计和分析成为可能; 2）允许以安全，可靠和弹性的方式在各种现实世界的系统中部署NN。该项目的智力价值是重新定义如何为高度复杂的自主和网络物理系统提供不同计算级别的严格证书。具体而言，该项目的重点是1）开发新型数据驱动控制方法，可以处理传统基于模型的方法无法处理的高度复杂系统。这些方法将为最终的闭环系统提供安全性，鲁棒性和弹性的数学证书，这些证书在纯数据驱动的方法中通常是缺失的。2)开发新的数据驱动设计方法，实现全自治堆栈的端到端优化，并通过执行程序级符号敏感性分析提供鲁棒性证书。3)探索基于哈密顿力学的随机验证方法，开发新的策略抽样方法，以增加训练样本中的罕见情况。该方法可以减少执行中不可预见的行为，提高数据驱动方法的采样效率。研究人员正在与行业合作伙伴密切合作，以转移研究成果，并使用他们的现实问题/数据来产生具有挑战性的研究问题。研究人员正在通过多种渠道传播该项目的结果，在顶级AI/ML和正式方法会议上建立安全自治的永久身份，并促进顶级工程项目的多样性。调查员正在创建一个新的课程，将该项目的所有成果和资源纳入课程，并向公众提供。研究者有一个具体的路线图，通过麻省理工学院本科生研究机会计划，麻省理工学院夏季研究计划和麻省理工学院少数民族教育办公室的长期合作，将妇女和代表性不足的少数民族本科生纳入研究活动。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

Providing safety and reliability assurances for data-driven methods is urgently needed as Machine Learning (ML) and Neural Networks (NN) perform more tasks in real-world autonomous systems. However, ML-based approaches for decision-making largely lack appropriate methods for certification. In the meantime, rigorous model-based approaches based on Formal Methods, control, and programming languages have made fundamental contributions to developing many reliable hardware and software systems and can provide rigorous guarantees. Unfortunately, these rigorous approaches cannot scale to today's complex critical systems. The projects’ novelties are to combine the effectiveness of data-driven methods and the rigor of formal approaches. The project is developing a novel set of certifiable data-driven technologies for the control, design, and risk analysis of highly challenging autonomous systems. The project is investigating theoretical and algorithmic foundations of the methods, integrating them into a unified design automation framework, and evaluating their capability thoroughly in advanced simulation environments and on practical hardware platforms. The project’s impacts are 1) addressing the insufficiency and poor scalability of existing methods and enabling the design and analysis of new systems that existing methods cannot support; and 2) allowing the deployment of NNs in various real-world systems in a safe, reliable, and resilient way. This project's intellectual merit is redefining how to provide rigorous certificates at different levels of computation for highly complex autonomous and cyber-physical systems. Specifically, the project is focusing on 1) Developing novel data-driven control methods that can handle highly complex systems beyond the capability of traditional model-based approaches. The methods will provide the resulting closed-loop systems with mathematical certificates for safety, robustness, and resiliency, which are often missing in pure data-driven approaches. 2) Developing novel data-driven design methods that enable end-to-end optimization of the full autonomy stack and provide certificates of robustness by performing program-level symbolic sensitivity analysis. 3) Exploring stochastic verification methods based on Hamiltonian mechanics to develop novel strategic sampling methods to increase rare case appearances in training samples. The methods can reduce unforeseen behaviors in executions and improve the sampling efficiency of the data-driven methods. The investigator is working closely with industry partners to transfer research results and use their real-world problems/data to generate challenging research problems. The investigator is disseminating the project's results through multiple channels, establishing the permanent identity of safe autonomy in top AI/ML and Formal Methods conferences, and promoting diversity in top engineering programs. The investigator is creating a new course, incorporating all results and resources in this project into the course and making them publicly available. The investigator has a concrete roadmap to integrate women and underrepresented minority undergraduate students into research activities through the MIT undergraduate research opportunities program, MIT summer research program and the long-term collaboration of the MIT Office of Minority Education.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.