PlatoLTL: Learning to Generalize Across Symbols in LTL Instructions for Multi-Task RL

TL;DR

PlatoLTL tackles the challenge of generalizing LTL-guided multi-task RL across unseen proposition vocabularies by reparameterizing atomic propositions as predicate instances with learnable parameter embeddings. A predicate-aware embedding and a sequence composition pipeline—combining graph neural networks over LTL ASTs with a recurrent aggregator—enables the policy to generalize across both LTL structure and proposition parameters. Trained with PPO on a curriculum of reach-avoid sequences, PlatoLTL demonstrates fast convergence and strong zero-shot generalization to unseen and even continuous proposition spaces in RGBZoneEnv and FalloutWorld, outperforming state-of-the-art baselines. This approach significantly broadens the practical applicability of LTL-guided RL to real-world robotics and complex, parameterized tasks by enabling scalable, generalizable grounding of high-level specifications.

Abstract

A central challenge in multi-task reinforcement learning (RL) is to train generalist policies capable of performing tasks not seen during training. To facilitate such generalization, linear temporal logic (LTL) has recently emerged as a powerful formalism for specifying structured, temporally extended tasks to RL agents. While existing approaches to LTL-guided multi-task RL demonstrate successful generalization across LTL specifications, they are unable to generalize to unseen vocabularies of propositions (or "symbols"), which describe high-level events in LTL. We present PlatoLTL, a novel approach that enables policies to zero-shot generalize not only compositionally across LTL formula structures, but also parametrically across propositions. We achieve this by treating propositions as instances of parameterized predicates rather than discrete symbols, allowing policies to learn shared structure across related propositions. We propose a novel architecture that embeds and composes predicates to represent LTL specifications, and demonstrate successful zero-shot generalization to novel propositions and tasks across challenging environments.

Figures (13)

• Figure 1: PlatoLTL overview. We first train a policy $\pi$ conditioned on arbitrary reach-avoid sequences of Boolean formulae of propositions (corresponding to the second half of the diagram only). At evaluation time, given a new LTL specification $\varphi$, we construct an LDBA $\mathcal{B}_\varphi$ representing the specification and extract a reach-avoid sequence of Boolean formulae to an accepting cycle in $\mathcal{B}_\varphi$ upon which to condition the policy. Whenever the LDBA state changes, we re-condition the policy on a reach-avoid sequence from the new state. Since the policy was trained on arbitrary reach-avoid sequences, it generalizes across LDBAs, and therefore across LTL formula structures.
• Figure 2: PlatoLTL policy architecture. The sequence module processes the given reach-avoid sequence of Boolean formulae into a learned sequence embedding. It first composes predicate instance embeddings using the predicate type and parameters for each proposition. It then builds up compositionally from the predicate instance embeddings, using a GNN over the Boolean formula graphs followed by an RNN over the sequence. The observation module processes the observation from the environment into a learned state embedding. The outputs are then concatenated and passed into the actor-critic module to obtain the action.
• Figure 3: Success rate (as a proportion of total roll-outs) and average episode length (in steps) during training for reach-avoid LTL specifications composed from the training set of atomic propositions. Results are averaged over $5$ seeds, $50$ specifications per seed and 16 episodes per specification per seed, with $95\%$ confidence intervals marked by the shaded area.
• Figure 4: LDBA for the formula $(\mathop{\mathsf{F}} \mathop{\mathsf{G}} \mathsf{a}) \lor \mathop{\mathsf{F}} \mathsf{b}$.
• Figure 5: Visualizations of example environment reset configurations. In both cases, the distribution of environment resets covers an infinite number of possible atomic propositions, as described in Appendix \ref{['app:experimental_details:train_eval_props']}.

Theorems & Definitions (2)

• Example 5.2
• Definition 3.1: Product MDP; jackermeier_deepltl_2025