Skip to content

Zero-Shot Instruction Following in RL via Structured LTL Representations

🕒 Published (v1): 2025-12-02 10:44 UTC · Source: Arxiv · Venue: ICML 2025 · link

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

This paper introduces LTL-GNN, a method for training RL agents to zero-shot follow arbitrary Linear Temporal Logic (LTL) instructions by representing task structure as sequences of Boolean formulae extracted from Büchi automata, encoded via graph neural networks. The key insight is that Boolean formulae over automaton transitions—rather than raw proposition assignments—enable compositional generalization when multiple atomic propositions are simultaneously true. The approach outperforms state-of-the-art baselines on a complex chess-based environment.

Problem

Existing multi-task LTL-conditioned RL approaches condition policies on sets of atomic proposition assignments drawn from automaton transitions, treating each possible assignment as a separate, isolated goal. This fails in environments where many propositions can be simultaneously true and interact in complex ways (e.g., a square attacked by multiple chess pieces), because the policy cannot generalize across combinatorially many assignment combinations.

Method

Starting from a given LTL formula φ, the method constructs a limit-deterministic Büchi automaton (LDBA) Bφ and extracts accepting runs via DFS over the automaton. For each transition qi→qi+1 in an accepting run, two compact Boolean formulae are constructed: β⁺ᵢ (assignments that trigger the desired transition) and β⁻ᵢ (assignments causing undesired transitions). These formulae are minimized via approximate candidate template matching (conjunctions, disjunctions, negated disjunctions) rather than naive DNF expansion. Each formula is converted to an abstract syntax tree (AST) and encoded by a graph convolutional network (GCN, 3 layers, hidden dim 32). The GCN root embeddings for the β⁺/β⁻ pairs across a run are concatenated and fed through a GRU to produce a run embedding, which is combined with the MDP state encoding in a PPO-trained policy. At test time, the value function selects among multiple candidate accepting runs for a novel instruction.

Key Contributions

  • Novel task representation: sequences of Boolean formulae over LDBA transitions, replacing raw assignment sets used by prior work
  • GNN-based encoding of Boolean formula ASTs that supports compositional generalization across proposition combinations
  • New ChessWorld benchmark environment with 5 piece types and complex overlapping proposition assignments, enabling rigorous multi-proposition evaluation
  • Empirical demonstration of zero-shot generalization to unseen LTL instructions, with state-of-the-art results on both finite- and infinite-horizon tasks

Results

  • Finite-horizon tasks (7 task sets): LTL-GNN achieves SR 74.3–99.3% vs. DeepLTL 67.1–99.1% and Transformer 41.7–80.8%; LTL-GNN most clearly wins on ϕ₃ (82.6% vs. 68.8% vs. 51.7%) and ϕ₅ (74.3% vs. 67.1% vs. 41.7%)
  • Infinite-horizon tasks: LTL-GNN ϕ∞₁: 86.0±28.0% and ϕ∞₂: 76.7±36.7% vs. DeepLTL 40.0±49.0% and 35.7±44.0% (near-random); Transformer similarly fails at 43.1% and 33.6%
  • Scaling difficulty (reach-avoid ¬a U b, 1–5 pieces to avoid): LTL-GNN degrades more gracefully than both baselines across all difficulty levels
  • All results averaged over 5 seeds; 15M training steps

Limitations

  • Evaluated only in ChessWorld (8×8 grid, discrete low-dimensional state); no validation in high-dimensional or continuous observation spaces
  • Labeling function L: S → 2^AP is assumed known; not applicable to vision-based environments without a separate event detector
  • Boolean formula minimization is NP-hard in general; the approximate candidate template approach may fail for large proposition sets, falling back to exponential DNF
  • High variance on infinite-horizon tasks (±28–37% std) suggests instability, likely due to sparse accepting-state rewards
  • Only 5 atomic propositions in ChessWorld; scalability to larger AP sets untested

Relevance to Agentic AI / LLM Agents

This work advances formal instruction-following for RL agents—directly relevant to grounding agentic behavior in precise, compositional task specifications rather than ambiguous natural language. The LTL+automata framework provides well-defined semantics and compositionality that are valuable for safety-critical agent deployments where task ambiguity is unacceptable. The zero-shot generalization to novel instructions mirrors a core desideratum of general-purpose LLM agents: a single policy that executes diverse goals without per-task fine-tuning. Integrating such formal specification approaches with LLM-based agents (e.g., using an LLM to translate natural language goals into LTL, then using LTL-GNN to execute) is a natural near-term research direction.