IST LUNCH BUNCH

Abstract: Learning offers new opportunities for autonomous systems to acquire skills, adapt to their environment and to infer user preferences. On the other hand, existing learning algorithms often lack verifiable guarantees---necessary for autonomous systems---in terms of formal safety and mission specifications. 

 

We present a series of learning algorithms at the intersection of learning theory and formal methods. A common feature in these recently developed algorithms is the guarantees they provide during both training and execution with respect to given formal specifications expressed in variants of temporal logic. The first algorithm merges data efficiency notions (e.g., so-called probably approximate correctness) from reinforcement learning with probabilistic specifications. The second one builds on reactive synthesis from formal methods to construct run-time error correction modules. When implemented along with a system learning through reinforcement, the error correction module monitors and overwrites the system's decisions only if a violation of the underlying safety specifications is to become inevitable and for the shortest period necessary so that other desirable properties of the underlying learning algorithm are conserved. The third algorithm is for learning from demonstration in a setting in which extra side information about the demonstration source is available, and encoded as temporal logic formulas. Co-existence of demonstrations and such side information offers attractive a-priori guarantees on out-of-sample generalization.