Skip to content

Expressive Temporal Specifications for Reward Monitoring

🕒 Published (v1): 2025-11-16 22:28 UTC · Source: Arxiv · Venue: AAAI · link

Ask a follow-up

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

💬 Ask ChatGPT✦ Ask Claude

TL;DR

This paper introduces Quantitative Reward Monitors (QRMs) synthesized from Quantitative Linear Temporal Logic on finite traces (LTLf[F]), replacing binary Boolean monitors with real-valued [0,1] satisfaction degrees to produce dense reward streams. The approach directly mitigates sparse rewards in long-horizon RL by providing per-step quantitative feedback proportional to task progress. Across 13 Gymnasium environments, QRMs consistently match or outperform Boolean monitors and occasionally surpass handcrafted reward functions.

Problem

Existing temporal logic-based reward specifications for RL use Boolean (qualitative) semantics, emitting reward only upon full formula satisfaction. This produces sparse rewards that hinder credit assignment, inflate sample complexity, and degrade performance on long-horizon tasks. The gap between formal task specification and dense training signal is unaddressed in the literature.

Method

The authors define Quantitative Reward Monitors (QRMs) as finite state machines with typed registers. Starting from an LTLf[F] formula φ, the SYNTH/CONSTRUCT algorithm inductively builds sub-monitors for each syntactic subformula (atomic, negation, conjunction, Next, Until, Release), combining them via Cartesian product states. Registers track running min/max values of subformulas to correctly implement Until/Release semantics. At each time step, the reward register outputs the real-valued degree of formula satisfaction [φ, i] ∈ [0, 1] (Theorem 3, correctness). Construction cost is linear in formula size (Theorem 1). The QRM is composed with the environment MDP as a synchronous product M ⊗ A, extending the state space to include monitor state; a Markovian policy in M ⊗ A suffices to capture non-Markovian goals (Theorem 4). Safety subformulas (safe-LTLf, Until-free NNF) veto all rewards globally upon violation, clamping output to ζ ≤ 0 for all subsequent steps.

Key Contributions

  • Formal definition and synthesis algorithm for QRMs from LTLf[F] specifications with linear state/transition overhead relative to formula size.
  • Correctness proof that the monitor's reward register equals the LTLf[F] formula's quantitative evaluation at every trace index.
  • Safety compositionality: safe-LTLf subformulas globally block reward upon violation, independent of other monitors.
  • Algorithm-agnostic framework: compatible with tabular Q-learning and PPO; requires only a state labelling function L: S → [0,1].
  • Empirical demonstration across 13 environments spanning Classic control, Toy gridworlds, Box2D, and DeepMind Safety Gridworlds.

Results

  • Acrobot: QRM 94.77% ± 0.09% task completion vs. Boolean 4.84% ± 0.40% (Boolean converges suboptimally).
  • Pendulum: QRM 72.11% ± 0.28% vs. Boolean 45.03% ± 0.18%.
  • Bipedal Walker: QRM 14.43% ± 0.41% vs. Boolean 7.43% ± 0.15%.
  • Lunar Lander: QRM 45.61% ± 0.16% vs. Boolean 43.44% ± 0.17%.
  • Cliff Walking: QRM 84.95% ± 0.05% vs. Boolean 84.38% ± 0.05% (marginal; gridworld).
  • Taxi: Boolean converges suboptimally (1301 episodes); QRM converges in 1221 episodes.
  • QRMs never underperform Boolean monitors on task completion; improvement magnitude is domain-dependent.
  • Convergence speed (time/episodes): QRMs faster in Classic and several Safety Gridworld environments.

Limitations

  • Quantitative labelling functions must be hand-specified per environment; no automated synthesis of L from observations.
  • Performance gain is bounded by the quality of the user-defined quantitative properties — if good distance metrics cannot be expressed from agent observations, QRM degrades to Boolean-level performance.
  • In obstacle-rich discrete gridworlds, Manhattan-distance-based atoms mislead the agent around walls, reducing the advantage of quantitative semantics.
  • Evaluation covers episodic, finite-horizon settings only; extension to infinite-horizon or stochastic trace semantics is left as future work.
  • No multi-agent experiments; ATLf[F] extension is noted but not evaluated.

Relevance to Agentic AI / LLM Agents

Reward specification and credit assignment are foundational to training RL-based agents, including those used in agentic LLM pipelines that employ RLHF, RLAIF, or tool-use reward shaping. QRMs provide a formal, interpretable, and composable alternative to handcrafted scalar reward functions, enabling complex multi-step task goals (e.g., "complete subtask A before B, always respecting safety constraint C") to be specified in temporal logic and automatically compiled into dense training signals. The non-Markovian goal handling — where extended monitor state tracks task history — directly addresses long-horizon planning challenges central to agentic systems. The safety-veto compositionality aligns with constrained optimization concerns in AI alignment, making this work relevant to researchers designing reward structures for autonomous agents operating under safety constraints.