Correct-by-Learning Methods for Reliable Control

No ratings

Presented at High Confidence Software and Systems Conference 2022 by

Sicun Gao

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.