Career: Correct-by-Learning Methods for Reliable Autonomy

Computing systems that engage people physically with high degrees of autonomy need to provide rigorous guarantees of safety. Formal methods can been used on such systems to provide mathematical proofs to ensure correct behavior. However, machine learning and data-driven approaches are now an indispensable part of autonomous-systems design, and their reliance on highly nonlinear continuous functions and probabilistic reasoning has largely been at odds with the logical and symbolic-analysis frameworks in formal methods.

As a result, the lack of formal assurance has become the key bottleneck that impedes the wider deployment and adoption of autonomous systems. This project targets this open challenge by developing formal synthesis and verification techniques for learning-based and data-driven control and planning methods for autonomous systems.

The project develops the theoretical foundations as well as practical techniques and tools for improving the fundamental reliability of realistic autonomous systems such as autonomous cars and unmanned aerial vehicles. The work builds on the investigator's prior work on formal methods over continuous and hybrid domains towards the unification of symbolic and numerical methods in practical engineering.

The correct-by-learning methods can ensure formal properties of general learning-based decision-making algorithms towards safety and trustworthiness in all areas of AI applications. The education and outreach activities are a crucial part of the project, as the methods developed are only useful if they are adopted by the new generations of developers of autonomous systems in a broad range of engineering domains.

The education efforts contribute directly to improving automation and usability of formal methods in practical engineering.

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.