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

职业：DeepCertify：数据驱动的安全自治正式方法

• 批准号: 2238030
• 负责人: Chuchu Fan
• 金额: $ 52.5万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-02-01 至 2028-01-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2238030&HistoricalAwards=false
• 关键词: CAREER; DeepCertify; Data; driven; Formal

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.

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

项目成果

Signal Temporal Logic Neural Predictive Control

• DOI: 10.1109/lra.2023.3315536
• 发表时间: 2023-09
• 期刊: IEEE Robotics and Automation Letters
• 影响因子: 5.2
• 作者: Yue Meng;Chuchu Fan

Shield Model Predictive Path Integral: A Computationally Efficient Robust MPC Method Using Control Barrier Functions

• DOI: 10.1109/lra.2023.3315211
• 发表时间: 2023-02
• 期刊: IEEE Robotics and Automation Letters
• 影响因子: 5.2
• 作者: Ji Yin;Charles Dawson;Chuchu Fan;P. Tsiotras

Model-Free Neural Fault Detection and Isolation for Safe Control

• DOI: 10.1109/lcsys.2023.3302768
• 发表时间: 2023
• 期刊: IEEE Control Systems Letters
• 影响因子: 3
• 作者: Kunal Garg;Charles Dawson;Kathleen Xu;Melkior Ornik;Chuchu Fan