Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version)

TL;DR

This paper introduces a new framework using first-order temporal logic for specifying non-Markovian rewards in reinforcement learning, enabling complex task descriptions over unstructured data and addressing reward sparsity.

Contribution

It proposes LTLfMT, an expressive logic extension for reward specification, and develops a practical method combining reward machines and HER for complex task learning.

Findings

Enables natural specification of complex tasks in continuous control.

Shows the importance of tailored HER in solving complex goal tasks.

Addresses theoretical and computational challenges of LTLfMT.

Abstract

In this work, we propose a novel framework for the logical specification of non-Markovian rewards in Markov Decision Processes (MDPs) with large state spaces. Our approach leverages Linear Temporal Logic Modulo Theories over finite traces (LTLfMT), a more expressive extension of classical temporal logic in which predicates are first-order formulas of arbitrary first-order theories rather than simple Boolean variables. This enhanced expressiveness enables the specification of complex tasks over unstructured and heterogeneous data domains, promoting a unified and reusable framework that eliminates the need for manual predicate encoding. However, the increased expressive power of LTLfMT introduces additional theoretical and computational challenges compared to standard LTLf specifications. We address these challenges from a theoretical standpoint, identifying a fragment of LTLfMT that is tractable but sufficiently expressive for reward specification in an infinite-state-space context. From a practical perspective, we introduce a method based on reward machines and Hindsight Experience Replay (HER) to translate first-order logic specifications and address reward sparsity. We evaluate this approach to a continuous-control setting using Non-Linear Arithmetic Theory, showing that it enables natural specification of complex tasks. Experimental results show how a tailored implementation of HER is fundamental in solving tasks with complex goals.