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

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. 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.