Reinforcement learning provides a powerful framework for learning decision-making strategies from interaction, but specifying what an agent should learn is often as challenging as designing the learning algorithm itself. A scalar reward can be an inadequate description of objectives that involve sequences of events, long-term requirements, safety constraints, or other temporal properties.

In this talk, I will discuss how ideas from formal methods can help address this problem. Temporal logic, automata, and related specification formalisms provide precise ways to describe desired behavior, while reinforcement-learning algorithms provide mechanisms for learning how to achieve such objectives from experience. I will describe ways in which these viewpoints can be connected so that richer specifications can be incorporated into learning algorithms without losing the ability to reason about their behavior.

I will also discuss some of our recent work on reinforcement learning with formally specified objectives and on obtaining statistical and formal guarantees for learned policies. More broadly, the talk will illustrate how classical ideas from algorithms, automata, and verification can contribute to the design of learning systems that are easier to specify, analyze, and trust.

Short bio: Ashutosh Trivedi is an Associate Professor of Computer Science at the University of Colorado Boulder. His research lies at the intersection of formal methods, reinforcement learning, and trustworthy artificial intelligence, with applications to cyber-physical and safety-critical systems. His work develops mathematical foundations and algorithms for specifying, learning, and verifying the behavior of learning-enabled systems.