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

随着机器学习(ML)和神经网络(NN)在实际自治系统中执行更多的任务，迫切需要为数据驱动的方法提供安全和可靠性保证。然而，基于ML的决策方法在很大程度上缺乏适当的认证方法。与此同时，基于形式化方法、控制和编程语言的严格的基于模型的方法为开发许多可靠的硬件和软件系统做出了根本贡献，并可以提供严格的保证。不幸的是，这些严格的方法无法扩展到当今复杂的关键系统。这些项目的创新之处在于将数据驱动方法的有效性和正式方法的严密性结合在一起。该项目正在开发一套新的可认证的数据驱动技术，用于高度挑战的自治系统的控制、设计和风险分析。该项目正在研究这些方法的理论和算法基础，将它们集成到一个统一的设计自动化框架中，并在高级仿真环境和实际硬件平台上彻底评估它们的性能。该项目的影响是1)解决现有方法的不足和较差的可扩展性，并使现有方法无法支持的新系统的设计和分析成为可能；2)允许以安全、可靠和有弹性的方式在各种现实系统中部署NNS。该项目的智力优势在于重新定义了如何在高度复杂的自治和网络物理系统的不同计算级别上提供严格的证书。具体地说，该项目的重点是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.