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

AI summary

Overview

• Research area: Reinforcement learning with formal (temporal-logic) reward specification, satisfiability modulo theories (SMT), and automata-based reward machines.
• Technical level: Advanced. The paper assumes familiarity with MDPs, Linear Temporal Logic over finite traces (LTLf), first-order theories, determinization into DFAs, and deep-RL techniques such as Hindsight Experience Replay (HER).
• Scope: One-sentence scope: the paper proposes LTLfMT (Linear Temporal Logic Modulo Theories over finite traces) as a reward-specification language for RL, isolates a tractable fragment of it, and shows that combining reward machines with a tailored HER helps solve sparse-reward continuous-control tasks.

What This Paper Is About

Reward engineering in RL is difficult, and the commonly used logic-based reward languages (LTLf, reward machines) are limited to Boolean propositions, so continuous or heterogeneous state variables must be hand-encoded by a human-written labeling function. This paper replaces those Boolean propositions with first-order formulas evaluated by an off-the-shelf SMT solver, so a task can be written as a single temporal formula over real arithmetic (or other theories) without manual encoders. The paper then tackles the reward-sparsity that such logic specifications produce, using reward machines together with HER in a continuous-control setting.

Key Contributions

1. A theoretical reward-specification framework based on LTLfMT. The paper extends classical LTLf by replacing atomic propositions with first-order formulas over arbitrary first-order theories, allowing heterogeneous and unstructured data (e.g., real-valued positions, object IDs, weights) to be expressed directly in the specification.
2. Identification of a tractable, sufficiently expressive fragment. The authors remove the (weak) lookahead operators on Σ-terms from the LTLfMT grammar, arguing that temporal constraints on data collection are neither natural nor beneficial for reward specification. In this fragment the only remaining source of undecidability is the underlying theory itself (and the use of quantifiers), so any decision procedure for that theory can be reused.
3. A practical pipeline from formula to product MDP. The fragment is propositionalized syntactically into an LTLf formula and translated into a Deterministic Finite Automaton (DFA) using the translation technique of Zhu et al. (2019) and the LTLf2DFA library, yielding a product MDP over state space S × Q that standard RL methods can handle. The SMT solver acts as an "extremely general labeling function."
4. A non-trivial combination of CRM and HER. The paper instantiates the framework with Non-Linear Real Arithmetic (NRA) for continuous control and adapts Counterfactual Experiences for Reward Machines (CRM) and Hindsight Experience Replay (HER) to the product MDP, automating HER's goal specification by defining goals over accepting-state predecessors in the automaton.

Main Findings

• Tractability of the fragment: For decidable underlying first-order theories, LTLfMT is semi-decidable. By removing the lookahead operators, the authors obtain a fragment whose undecidability stems only from the theory and quantifiers; if the theory admits quantifier elimination (as real arithmetic does, via Tarski and Collins' procedures), the quantifier-free part can be handed to a standard SMT solver.
• Boolean-abstraction lineage: Geatti et al. (2022) gave a non-constructive proof that a Boolean abstraction of any lookahead-free LTLfMT language is also definable in LTLf. This paper takes a practical viewpoint, providing an explicit syntactic transformation of formulas and traces to make automaton construction usable.
• No hand-written labeling function needed: In contrast to reward machines (Icarte et al., 2018) and labeling-function approaches, the only user input required is the specification formula plus an optional assignment of first-order constants to numerical values, which parametrizes the task for multi-goal RL.
• Automatic HER goal definition: The paper defines the "true" goal of the product MDP as a state ⟨s, q⟩ where q is the predecessor of an accepting state q_f ∈ F and s triggers the transition to q_f, giving goal space G = S′, f_g(s) = I[m(s) = g], and m(s) = s.
• Empirical headline (as reported): Results on continuous-control tasks with complex goals suggest an improvement over using only CRM (Section 6). Figure 1 reports the success rate of each baseline for the parking environment across 4 different tasks, with a 95% bootstrap confidence interval over 20 independent experiments. The specific numerical success rates are not included in the available text.

Methodology in Plain English

The authors start from the observation that existing logic-based reward languages speak only in true/false facts, so any continuous quantity—distance to a target, a weight, an object ID—must be converted to a Boolean by a hand-written encoder. They instead let each predicate be a first-order formula over a chosen theory, such as real arithmetic. To keep the approach usable, they strip out one feature (lookahead on data variables) that creates decidability problems without adding anything useful for reward design, and they keep the familiar temporal operators (next, weak next, until, eventually). A task formula is then mechanically rewritten into a plain LTLf formula by replacing each first-order predicate with a fresh propositional letter. During training, an SMT solver decides at each timestep which of those letters is true for the current state; this replaces the labeled-environment assumption. The resulting propositional formula is compiled into a DFA, which is combined with the environment to form a product MDP whose rewards are Markovian again. Because logic rewards are rare, the authors generate extra training data in two ways: counterfactual reasoning over the DFA (replacing the DFA state with every other state q ∈ Q and recomputing the reward, producing |Q| artificial transitions per experience) and HER (relabelling trajectories with goals achieved later), with goals derived automatically from the DFA's accepting states rather than from a human. They demonstrate the pipeline on continuous control: an autonomous car in 2-dimensional space that must reach point A, then point B, without passing through an unsafe region, specified with NRA and propositionalized using an SMT solver suited for Linear Real Arithmetic (LRA) and NRA.

Why This Matters

• Impact on research: The paper pushes logic-based reward specification beyond Boolean propositions and situates itself in a lineage of work on reward machines, "restraining bolts," and labeling functions. It offers a concrete, implementable bridge between SMT technology and deep RL, and revives a previously suggested but unexplored synergy between reward machines and HER (noted by Icarte et al., 2022).
• Real-world applications (as motivated in the paper):
  • Warehouse robots delivering boxes: reach an object, match its ID, and satisfy a weight constraint.
  • Autonomous vehicles: reaching a sequence of waypoints while avoiding an unsafe zone (the parking-area example).
  • HVAC control: driving a temperature to a target value or range.
  • Cruise control: controlling a variable or vector of variables to a target.
  • Business process management, named in the paper as a domain where richer specification languages matter.
• Industry relevance: Because the user supplies only a formula string and a configuration file of constants, new tasks in the same environment can be added quickly, and changing the domain (for example, from NRA to linear arithmetic) may require only swapping the theory and its solver. This reduces the engineering effort and error-proneness associated with black-box labeling functions, and improves reusability and interpretability of specifications.

Future Directions

• Theory selection and combination: How to systematically choose and combine theories (arithmetic, uninterpreted functions and relations for relational databases, complex datatypes such as lists and arrays, custom domain predicates) when some theories lack available solvers, and how that affects decidability and practicality.
• Quantifier handling: When quantifiers push a theory into undecidability, the authors suggest further restricting the fragment by removing them, yielding a fragment similar to "data-LTLf" by Gianola et al. (2024); the trade-off between expressiveness and decidability remains open.
• Runtime efficiency: Propositionalization calls an SMT solver at every timestep, so the cost of solver calls during training is a natural scalability question, especially as state spaces and formulas grow.
• Reward-shaping alternatives: The paper frames CRM, hierarchical reward machines (HRM), and Automated Reward Shaping (ARS) as existing ad-hoc remedies for sparsity; whether the proposed LTLfMT-plus-HER combination can be improved by or combined with those alternatives is left open.

Target Audience

Researchers and graduate students working at the intersection of reinforcement learning, formal methods, and automated reasoning—particularly those interested in temporal-logic reward specification, reward machines, and non-Markovian reward decision processes. It will also be useful to practitioners in robotics and industrial control who need expressive, reusable task specifications over continuous and heterogeneous sensor data without writing custom feature encoders. Readers without background in LTLf, automata, or SMT will find Section 3 and Section 4 demanding.

Authors’ 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.