Correct-by-Learning Methods for Reliable Control

ABSTRACT: Computing systems that engage us physically with high degrees of autonomy pose longstanding challenges to formal methods. In particular, learning-based and data-driven approaches are quickly becoming indispensable in design, but their reliance on highly nonlinear function approximators and probabilistic reasoning has largely been at odds with the logical and symbolic analysis frameworks in formal methods.

These challenges push formal methods in two important directions in the domain of automation and autonomous systems. First, we need to shift from posterior verification to correct-by-construction synthesis, and integrate formal methods with learning-based approaches. Second, new numerical and statistical perspectives on formal methods are critical, and we need to shift from all-or-nothing guarantees to quantitative analysis with risk quantification, for tackling real-world systems with inherent nonlinearity and uncertainty.

I will present our ongoing work along these directions for developing the fundamental theories and practical algorithms for correct-by-learning control synthesis methods. I will connect topics from formal reasoning in nonlinear theories over the reals [3, 5], numerically-robust inductive proof methods [4], and our recent development of neural certificate methods [1, 2]. I will emphasize how learning-based methods can bring exciting opportunities towards a general framework of numerically-driven and sampling-based inductive synthesis and certification methods for highly complex systems.

Sicun Gao received the Ph.D. degree from Carnegie Mellon University and was a Postdoctoral Researcher with MIT. He is an Assistant Professor of Computer Science and Engineering with the University of California at San Diego. He works on search and optimization algorithms for improving the reliability of automation and autonomous systems. He is a recipient of the Amazon Research Award, Air Force Young Investigator Award, the NSF Career Award, and the Silver Medal for the Kurt Godel Research Prize.

You must register and request HCSS Community membership to view the slides.