Safe and Performant Policies via Specification Guided Reinforcement Learning

Abstract: Linear temporal logic (LTL) offers a principled way of specifying tasks for policy optimization that may otherwise be difficult to describe with scalar reward functions. However, the standard Reinforcement Learning (RL) frameworks can be too myopic to find maximally satisfying policies. In this talk we will discuss eventual discounting, a value-function based proxy under which one can find policies that satisfy a specification with the highest achievable probability. To improve the efficiency of learning from specifications we combine eventual discounting with LTL-guided Counterfactual Experience Replay, a method for generating off-policy data from on-policy rollouts via counterfactual reasoning. We will then discuss mechanisms for exploiting the compositionality of a LTL specifications to (i) provide formal guarantees on the behavior of learnt policies for reach-avoid tasks, and (ii) automatically refine specifications from experience.

Bio: Abhinav Verma is an Assistant Professor in the Department of Computer Science and Engineering at The Pennsylvania State University. Previously, he was a postdoc at the Institute of Science and Technology (IST) Austria in the Henzinger Group. Before joining IST, he completed his PhD from the University of Texas at Austin advised by Prof. Swarat Chaudhuri. Verma’s research lies at the intersection of machine learning and formal methods, with a focus on building intelligent systems that are reliable, transparent, and secure. This work builds connections between the symbolic reasoning and inductive learning paradigms of artificial intelligence