Source-linked AI summary
hint$^2$: Hierarchical World Models for Inference-Time Temporal Logic Guidance
Moritz Zoellner, Anastasios Manganaris, Ahmed H. Qureshi, Rohan Paleja
TL;DR
Robots still struggle to follow long-horizon temporal-logic instructions while respecting runtime safety constraints. hint2 uses hierarchical world models to guide short-horizon diffusion policies, achieving complete satisfaction across tested automaton distances and real-world instructions.
Problem
Learned manipulation policies remain limited in executing long-horizon, non-Markovian instructions with runtime safety constraints, while full-trajectory temporal-logic guidance suffers from compounding prediction errors.
Method
hint2 uses high- and low-level world models to guide action chunks toward LTL automaton progress and precise local safety objectives at inference time.
Results
100% satisfaction across all automaton distances, with successful completion of all evaluated real-world inference-time instructions.
Takeaways & Limitations
The approach enables pretrained diffusion policies to satisfy significantly more complex LTL constraints than state-of-the-art techniques.
Takeaways & Limitations
The method relies on fixed atomic propositions and provides exact guidance only for constraints that are stutter-invariant relative to the MDP.
Abstract
from arXiv · showhide
A central goal of robot learning is to enable robots to execute rich instructions specified at runtime. Large-scale language-conditioned policies have made substantial progress toward this goal, yet still struggle with temporal structure and safety constraints. Linear Temporal Logic (LTL) provides a powerful language to express complex, non-Markovian instructions. However, guiding learned manipulation policies toward LTL satisfaction remains challenging because modern policies generate short-horizon action chunks and replan in closed loop, while almost all LTL specifications are evaluated over long-horizon trajectories. In this paper, we introduce hint$^2$, a method for guiding short-horizon policies toward satisfying complex LTL specifications at inference time using hierarchical world models. Our key idea is to derive two separate guidance objectives using each world model's abstraction level. A high-level model predicts future action-induced transitions in task-relevant atomic propositions to guide progress through the LTL automaton, while a low-level dynamics model predicts immediate state evolution for accurate local safety guidance. Our results show that hint$^2$ overcomes the limitations of current LTL-guided diffusion methods, outperforms existing inference-time steering methods in CALVIN, and successfully completes instructions with complex liveness and safety constraints more elegantly than language-conditioned alternatives. Finally, we demonstrate that hint$^2$ can handle complex instructions on a real UR5e manipulator.
1 Introduction
Large-scale language-conditioned robot policies still struggle with long-horizon, non-Markovian instructions and runtime safety constraints. hint2 addresses the mismatch between short-horizon diffusion policies and long-horizon LTL satisfaction through hierarchical inference-time guidance using two world models.
- Motivation: Generalist robot policies show strong language and physical-behavior generalization but struggle with long-horizon, non-Markovian instructions and runtime safety constraints.These limitations persist despite progress from large-scale imitation learning.
- Motivation: Inference-time guidance preserves the learned policy and modifies how actions are selected from its distribution.Prior work demonstrated guidance for simpler objectives such as goal images and human-supplied keypoints, whereas temporal logic poses a richer challenge.
- Method: hint2 guides short-horizon diffusion policies toward satisfying long-horizon temporal logic specifications at inference time.The method addresses the mismatch between short-horizon action generation and long-horizon specification evaluation.
- Method: A high-level world model predicts action-chunk-induced transitions in task-relevant atomic propositions to guide progress through the LTL automaton.This model operates at a higher abstraction level and supports temporal-logic progress guidance.
- Method: A low-level world model predicts immediate state consequences of actions to provide local guidance.hint2 therefore derives guidance objectives from two world models operating at different abstraction levels.
2 Related Work
Related work spans temporal-logic task specification, inference-time guidance of learned policies, and world models for long-horizon robot behavior. Existing methods combine automata, policy steering, and learned state prediction, but face challenges including long-horizon rollout errors.
- Temporal logic for robot task specification: Temporal-logic specifications express non-Markovian robot behaviors through liveness constraints requiring desired events eventually and safety constraints preventing undesired events.Classical approaches compose an abstraction of robot-environment dynamics with an automaton encoding an LTL specification, then define a controller over the resulting product system.
- Guiding learned policies at inference time: Inference-time guidance steers pretrained policies toward objectives not necessarily covered during training, complementing dominant training-time language or formal-specification conditioning.Examples include biasing diffusion denoising and selecting sampled actions that score best under a learned objective.
- World models for long-horizon robot behavior: World models predict action-induced state changes and, with differentiable robustness, guide policies toward local STL satisfaction but remain limited in long-horizon evaluation by compounding rollout errors.Recent work moves long-horizon reasoning to a higher abstraction level using hierarchical models.
3 Preliminaries and Problem Formulation
This section defines LTL and its automaton representation, then formulates inference-time guidance as minimally modifying a diffusion policy so induced trajectories satisfy the specification. Sampling reduces to estimating the probability of eventual specification satisfaction for candidate action chunks.
- Temporal Logic: LTL expresses temporal properties over atomic propositions using Boolean operators and the temporal operators next, eventually, always, and until.The method uses quantitative LTL semantics.
- Automata: The method targets recurrence-class LTL formulas translated into Deterministic Büchi Automata with states, alphabet 2^AP, transitions, an initial state, and accepting states.Atomic-proposition labels map environment states into the automaton alphabet.
- Problem Formulation: The desired policy minimizes D_KL(π̂∥π) relative to a diffusion policy while requiring induced trajectories to satisfy ϕ.Equivalently, the product-MDP automaton sequence must intersect accepting states infinitely often.
- Problem Formulation: Sampling from the guided policy reduces to estimating P(ϕ | s_t, q_t, a_t:t+H), or its score function, while sampling action chunks from π.This probability conditions on executing the candidate chunk and then continuing under π.
4 hint2
hint2 guides pretrained diffusion policies toward LTL satisfaction at inference time by modeling how short-horizon action chunks affect long-horizon specification progress. It combines high-level atomic-proposition guidance with low-level safety guidance to address both temporal progress and hard constraints.
- 4 hint2: hint2 targets the action-chunk effect on future LTL satisfaction, a probability that is otherwise infeasible to model directly because satisfaction depends on the entire induced trajectory.The method is introduced specifically for guiding pretrained diffusion policies at inference time.
- High-Level Guidance: The high-level world model predicts probabilities for the next N distinct atomic-proposition labels and uses them to compute an exact distribution over future automaton states.Repeated labels can represent long trajectory segments, enabling guidance over arbitrary LTL formulas at the proposition abstraction level.
- High-Level Guidance: For stutter-invariant formulas, the automaton-state distribution after N label segments is independent of segment durations and equals αN = MNMN−1 · · · M1 α0.Stutter-invariance makes repeated occurrences of the same reachable label equivalent to observing it once.
- High-Level Guidance: The method maximizes expected cumulative automaton potential across the high-level horizon and backpropagates it through the world model to guide short-horizon action chunks toward long-horizon satisfaction.The resulting signal can be used for any horizon N when the predicted actions induce expected automaton progress.
- Low-Level Guidance: Because proposition-level boolean guidance is less expressive and lacks an adjustable constraint threshold, hint2 adds a low-level guidance term aimed directly at safety constraints.The low-level term is motivated especially by hard safety constraint satisfaction.
5 Experimental Results
Across 2D, simulated manipulation, and real-world experiments, hint2 guides short-horizon diffusion policies toward increasingly complex LTL objectives. It maintains 100% satisfaction in the 2D domain, achieves 91% average success for CALVIN behavior selection, reaches near-perfect success on expressive specifications, and completes all evaluated real-world instructions.
- 2D LTL guidance: 100% LTL satisfaction is maintained across increasing automaton distances in the 2D Toy Squares domain.Baselines become unreliable or horizon-limited when longer LTL specifications require behavior beyond single-target training trajectories.
- CALVIN inference-time goal selection: 91% average success across eight CALVIN behaviors lets hint2 outperform DynaGuide and ITPS in single-behavior selection.The high-level world model learns which action chunks are likely to lead to each future behavior, biasing diffusion sampling toward the desired outcome.
- Expressive guidance capabilities: Symbolic proposition objectives provide a more accessible runtime interface than goal images or hand-specified 3D positions while supporting richer temporal structure.The paper evaluates hint2 beyond single-behavior selection because LTL can express complex instructions and safety constraints unavailable to image- and position-based steering.
- Expressive guidance capabilities: Near-perfect success across evaluated specifications shows hint2 can execute complex CALVIN instructions with long-horizon liveness and runtime safety constraints.The comparison includes FLOWER and variants augmented with an LLM planner or GPC-based safety guidance.
- Real-world experiments: All evaluated real-world inference-time instructions are successfully completed, while STL-GPC provides weaker guidance than hint2.The real-world experiment uses 130 demonstrations of box pouring and placement behaviors; STL-GPC may commit to a target mode before short-horizon robustness becomes informative and can underperform the base policy on safety tasks.
6 Conclusion
hint2 guides pretrained diffusion policies toward substantially more complex LTL constraints by predicting action-chunk consequences at two abstraction levels. Its current formulation relies on fixed atomic propositions and provides exact guidance only for stutter-invariant constraints relative to the MDP.
- hint2 guides pretrained diffusion policies in high-dimensional domains toward significantly more complex LTL constraints than state-of-the-art techniques support.
- Its success depends on predicting action-chunk consequences at two abstraction levels, including a higher level that captures task-relevant state information and evolves more slowly.
- Limitations and Future Work: The method currently uses a fixed set of atomic propositions for its high-level abstraction.Future work will investigate automatically learning discrete, slow-evolving world features for more general guidance.
- Limitations and Future Work: For LTL guidance, hint2 obtains an exact guidance signal only for constraints that are stutter-invariant relative to the MDP.
A Derivation of Optimal Policy Factorization
The section derives the factored LTL-guided policy by imposing a trajectory-satisfaction constraint on the expected log continuation probability and solving the resulting KL-regularized optimization. The solution is proportional to the base policy multiplied by the satisfaction probability.
- Constraint formulation: The derivation constrains the expected logarithm of continuing to satisfy ϕ given ⟨s, q, a⟩ to exceed a threshold ϵ ∈(−∞, 0].The expectation is taken over possible policies ˆπ, and the constraint applies to trajectories induced by ˆπ.
- Optimization: Taking the derivative of the Lagrangian with respect to ˆπ and setting it to zero yields the stationarity condition.The optimization uses multipliers β ≥0 and λ.
- Policy solution: Solving the stationarity condition gives log ˆπ(a | s, q) = log π(a | s, q) + β log P(ϕ | s, q, a) + (λ −1).This is Equation 7 in the derivation.
- Policy solution: Exponentiating gives ˆπ(a | s, q) = π(a | s, q)P(ϕ | s, q, a)βeλ−1.The factor eλ−1 acts as a normalization-related constant.
- Final factorization: With β = 1 and π(a | s, q) = π(a | s), the optimal factorization is ˆπ(a | s, q) ∝π(a | s)P(ϕ | s, q, a).λ determines the normalization constant.
B Proof of Proposition 1 · B.1 Justification for Maximizing Expected Automaton Potential
Under stutter-invariance and independent proposition labels, automaton-state distributions evolve exactly through stochastic transition matrices and do not depend on segment durations. The cumulative expected automaton potential extends constrained receding-horizon guidance while rewarding feasible, earlier progress toward accepting states.
- B Proof of Proposition 1: Proposition 1 assumes a stutter-invariant LTL formula, a deterministic Büchi automaton, and predicted proposition probabilities with mutually independent labels.These assumptions define the stochastic symbols and transition matrices used in the proposition.
- B Proof of Proposition 1: For any initial automaton state and segment durations T1, …, TN ≥1, the final state distribution is independent of durations and equals αN = MNMN−1 · · · M1 α0.Here, α0 is the unit vector for the initial automaton state.
- B Proof of Proposition 1: The proof establishes by induction that repeating any segment label σ for T ≥1 steps produces the same automaton state as observing σ once.The induction uses δT(q, σ) = δ(q, σ) and shows the result persists from T to T+1.
- B Proof of Proposition 1: Because each segment’s state depends only on its label, the probability of transitioning to q′ is obtained by summing label probabilities over σ satisfying q′ = δ(qk−1, σ).This relation supplies the entries of the stochastic matrix Mk.
- B Proof of Proposition 1: Mutual independence factorizes each label probability exactly from ℓk, yielding αk = Mkαk−1 and, by iteration, the stated product formula.Initializing with α0 = eqt completes the result for any initial automaton state qt.
- B.1 Justification for Maximizing Expected Automaton Potential: The guidance objective is a stochastic extension of Ding et al.’s constrained receding-horizon controller for deterministic finite systems.It maximizes expected cumulative automaton potential over the high-level prediction horizon while retaining feasibility in all cases.
- B.1 Justification for Maximizing Expected Automaton Potential: Cumulative potential encourages persistent increases in expected potential across iterations and prefers shorter paths to accepting states over terminal potential alone.Two action chunks reaching F at steps k1 < k2 contribute vT αk1:N > vT αk2:N, rewarding earlier progress.
C Toy Squares - Complex Specification · D CALVIN Implementation · D.1 Model Training
The paper evaluates hint^2 on a complex Toy Squares specification combining liveness, branching, sequencing, and safety, then details its CALVIN adaptation and hierarchical world-model training. hint^2 achieves 100% satisfaction on the Toy Squares task, while CALVIN uses short-horizon diffusion policies guided by high- and low-level state models.
- C Toy Squares - Complex Specification: The additional Toy Squares evaluation tests whether results extend beyond simple ordered reachability.The specification explicitly combines the main temporal concepts evaluated throughout the paper.
- C Toy Squares - Complex Specification: hint^2 achieves 100% satisfaction on a Toy Squares specification combining unordered liveness, branching, sequencing, and safety constraints.The task requires reaching red and blue in either order, following one of two branches, and always avoiding unsafe regions.
- D CALVIN Implementation: The CALVIN implementation adapts robomimic’s diffusion-policy implementation and follows the setup used by DynaGuide.The policy observes proprioception, wrist RGB, and third-person RGB images.
- D.1 Model Training: The CALVIN policy predicts action trajectories with prediction horizon 16 and execution horizon 8, while world models use low-dimensional robot and scene state.All models are trained solely on the CALVIN-D training dataset.
- D.1 Model Training: The high-level world model predicts the next binary label probability vector from robot and scene state, the current labels, and an 8-step action chunk.Its prediction horizon is N = 1, and labels include switch, button, drawer, and door states generated from environment thresholds.
- D.1 Model Training: The low-level dynamics model predicts normalized state deltas from the current state and a single 7D action.It uses continuous 6D rotation representations and an MLP with hidden size 512, depth 4, and dropout 0.02, trained with Adam and mean-squared error.
D.2 Experiments
The experiments evaluate individual guidance in the DynaGuide articulated-object setup and composite temporal-logic objectives against language-conditioned baselines. In both setups, hint^2 selects among 32 candidate 8-action chunks using expected cumulative automaton potential, with additional low-level safety guidance when required.
- Individual guidance: The individual guidance experiment replicates DynaGuide’s articulated-object evaluation setup, including its task set, reset configurations, initial-state sampling, and randomization procedure.The button_on and button_off tasks are both represented by the label button_pressed because they use the same underlying movement.
- Composite temporal-logic objectives: The composite-objective experiment evaluates temporal-logic objectives against language-conditioned baselines using the LTL specifications and corresponding natural-language instructions listed in Table 1.Movable blocks are removed so evaluation focuses on temporal guidance over behaviors represented in the high-level label set.
- Guidance procedure: For both setups, hint^2 samples 32 candidate 8-action chunks and executes the chunk with the highest expected cumulative automaton potential.When safety constraints apply, low-level dynamics-model gradients are integrated into denoising, followed by 10 additional gradient steps on the sampled action chunk.
E Further Implementation Details
The experiments share a common implementation built around a robomimic-adapted diffusion policy and MLP world models, with domain-specific model sizes and FoundationPose-based state tracking in the real-world setup. Cyclic tasks are evaluated for two full cycles, and hint2 achieves 100% success over five real-world runs.
- Implementation: Across domains, the base policy is a robomimic-adapted diffusion policy, while both world models are MLPs over low-dimensional state observations.Only the model sizes are adjusted to match each domain’s complexity.
- Implementation: FoundationPose tracks the Cheez-It box’s position and orientation to obtain low-dimensional state in the real-world setup.This provides the state representation used by the shared implementation structure.
- Evaluation: 100% success over five runs is achieved by hint2 on the real-world cyclic task.Because true infinite-horizon evaluation is impossible, cyclic tasks terminate after two full cycles.