Automating the Refinement of Reinforcement Learning Specifications
Authors: Tanmay Ambadkar
Đorđe Žikelić
Abhinav Verma
Venue: ICLR 2026 Poster (2026)
Keywords: Reinforcement Learning Specifications
Automatic Specification Refinement
SpectRL
Primary area: reinforcement learning
TL;DR: A framework that refines logical specifications without human intervention

Abstract: Logical specifications have been shown to help reinforcement learning algorithms in achieving complex tasks. However, when a task is under-specified, agents might fail to learn useful policies. In this work, we explore the possibility of improving coarse-grained logical specifications via an exploration-guided strategy. We propose **AutoSpec**, a framework that searches for a logical specification refinement whose satisfaction implies satisfaction of the original specification, but which provides additional guidance therefore making it easier for reinforcement learning algorithms to learn useful policies. **AutoSpec** is applicable to reinforcement learning tasks specified via the SpectRL specification logic. We exploit the compositional nature of specifications written in SpectRL, and design four refinement procedures that modify the abstract graph of the specification by either refining its existing edge specifications or by introducing new edge specifications. We prove that all four procedures maintain specification soundness, i.e. any trajectory satisfying the refined specification also satisfies the original. We then show how **AutoSpec** can be integrated with existing reinforcement learning algorithms for learning policies from logical specifications. Our experiments demonstrate that **AutoSpec** yields promising improvements in terms of the complexity of control tasks that can be solved, when refined logical specifications produced by **AutoSpec** are utilized.

AUTOMATING THE REFINEMENT OF REINFORCEMENT LEARNING SPECIFICATIONS
Tammay Ambadkar* The Pennsylvania State University tsa5252@psu.
Dorde Žikeličt Singapore Management University dz frke 1 icc edu.sg
Abhinav Verma
The Pennsylvania State University ve verma@psu.ed edu
ABSTRACT
Logical specifications have been shown to help reinforcement learning algorithms in achieving complex tasks. However, when task under-specified, agents might fail to learn useful policies. In this work, we explore the possibility of improving coarse- grained logical specifications via an exploration- guidedd strategy. We propose AUTOSPEC, a framework that searches for a logical specification refinement whose satisfaction implies satisfaction the original specification, but which provides additional guidance therefore making it easier for reinforcement learning algorithms to learn useful policies. AUTOSPEC applicable to reinforcement learning tasks specified via the SpectRL. specification logic. We exploit the compositional nature of specifications written in SpectRL, and design four refinement procedures that modify the abstract graph of the specification by either refining its existing edge specifications or by introducing new edge specifications. We prove that all four procedures maintain specification soundness, i.e. any trajectory satisfying the refined specification also satisfies the original. We then show how AUTOSPEC can integrated with existing reinforcement learning algorithms for learning policies from logical specifications. Our experiments demonstrate that AUTOSPEC yields promising improvements in terms of the complexity of control tasks that can be solved, when refined logical specifications produced by AUTOSPEC are utilized.
INTRODUCTION
Reinforcement Learning (RL) algorithms have made tremendous strides in recent years Sutton & Barto (2018): Silver et al. (201)); Mnih al. (2013): Levine et al.) (2016). However, most algorithms assume access to a scalar reward function that must be carefully engineered to make environments amenable to RI.-a practice known as reward engineering Ibrahim al. (0224). This creates challenges in applying RL. to new environments where useful reward functions are hard to construct.
Furthermore, scalar Markovian rewards cannot provide sufficient feedback for certain tasks Abel et
(2021): Bowling et al. (2023), leading to growing interest in non-Markovian reward functions Li et al.
(2017a) Jothimurugan et al. (2021); Alur et al. (2023).
To make non-Markovian rewards tractable, it is standard to represent them via logical specifica- tion formulas that capture the intended task. These approaches, known as specification- guided reinforcement learning Aksaray al. (016); Li et al. (2017b); Icarte et al. (2018); Dothimurugan et al. 2019 2021). ) derive reward functions from logical specifications. However, this creates two challenges: (i) providing specifications granular enough to guide RL algorithms, and (ii) defining accurate labeling functions mapping environment states to specification predicates. Users often create
coarse specifications or labeling functions that, while logically correct, provide insufficient guidance for learning.
DDepartment of EECS. The Pennsylvania State University
School of Computing and Information Systems, Singapore Management University 1 Department of BECS, The Pennsylvania State University

---

ND
STANT
Figure I:
Example of refinement by AUTOSPEC a 9-rooms environment. The original MID-node region includes trap state from which recovery is impossible. The refined specification excludes this trap, enabling the agent to learn a policy with higher satisfaction probability.
We present AUTOSPEC, framework for automatically refining coarse specifications without user intervention. We say that logical specification is coarse (or under-specified) if its predicate labelings or logical structure are too coarse to allow specification-guii specifications into reward functions that allow for effective learning of RL policies. AUTOSPEC starts with an initial logical specification, translates it to a reward function, and attempts to learn a policy. If the learned policy's performance unsatisfactory, AUTOSPEC identifies which specification components cause learning failures and automatically refines both the specification formula and labeling function. The refined specification's satisfaction implies the original's satisfaction while providing additional structure for learning. This process repeats until a satisfactory policy is learned.
RL algorithms to translate logical
AUTOSPEC works with SpectRL specifications: boolean and sequential combinations reach-avoid tasks Jothimurugan et al. (219).. Any SpectRL specification decomposes into an abstract graph where edges specify reach-avoid tasks Jothimurugan et al. (202T). AUTOŠPEC identifies problematic edges and applies targeted refinements: either modifying the labeling function for regions (Figure 1 or restructuring the graph to add alternative paths. These problematic edges are identified by employing an exploration-guiann guided stralegy that utilizes empirical trajectory data identify edges in the abstract graph whose reach-avoid tasks (i.e. initial, target or unsafe regions) make it hard to learn a good RL policy. For instance, in Figure [ the initial MID region of the MID-GOAL edge in the abstract graph under-specified, as it overlaps with a trap state. The trap state is not immediately obvious as there path from MTD to GOAL. By analyzing explored traces, AUTOSPEC identifies problematic start states in MTD and refines the region to exclude the trap (as shown in Figure I. thereby refining the logical reach-avoid specification associated the MID-GOAL edge.
We prove that all refinements maintain soundness, where satisfaction of the refined specification im- plies satisfaction of the original. AUTOSPEC integrates with existing SpectRL-compatio algorithms as demonstrated with DIRL DIRL,Jothimuruge el al. (202T) and LSTS Shukla et al. (2024).
Our contributions:
1. A framework for automated refinement of logical RL specifications with four refinement procedures, all with formal soundness guarantees (Section
2. Integration with existing specification-guiiee RL algorithms, enabling them to solve tasks with coarse specifications (Section 3
3. Empirical demonstration that AUTOSPEC enables learning from specifications that existing methods cannot handle (Section
Related work. Recent years have seen substantial progress in solving RL tasks specified via logical
specifications AAssrayy et al. (2016); Li et al. (2017b); Iearte et al. 20: Camacho et al. (2019);
Giacomo et (2019); Hasanbeig et al. (2022; 2019] Hahn et al. (2019); Jothimurugan al. (2019)
2021); Xu & Topcu 2019). Many works consider different fragments of Linear Temporal Logic (LTL) or their variants for specifying RL tasks. Icarte et al. (0188): Camacho et al. (2019) consider tasks that can be specified using deterministic finite automata (DFA) and solve them by reward machines, which decompose these tasks and translate them into a reward function. The reward function then be used to train existing RL algorithms. Li et al. (2017b) considers variant of LTL called TLTL for specifying tasks and propose a method for translating these specifications into continuous reward functions. Hasanbeig et al. 2002 2019) Hahn et al. (2019) study the translation
2

---

of tasks specified in LTL into reward functions. Alur al. (2022) examines the theoretical questions related to the translation of logical specifications into reward functions.
Jothimurugan al. 2019) defines the specification language SpectRL, finitary fragment of LTL and provides justification for using this language to define specifications for RL tasks. A compositional method that decomposes SpectRL specifications into an abstract graph and constructs reward function for each abstract graph edge was proposed in JnJoiimuuuaann et al. (2021). The approach by Toro Icarte et al. (2019) focuses on discovering optimal reward structures through environmental exploration and reward analysis. Compositional methods are further explored by Neary et al. (2022). who propose removing unfulfillable subtasks, and Neary et al. (2023), who introduce verification techniques to certify learned policies. ZZikelic et al. (2023b) propose CLAPS, a compositional method for learning neural network policies with formal guarantees on the satisfaction of SpectRI. specifications, thus advancing the applicability to safety-critical RI applications by utilizing prior methods for learning reach-avoid policies with formal guarantees Lechner (2023a) Chatterjee et al. (2023).
Lecnnee et al. (2022) Zikelic et al.)
Recent advancements also include LTL2Action Vaezipoor et al. [202] which translates LTL specifi- cations into sequences of tasks for RL agents. Other recent approaches, such as QQuu et al. (2023) and DeepLTL Saa.TLLDackemmiec. Jackermeier & Abate (2025), leverage coul-condi RL and automata-bass
architec- tures to solve complex LTL and w-regular tasks zero-shot in multi-task settings. Trainify Jin et al. (2022) employs counterxxample-guddee abstraction and refinement (CEGAR) to iteratively improve policies by addressing failure cases identified through counterexamples. However, these works primarily focus on learning policies for fixed, well-defined specifications. In contrast, AUTOSPEC studies the problem of automated logical specification refinement towards improving reward functions obtained by translation from coarse logical RL specifications. Thus, our work is complementary to the works on RL from logical specifications and can be integrated into off-the- shelf specification-gus -iiiidd RL algorithms to improve the performance of learned agents.
2 PRELIMINARIES
MDPs. A Markov Decision Process (MDP) is a tuple M = R, where S C R" is the state space, A C R" is the action space, P S x A x S - [0. 1] is the probabilistic transition function, R is the (possibly non-Markovian) reward function. and y is the discount factor. Let 5 - [0, 1] be the initial state distribution. A trajectory ( in M is sequence of states and actions Ç = Sg, ag 81, 01,... where 8; E 5 and a; E A. We use 2 to denote the set of all trajectories in M and 2 to denote the set of all finite trajectories in M, which are finite prefixes of trajectories ending in states. A (pure) policy π y + A assigns an action to each finite trajectory, and non-Markovian reward R: 2 IR assigns reward to finite trajectory. The MDP M under any policy gives rise to probability space over the set of all trajectories in the MDP Puterman (994).. We use IP" and E" to denote the probability measure and the expectation operator this probability space, respectively.
Logical specifications for Reinforcement Learning. In this work, we are solving RL tasks defined by logical specifications. Formally, a logical specification (or, simply, a specification) is boolean function @ Z - (true, false) } which specifies whether a trajectory in the MDP satisfies the specification. We write + & whenever trajectory ( satisfies the specification c. The objective of a specification--uicnn the given specification Φ, i.e. n" E argmax, F [< }= Φ). Specification-uuided RL algorithms use the specification to create a dense reward that guides the policy search, and therefore outperform algorithms that cannot leverage the specification for learning and instead require manual reward engineering Jothimurugan et al. 2022 Shukla et al. (2024).
RL task is to find a policy n² that maximizes the probability of satisfying
SpectRL specification logic. We consider RL tasks specified in the SpectRL. specification logic. SpectRL Jothimurgan et al. (2019) is fragment of Linear Temporal Logic (LTLL) which consists of all boolean and sequential combinations of reach-avoid tasks. Formally, a specification in SpectRL is defined in terms of predicates and specification formulas. An atomic predicate is function a: S + {true, false} which defines a set of states that satisfy the atomic predicate. A predicate is a boolean combination of atomic predicates, i.c. b a by A b2 b1 V b2, where is an atomic predicate and by and b2 are predicates. Specification formulas in SpectRL are defined by the grammar
s achieve Φi ensuring b Φ2; ti or Φ2
(1)
3

---

where b is a predicate and Φ1 and Φ2 are specification formulas. Intuitively, "achieve 6" requires the agent to reach a state in which the predicate is satisfied. The clause "Ø1 ensuring b" requires the agent to satisfy the specification ó while only visiting states in which the predicate 6 is satisfied. The clause "<1; dh2" " requires the agent to first satisfy specification Φ and then satisfy specification dz-
The clause "ch1 02 " requires satisfaction of at least one of Φ1 Φ2. See Lothimurugan al. (2019) for the formal definition of the semantics of each clause.
Abstract graphs for SpectRL specifications. It was shown in Jothimurugan al. (2021) that each specification written in the SpectRL specification logic can be translated into an equivalent abstract graph. An abstract graph is directed acyclic graph (DAG) whose vertices represent sets of MDP states and whose edges are annotated with sets of safe MDP states. Hence, each abstract graph edge defines a reach-avoid specification, where the task is to reach the set of states defined by the target vertex of the edge starting from the set of states defined by the source vertex of the edge, while staying within the set of safe states defined by the edge.
Definition (Abstract graph). An abstract graph G BV, is DAG, where is a finite set of vertices, E is a finite set of edges, : VUVE E - ((S) is a labeling function that maps each vertex and each edge to a subset of the MDP states S, s E V the source vertex and t V is the targer vertex. Furthermore, we require that ((s) support(n) is the support of the initial state distribution n of the MDP
Given a trajectory ( in the MDP and an abstract graph G EV, (). we say that Ç satisfies abstract reachability for G' (written Ç - G) if it gives rise to path in G that traverses G from to t and satisfies the reach-avoid specifications of every traversed edge. It was shown in Jothimurugan et al. 202T) that, given any SpectRL. specification ø, one can construct an abstract graph G such that F Φ and only if < + G holds for each trajectory Ç in the MDP. Hence, solving an RL. task for SpectRL specification reduces solving abstract reachability task in the abstract graph G.
Problem statement. Given an MDP M and a SpectRL specification é, our goal is to learn a policy n such that the probability pa [S - 6) of a trajectory satisfying the specification is maximized.
Specification refinement. In order to solve this problem, we will utilize a common approach in specification -uideed RL, to first translate the logical specification o to (non-sparse) reward function and then learn policy by using existing RL algorithms with this reward function. However, if the probability of the specification being satisfied under the learned policy is unsatisfactory (i.e. below some desired probability threshold p E [0. 1). we will then refine the logical specification 6 into new SpectRL specification o,. We will then repeat the above process until the probability of the specification being satisfied under the learned policy becomes satisfactory.
Definition 2 (Specification refinement). Given two logical specifications & and or. we say that s, refines Φ, if any MDP trajectory that satisfies the refined specification o, also satisfies the specification Φb That is, for an MDP trajectory Ç we have (5 } Φr) = ((
3 AUTOMATED REFINEMENT OF RL SPECIFICATIONS
We now present AUTOSPEC, a framework for automated refinement of logical specifications in RL tasks. The key insight is that specification failures often stem from identifiable issues that can be systematically addressed: overly broad target regions, insufficient safety constraints, missing waypoints, or lack of alternative paths. When a specification-guiin guided RL algorithm A fails to learn a satisfactory policy for specification é. AUTOSPEC identifies which components caused the failure and applies targeted refinements to improve learnability while maintaining soundness.
AUTOSPEC operates as a wrapper around any SpectRI algorithm. It monitors the learning process, and when a policy и fails to satisfy the specification with probability least p E [o. 1 (a user-provided threshold), computes refined specification o, such that: (1) satisfaction of o implics satisfaction of ó (soundness), and (2) Φr provides additional structure that makes it easier to learn. This refined specification is returned to algorithm A to continue learning. Through this iterative refinement process, AUTOSPEC enables solving RL tasks with coarse specifications that would otherwise be unlearnable.
Overview of AUTOSPEC, Algorithm|] shows the complete AUTOSPEC framework. The algorithm takes as input MDP M, SpectRI. specificatinnnn é, satisfaction threshold p, and any specification-
4

---

guided RL algorithm A. It first translates & into abstract graph G and uses A to learn policies for the graph edges. For each edge e where learned a policy but that policy fails to achieve satisfaction probability p, AUTOSPEC applies four refinement procedures in sequence: SeqRefine, AddRefine, PastRefine, and OrRefine. This ordering reflects increasing levels of structural modification; from local predicate adjustments graph topology changes. The first refinement that successfully improves performance above threshold is applied, the graph is updated, and policies are relearned before proceeding to the next edge.
Algorithm 1 AUTOSPEC
Require: MDP M, specification o, threshold p E [0, 1]. spec-guided RI. algorithm A G - abstract graph corresponding to Φ II A(G) [set of policies for edges in G learned by algorithm A] for e u + u' an edge in G' do
Te E II < policy learned for edge (Null if A does not learn policy for edge e)
if .T is not Null and ( < then
< < sampled trajectories of the system
if L...ARNPOLLIC EETEARRRPPLCCYTSSSTOEEIIIIIC... f- SFOREFINF(e.G.))
p then
else if LEARN/OLICYCCADDDDENNGGC... + ADDREFINE(C.G.C)
p then
else if LEARKFPLLICYGGPPSTREEENNGGGGG) p then
G + PASTREFINE(C.G..)
else if LEBANPPLLCYCC.ORREEEEEE...)))> then
+ ORREFINE(e.G..)
end if
II < A(G) [set of policies for updated abstract graph G] end if
end for Return and IT
AUTOSPEC iterates through all edges e u - u' of the abstract graph G for which the specification- guided RL algorithm AA has learned policy but for which the reach-avoid task satisfaction probability is below the provided probability threshold p. For each such edge, AUTOSPEC performs four refinement procedures that focus on different possible reasons for the edge u + u' being challenging for learning a satisfactory policy.
ReqRefine, which invoked first, tries to locally refine the problematic edge = + u' by using predicate refinement techniques to refine the labeling function at the target region associated to the vertex u' and the safety region associated the edge e. SeqRefine fails to improve performance above threshold, AUTOSPEC invokes AddRefine which attempts to add waypoint (i.e. new abstract graph vertex) between the vertices u and u', making path-fine finding easier. If AddRefine also fails, AUTOSPEC invokes PastRefine which tries to refine the source node u. Finally, if other refinement procedures fail, AUTOSPEC invokes OrRefine which aims to find alternative paths to u'.
After each attempted refinement, off-the-shelf RI. algorithm (LEARNPOLICC in Algorithm ! is used to estimate the satisfaction probability of the refined edge. When a refinement succeeds in achieving satisfaction probability above p, the refined abstract graph G is updated and AUTOSPEC applies the ieeifiicationguudee RL algorithm A to learn a new set of edge policies for the entire graph. At the end, the final abstract graph G corresponds to the refined specification o, of the input specification Ø
3.1
SPECIFICATION REFINEMENT SUBPROCEDURES
We now define the four specification refinement subprocedures used by AUTOSPEC in Algorithm Each procedure addresses specific type of specification inadequacy, and they are applied in order of increasing structural modification to the abstract graph. The detailed pseudocodes are provided the Appendix. Once problematic edge below threshold p), AUTOSPEC samples trajectories Ç using the learned policy, where the number of trajectories is an algorithm hyperparameter.
- u' is identified (an edge with satisfaction probability
5

---

Peo
Peculs)
(a) ReachRefine
(b) AddRefine
(c) PastRefine
(d) OrRefine
Figure Illustrations of abstract graph refinement processes. (a) ReachRefine demonstrating removal of failed part of goal region and addition of unsafe states set to existing avoid. (b) AddRefine
demonstrating addition of waypoint between nodes. (c) PastRefine removes part the source node from where the agent failed (red) to get to the target, and keeps successful start states (green). (d) OrRefine shows how alternative paths (dotted lines) to target are constructed using existing specification nodes.
Refining Predicates. The first refinement subprocedure addresses overly coarse pred- icates in the reach and avoid conditions. For edge e = u - u', SeqRefine refines both the target predicate b B(u') and the safety predicate ((e) by calling two subprocedures:
ReqRefine:
ReachRefine collects all states along sampled trajectories that successfully reached the goal re- gion b. The refined goal region is computed b,- n ConvexHull (reahhe states), effectively excluding unreachable portions of the original target region. AvoidRefine collects states where trajectories entered unsafe regions (complement of The refined safe region is computed as e, = c ConvexHull(Iast unsafe trajectory states), where A: is a hyperparameter specifying how much of the trajectory tail remove. This removes demonstrated unsafe areas from the safety region.
SeqRefine returns a refined graph G. identical to G except with updated labeling: 8, (y') = b, and B, (e) c,, This refinement provides more precise guidance by excluding problematic regions discovered through exploration.
AddRefine: Introducing Waypoints. The second refinement addresses long or complex paths by decomposing them. When direct navigation from u to u' proves difficult, AddRefine introduces an intermediate vertex z by collecting midpoint states from successful trajectories that reached 3(u'). defining ((u") ((e) n ConvexHull (midpoont) and replacing edge - u' with two edges: e" u u" and e u² n' This decomposition breaks challenging long-horizon task into two shorter subtasks that are easier learn.
PastRefine: Partitioning Source Regions. The third refinement addresses heterogeneous starting conditions where some initial states in consistently lead to success while others lead to failure. PastRefine separates trajectories into successful and failing sets based on whether they satisfied edge then learns a hyperplane separating successful from failing initial states. It creates region b, containing successful starting states and introduces new vertex u' with 3(u") = b, having the same incoming edges u. The refinement replaces problematic edge As shown in Figure (aa), this refinement identifies and isolates promising initial conditions while preserving the original vertex u and its connections.
- u' with e u² w'.
Exploiting Alternative Paths. The fourth refinement addresses blocked or infeasible direct paths by leveraging the existing graph structure. When the path through edge e cannot be made satisfactory, OrRefine identifies alternative parents of n' (vertices u; with existing edges e U, + n'), and for each viable U; adds new edge Cnew and B(e;) ((e) (ee)). It then tests if the alternative path -> u; - u' achieves the threshold. As illustrated in Higure[(b) this creates alternative routes to the target using only existing vertices, maintaining all original safety constraints. OrRefine can iteratively explore ancestors of u; if the direct connection fails.
OrRefine:
w'
+ ut with 3(enew) B(e)
As shown in Algorithm D any specification-guiiee RL algorithm that is applicable to SpectRL specifications and that learns policies for edges the abstract graph can be integrated into the AUTOSPEC framework. The specification-guii guideed RL algorithm learns policies for edges in the abstract graph, until it is unable to proceed beyond an edge with sufficient satisfaction probability. We then perform the refinements in AUTOSPEC, using sampling estimate the satisfaction probability

---

of each refinement until one is found to exceed the threshold. This refinement is used create updated abstract graph and an updated set edge policies are learned with respect to this graph.
3.2 CORRECTNESS OF AUTOSPEC
The following theorem establishes correctness AUTOSPEC, showing that the specification o, computed by AUTOSPEC is indeed refinement of the input specification ø. The proof, provided in the Appendix, proceeds by proving that each of the four refinement procedures results a specification refinement.
Theorem (Correctness of AUTOSPEC), Given an abstract graph G of SpectRL, specification and an edge AUTOSPEC computes a specification the and returns an abstract graph G, and an edge E, such that or refines 6. That is, for any MDP trajectory S, we have (5 or) = (c
Incompleteness of the Specification Refinement Problem. AUTOSPEC provides soundness guar- antees - as shown in Theorem T. the produced specification is guaranteed to be a refinement of the original specification must also satisfy the original specification. However, AUTOSPEC does not provide completeness guarantees. This is a limitation of AUTOSPEC, but inherent property of the specification refinement problem itself because the problem is unlecidable. This is because, even for the simplest case of reachability specifications (e.g.. "reach region G with probability least p"). deciding whether a given policy satisfies a specification is undecidable for general continuous-stan MDPs or probabilistic programs capable of encoding purine-complete behavior Kaminski & Katoen (205)). Consequently, no specification refinement algorithm can be both sound and complete. AUTOSPEC therefore focuses on soundness, which is important towards ensuring that policy for the refined task also solves the task defined by the original specification.
in Definition? 2 and every trajectory that satisfies the refined satisfaction
4 EXPERIMENTAL EVALUATION
We evaluate AUTOSPEC on its ability to diagnose and repair specification failures that prevent existing algorithms from learning satisfactory policies. Our experiments address three questions: (1)
Can AUTOSPEC correctly identify which refinement type needed for different failure modes? (2)
Do the refinements enable learning from previously unlearnable specifications? (3) What the requirements and limitations the refinement process?
4.1 EXPERIMENTAL SETUP
We integrate AUTOSPEC with two specification-guii RL algorithms: DIRL Jothimurugan et al. (2021) which uses Dijkstra-style graph search with systematic exploration, and LSTS Shukla et al. (2024), which uses multi-armed bandits for edge selection with epsilon-greedy exploration. These algorithms differ fundamentally in their exploration strategies, allowing to examine how AUTOSPEC's 's effectiveness depends on the underlying learning algorithm. We evaluate on two domains specifically chosen stress-test different aspects of specification refinement:
n- n-Rooms: Grid-based navigation with walls and doors, providing controlled tests of specific failure modes. State space: (xr, y, 0, E 4 (position, angle to goal, distance). Action space: (u, 0) R² (velocity. direction). The n-rooms domain has been extensively used in specification-guide RL research Jothimurugan et (202T 2019): Zikelic al.) (2023b) as provides clear geometric structure while still presenting challenging long- horizon tasks. Its modular room structure naturally creates the types of specification failures we aim to address: trap states at room boundaries, dangerous narrow passages between rooms, and multiple alternative paths through different door configurations.
PandaGym Gallouédec et al. (2021): Robotic manipulation requiring 3D navigation around obsta- cles. This domain tests refinement in high-dimensional continuous control where geometric intuitions may not apply directly. Following recent work showing the challenges of specification -guided RL in manipulation tasks Shukla et al. (2024), hyperplane-bare based refinements remain effective high- nigh-dimensional spaces where human intuition about specification failures is limited.
this domain to validate that our convex hull and
7

---

For learning edge policies, both algorithms use PPO Schulman al. (2017) with stable- 3abbeeb Raf fin et al. (2021) implementation, following the standard practice in recent specification eeeciiicaioonguidee guided RL workJothiuurugan et al. (202T); Zikelic al. (2023b). We use 2-layer networks (64 neurons each), learning rate 0.0003, and standard PPO hyperparammtees.
all experiments we evaluate refinements using deliberately high satisfaction threshold (p 0.99). The purpose of this choice is method- ological: by selecting a probability level that is difficult to achieve under coarse or under-specified predicates, can clearly observe how the cumulative probability of satisfying the specification improves as AutoSpec performs successive refinements. Using such stringent threshold ensures that even small improvements in guidance become visible the satisfaction curves and allows us to measure the full extent of the benefit provided by refinement, independent of how poorly the initial specification performs.
All experiments are repeated over five random seeds. Plots report the mean across the five runs, with error bars showing the empirical mean variance. Specifically, each data point in the learning curves represents the performance of policy trained for the distinct number of timesteps indicated on x-axis (e.g., policies are trained for 80,000, 100,000, and 120,000 steps independently across 5 seeds). To estimate the specification satisfaction probability (y-axis), the trained policy for each edge is evaluated over 1000 rollout trajectories to empirically count successful versus failed attempts. The final success probabilities displayed in the plots calculated using the product of success probability of the best path from start to goal.
4.2
EFFECTIVENESS: DIRL vs LSTS
M14
CON.
155
Figure 3: 100-rooms Environment with marked regions its DAG specification
Our experiments reveal that AUTOSPEC's effectiveness depends critically on the base algorithm's exploration strategy. We demonstrate this through 100-rooms environment (Figure with the complex specification: o Φstarti (0m1 or Φmz); 6mai (0m1 or óms): Øgoal
This specification structure, with multiple disjunctive branches and sequential compositions, rep- resents the type of complex task decomposition that prior work Jothimurugan et al. (2019) 2021) has identified as necessary for real-world applications but challenging for existing algorithms. The 100-rooms scale specifically tests whether refinements remain effective when the state space is large enough that exhaustive exploration is infeasible, reflecting concerns raised in SSukka et al. 2024) about scalability of compositional methods.
(a) Mid-goal DIRL performacce (b) Full-spec DIRI, performace (c) Mid-goal LSTS performance
Figure 4: Task satisfiability curves representing performances of DIRL and LSTS for sub- specifications and complete specification
8

---

With DiRL (Successful Refinement). As shown in Figure a- DiRL's systematic exploration enables successful refinement. The algorithm explores edges in order of estimated difficulty, providing sufficient trajectory data for each edge before moving to the next. AUTOSPEC successfully applies ReachRefine on the Φm1 edge to remove unreachable portions of the target region, PastRefine on the @m3 edge identify successful starting regions, and OrRefine when direct paths fail to find alternative routes through 6m2. The satisfaction probability improves from near 0% to approximately 60% through these refinements.
With LSTS (Refinement Failure). Figure c)) shows LSTS failing on the same specification. The bandit-based exploration spreads effort across all edges simultaneously, preventing deep exploration of any single edge. Consequently, edges to M4, M5, and Goal achieve 0% satisfaction, providing no successful trajectories for refinement computation. AUTOSPEC correctly reports its inability to refine without samples, demonstrating that refinement quality fundamentally depends on the base algorithm's 's exploration strategy.
Evaluation on Randomized 100-rooms and predicate placement To evaluate the generalization capabilities of our framework, we deployed AUTOSPEC a procedurally generated Way Gridworld where wall connectivity, and predicate placement were fully randomized for each seed (see the Appendix for generation details). This setup specifically tests the system's 's ability to synthesize policies without reliance on hand-engineered specifications or environment-speedee shown in Figure 6. AUTOSPEC significantly outperforms the DIRL baseline, achieving a terminal success probability of approximately 60% compared to the baseline's 's stagnation at 20%. These results confirm that AUTOSPEC autonomously identifies and resolves task bottlenecks, raising success rate of critical transitions from < 20% to 90% via automatic refinement, see the Appendix.
heuristics. As
4.3 EVALUATION OF INDIVIDUAL REFINEMENTS
We design targeted experiments isolating specific failure modes to validate each refinement procedure.
ReqRefine: Trap State Elimination (Figure 7). Setup: 9-rooms environment where the goal region includes a blocked room creating a trap state. Failure mode: Agent reaches the trap portion of the goal and cannot escape. Refinement: ReachRefine identifies that successful trajectories only reach the accessible portion of the goal. The refined specification excludes the trap region: b,
= bn Hulteeeehullrrecche states). Result: Satisfaction probability improves from 15% to 85%, demonstrating AUTOSPEC's ability to learn environmental constraints not captured in the original specification.
ReqRefine: Safety Constraint Diseovery (Figure 8). Setup: 9-rooms with a narrow dangerous passage below the goal. Failure mode: Shortest path goes through narrow passage where agent frequently fails. Refinement: AvoidRefine identifies failure states near the narrow passage. The refined specification expands the avoid region: c, c ConvexHull(aast 10 failure states). Result: Agent learns to use wider but longer safe path, improving satisfaction from 30% to 75%.
AddRefine: Waypoint Introduction (Figure Setup:
Long-horizon navigation across multiple rooms. Failure mode: Direct path too complex for single policy to learn reliably. Refinement: AddRefine identifies midpoints of successful trajectories and introduces intermediate vertex v".
Result: Decomposes task into two manageable subtasks, improving satisfaction from 20% to 90%.
PastRefine: Initial State Partitioning (Figure 10). Setup: Starting region includes states from which goal is unreachable. Failure mode: Policy cannot succeed from certain initial states. Re- PastRefine learns hyperplane separating successful from failing starts. Result: Focuses leamiing on viable initial states, improving satisfaction from 40% to 80%.
finement:
OrRefine: Alternative Path Discovery (Figure [1). Setup: Specification with multiple possible
paths: ΦMIDI; ØGOAL or ΦMId2; ÍGOAL- Failure mode: Direct path through MID1 blocked. Refinement: OrRefine adds edge ΦMID1 - ΦMID2. creating alternative route. Result: Enables satisfaction through alternate path when direct path has 0% success.
4.4 HICH--DIMENSIONAL VALIDATION: PANDAGYM
To validate beyond grid environments, we test AUTOSPEC on PandaGym's continuous 3D manipulation task. The specification requires navigating around an invisible wall:

---

Scitad
Figure 5: Evaluation of AUTOSPEC on PandaGym: (a) Two perspectives of the environment (Ist and 2nd Figures), where the red region is intermediate goal and an invisible wall blocks direct paths. (b) Performance DiRL with and without AUTOSPEC: ReachRefine on first edge (3rd Figure) and PastRefine second edge (4th Figure).
(reach red-region avoid wall); (reach green-region avoid wall). The invisible wall creates chal- lenging scenario where the agent cannot directly observe the obstacle, making specification refinement crucial.
As shown in Figure 5 AUTOSPEC with DiRL successfully applies ReachRefine on the first edge to identify and exclude unreachable portions of the red region behind the wall, focusing the policy achievable subgoals. On the second edge, PastRefine learns that only certain approach angles from the red region lead to successful reaching of the green region, effectively partitioning the intermediate state space based on trajectory outcomes. This demonstrates that AUTOSPEC's geometric refinements (convex hulls for ReachRefine. hyperplanes for PastRefine) remain effective in high- nigh-dimensional spaces where human intuition about the specification failures would be difficult. The success in this domain particularly noteworthy because the refinements must capture 3D spatial relationships without explicit knowledge of the obstacle geometry.
Computational Overhead. AUTOSPEC avoids full retraining by only updating the policies associated with the identified subset of refined edges R. The total computational cost is formalized as Trotal Thase + +..ER Te. Since [R] typically small relative to the initial graph size, the aggregate overhead is bounded (empirically Tiotll base). In the 100-room experiments, the baseline required ~ 240s to evaluate the fixed edges, while AUTOSPEC averaged 390 + 42s. This overhead corresponds directly to the training of 4-7 additional refinement edges per seed. with the observed variance (a ss 42s) driven by the differing topological complexity of the randomized environments. This computational investment is highly efficient, scaling linearly with the number of detected bottlenecks rather than the global state space size. Given the substantial improvement in success probability (from 20% x 60%). this bounded overhead represents favorable trade-off for achieving robust autonomy in stochastic domains.
CONCLUSION
We presented AUTOSPEC, framework for automated refinement of coarse- grasine logical specifica- tions in reinforcement learning. AUTOSPEC addresses common specification issues coarse formulas and coarse labeling functions through four refinement procedures that maintain formal soundness. Our experiments on n-rooms and PandaGym environments demonstrate that AUTOSPEC can improve specification satisfiability when integrated with existing algorithms like DiRL and LSTS.
Our evaluation also reveals fundamental limitations: AUTOSPEC requires sufficient exploration data from the base algorithm to compute meaningful refinements. When algorithms fail to generate successful trajectories LSTS did on complex specifications), refinement becomes impossible. Despite these limitations, AUTOSPEC represents the first systematic approach to automatically refining logical specifications based on learning failures. Future work should address reducing exploration requirements for refinement and extending beyond SpectRL to more expressive temporal logics, such as infinite-horizon w-regular specifications. While AUTOSPEC currently relies on finite witnesses, it could be adapted to these settings by decomposing tasks into a finite prefix (amenable to our current DaG-based refinement) and a cyclic suffix (which would require extending our witness analysis to handle infinite behaviors). The design of good specifications remains challenging in practice, and automated refinement an important step toward making specification guided RL more practical.
10

---

REFERENCES
David Abel, Will Dabney, Anna Harutyunyan, Mark K. Ho, Michael L.. Littman, Doina Precup. and Satinder Singh. On the expressivity of Markov reward. In Advances in Neural Information Processing Systems, 2021.
Derya Aksaray, Austin Jones, Zhaodan Kong, Mac Schwager, and Calin Belta. Q-learning for robust satisfaction of signal temporal logic specifications. In 55th IEEE Conference Decision and Control, CDC 2016, Las Vegas, NV, USA, December 12-14, 2016, pp. 6565 6570. IEEE, 2016. doi: 10.1109/CDC:2201..7999777 URL https: org 11w.11199//// 2016 7799279
Rajeev Alur, Suguman Bansal, Osbert Bastani, and Kishor Jothimurugan. A framework for trans- forming specifications in reinforcement learning. pp. 604-60444449 624, 2022.
Rajeev Alur, Suguman Bansal, Osbert Bastani, and Kishor Jothimurugan. Specification-guuee reinforcement learning. 2023.
Michael Bowling, John D Martin, David Abel, and Will Dabney. Settling the reward hypothesis, 2023.
Alberto Camacho, Rodrigo Toro Icarte, Toryn Q Klassen, Richard Anthony Valenzano, and Sheila A. Mcllraith. L.T. and beyond: Formal languages for reward function specification in reinforcement learning. In Sarit Kraus (ed.), Proceedings of the Twenty-Fight International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pp. 6065-6073, ijcai.org, 2et.////....9991111
2019. doi: 10.24963/UCAA2201999440 84C
Krishnendu Chatterjee, Thomas Henzinger, Mathias Lechner, and Dorde Zikelic. learner- verifier framework for neural network controllers and certificates of stochastic systems. In Sriram Sankaranarayanan and Natasha Sharygina (eds.), Tools and Algorithms for the Construction and Analysis of Systems- 29th International Conference, TACAS 2023, Held as Purt of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22- 27, 2023, Proceedings, Part I, volume 13993 of Lecture Notes in Computer Science, pp. 3-25. Springer, 2023. doi: 10.1007/978- 3-1199788---03--823333
URL https: dww. U1L
Quentin Gallouédec, Nicolas Cazin, Emmanuel Dellandréa, and Liming Chen. panda-gym: Open- Source Goal-Conditioned Environments for Robotic Learning. 4th Robot Learning Workshop: Self-Supervised and Lifelong Learning at NeurIPS, 2021.
Giuseppe De Giacomo, Luca Iocchi, Marco Favorito, and Fabio Patrizi. Foundations for restraining bolts: Reinforcement learning with Itlf/ldff restraining specifications. In J. Benton, Nir Lipovetzky, Eva Onaindia, David E. Smith, and Siddharth Srivastava (eds.), Proceedings of the Twenty-Ninth International Conference Automated Plamning and Scheduling, ICAPS 2019, Berkeley, CA. USA, July 11-15, 2019, pp. 1 136. AAAI Press, 2019. URL htt.ps://osss..coot aaai............................ / index.
wwt.vviwww///e 3549
Emst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, and Dominik Wojtezak. Omega-regular objectives in model-free reinforcement learning. In Tomás Vojnar and Lijun Zhang (eds.), Tools and Algorithms for the Construction and Analysis of Systems 25th International Conference, TACAS 2019, Held as Part of the European Joint Confer- ences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings. Part volume 11427 of Lecture Notes Computer Science, pp. 395 412. Springer, 2019. doi: 10. 1000000997---33300 17462-01 2 978 3 030 17:00-7766--00 27
1007/
Mohammadhosein Hasanbeig, Yiannis Kantaros, Alessandro Abate, Daniel Kroening, George J. Pappas, and Insup Lee. Reinforcement learning for temporal logic control synthesis with proba- bilistic satisfaction guarantees. In 58th IEEE Conference Decision and Control. CDC 2019, Nice, France, December 11-13, 2019, pp. 5338-5343, IEEE, 2019. doi: 10. 1099CDC44002420019 9028919. URL httpt: ttcsps://dol org 111.:....111.111.
201 9. 9028919

---

Mohammadhosein Hasanbeig, Daniel Kroening, and Alessandro Abate. LCRL: certified policy synthesis via logically-constrainee reinforcement learning. In Erika Ábrahám and Marco Paolieri (cds.), Quantitative Evaluation of Systems 19th International Conference, QEST 2022, Warsaw, Poland, September 12-16, 2022, Proceedings, volume 13479 of Lecture Notes in Computer doi: //doi. 000000/99788---31--336-----6061
Science, pp. 217-231, Springer, 2022.
11
URL https?
Sinan Ibrahim, Mostafa Mostafa, Ali Jnadi, Hadi Salloum, and Pavel Osinenko. Comprehensive overview of reward engineering and shaping in advancing reinforcement learnin applications, 2024. URLhttps: //axivv.//xvvvvv//a www.rwwww..gggaeeooooo abs 2408 10215
Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Anthony Valenzano, and Sheila Mcllraith, Using reward machines for high-level task specification and decomposition in reinforcement learning. In Jennifer G. Dy and Andreas Krause (eds.). Proceedings of the 35th International Conference Machine Learning, ICML 2018, Stockholmsmässan Stockholm, Sweden, July 10-15, 2018, volume 80 of Proceedings of Machine Learning Research, pp. 2112-1122221111 2121. PMLR, 2018. URL http::/proceecingg mwr.. prwss v/0 www.teaaatte.a....cc.... wat.://teel/aaaaaaaaaaaaaaaaa html
Mathias Jackermeier and Alessandro Abate. DeepLTL: Learning to efficiently satisfy complex LTL specifications for multi-task RL. In The Thirteenth International Conference on Learning Representations, 2025. URL
Peng Jin, Jiaxu Tian, Dapeng Zhi, Xuejun Wen, and Min Zhang. Trainify: A cegar-driven training and verification framework for safe deep reinforcement learning. In Sharon Shoham and Yakir Vizel (eds.), Computer Aided Verification. pp. 198-218, Cham, 2022. Springer International Publishing. ISBN 978-3-031-13185-1
Kishor Jothimurugan, Rajeev Alur, and Osbert Bastani. A composable specification language for reinforcement learning tasks. Advances in Neural Information Processing Systems, 32, 2019.
Kishor Jothimurugan, Suguman Bansal, Osbert Bastani, and Rajeev Alur. Compositional rein- forcement learning from logical specifications. In A. Beygelzimer, Y. Dauphin. P. Liang, and J. Wortman Vaughan (eds.), Advances in Neurul Information Processing Systems, 2021. URL ew net www.:nteffrrmmmiiiiicmmm
Benjamin Lucien Kaminski and Joost-Picter Katoen. On the hardness of almost-sure termination. In International Symposium Mathematical Foundations of Computer Science, pp. 307-318. Springer, 2015.
Mathias Lechner, Dorde Zikelic, Krishnendu Chatterjee, and Thomas A. Henzinger. Stability verification in stochastic control systems via neural network supermartingales. In Thirty-Sixti AAAI Conference on Artificial Intelligence, AAAI 2022. Thirty-Forrth Conference on Innova- tive Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educa- tional Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 March 1,
2022, pp. 7326-7336, AAAI Press, 2022. doi: 10.1609/AAALV3661 20695. URL https doi /oi..rgg/113 10. 1609 htt.//aaa...v........ 20695
Sergey Levine, Chelsea Finn, Trevor Darrell, and Pieter Abbeel. End-to-end training of deep visuomotor policies. J. Mach. Learn. Res., 17:39:1-39:40, 2016. URL
papers/v17/15-5/5 html
Xiao Li. Cristian-Loan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 3834-3839 IEEE, 2017a.
Xiao Li, Cristian loan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2017, Vancouver, BC, Canada, September 24-28. 2017, pp. 8206234. URL htt.:http//cccc.mm org 0. 1109 TRCS 2017. 82228
IEEE, 2017b. doi: 10. 10.1 1911
12

---

Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Andrei A. Rusu, Joel Veness, Mare G. Bellemare, Alex Graves, Martin A. Riedmiller, Andreas Fidjeland, Georg Ostrovski, Stig Pe- tersen, Charles Beattie, Amir Sadik, loannis Antonoglou, Helen King, Dharshan Kumaran, Daan Wierstra, Shane Legg, and Demis Hassabis. Human-level control through deep rein- forcement learning. Nat., 518(7540):529 533, 2015,
doi: 10. 10.1038/NATTRE144366 URL
Cyrus Neary, Christos Verginis, Murat Cubuktepe, and Ufuk Topeu. Verifiable and compositional reinforcement learning systems. In Proceedings of the International Conference on Automated Planning and Scheduling, volume 32, pp. 615-623, 2022.
Cyrus Neary, Aryaman Singh Samyal, Christos Verginis, Murat Cubuktepe, and Ufuk Topeu. Ver- ifiable reinforcement learning systems via compositionality. arXiv preprint arXiv:2309.066 04420, 2023.
Martin L.. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley, 1994. ISBN 978-0-471619777-2, doi: 10.1002/ 9780470316887. URL httpss://do wwtp//o.orr//... 1002 /ttp://...0000077777701111661681
Wenjie Qiu, Wensen Mao, and He Zhu. Instructing goal-conditioned reinforcement learning agents with temporal logic objectives. In Thirty-seventh Conference on Nearal Information Processing Systems, 2023. URL
Antonin Raffin, Ashley Hill, Adam Gleave, Anssi Kanervisto. Maximilian Ernestus, and Noah Dormann. :able- Reliable reinforcement learning implementations. Journal of Machine Learning Research, 22(268):1 2021. URL wtt.ttt::///////t httphhtttpm/mm///e wwwpplr.rrgppppss//e/eoea
20- 1364. html
John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms. CoRR, 0obs/1777.06330 2017. URL http::/arxiv..rgg/ http:/rxivv..cc org. /bs/
1707. 06347
Yash Shukla, Tanushree Burman, Abhishek Kulkarni, Robert Wright, Alvaro Velasquez, and Jivko Sinapov. Logical specifications--uider dynamic task sampling for reinforcement learning agents. In 34th International Conference on Automated Planning and Scheduling, 2024. URL https
7/ http://iwwwweeeettooommemeeeeeee http:/oorrmmmdd-ooooojjjj333
David Silver, Aja Huang, Chris J. Maddison, Arthur Guez, Laurent Sifre, George van den Driess- che, Julian Schrittwieser, loannis Antonoglou, Vedavyas Panneershelvam, Mare Lanctot, Sander Dieleman, Dominik Grewe, John Nham, Nal Kalchbrenner, llya Sutskever, Timothy P. Lillicrap, Madeleine Leach, Koray Kavukeuoglu, Thore Graepel, and Demis Hassabis. Mastering game of go with deep neural networks and tree search. Nat., 529(7587::4444499 10.1038/NATURE16661.. URL /RLtttps:://dbd/
2016. doi:
Richard S Sutton and Andrew G Barto. Reinforcement learning: An introduction. MIT press, 2018.
Rodrigo Toro Icarte, Ethan Waldie, Toryn Klassen, Rick Valenzano, Margarita Castro, and Sheila McIlraith. Learning reward machines for partially observable reinforcement learn- ing. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché-Buc, E. Fox, and R. Gar- nett (eds.), Advances in Neural Information Processing Systems, volume 32. Curran Asso- ciates, Inc., 2019, htL.httpp.//prrceedingg... neuriss papperr Files/paper/ 2003ff114/5220442223311111663333
Pashootan Vaezipoor, Andrew C Li, Rodrigo A Toro Icarte, and Sheila A Mcilraith. Ltl2action: Generalizing instructions for multi-task rl. International Conference on Machine Learning, pp. 10497-10508. PMLR, 2021.
Zhe Xu and Ufuk Topcu. Transfer of temporal logic formulas in reinforcement learning. In Sarit Kraus (ed.), Proceedings of the Twenty-Eight International Joint Conference Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16. 2019, pp. 4010 4018. ijcai.org. 2019. doi: 24963//JCAAL22099/91 U Utthhttsss///b...r///2....2..
20195555
13

---

Dorde Zikelic, Mathias Lechner, Thomas A. Henzinger, and Krishnendu Chatterjee. Learning control policies for stochastic systems with reach-avoid guarantees. In Brian Williams, Yiling Chen, and Jennifer Neville (eds.), Phirty-Seventh AAAI Conference Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium Educational Advances in Artificial Intelligence, FAAI 2023, Washington, DC, USA, February 7-14, 2023, pp. 11926-11923 1935, AAAI Press, 2023a. doi: 10. 10.1609/AAALV37710226666 http::///ol...r///1111000333 www.//00.....................a.. w3w..........2000
Dorde Zikelic, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas Hen- zinger. Compositional policy learning in stochastic control systems with formal guarantees. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Advances in Neural Information Processing Systems 36: Annual Conference Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 16. 2023, 2023b. pttps//peoonutttta///o/ooooorrop nips. 35227/0C..SSSST.TT.....TTTTAAT..
14


Reviews:
[{"review_id": "TIkaTefdz2", "reviewer": "Reviewer_7JgF", "summary": "The authors propose a method for automatically refining specifications defined using the SpectRL framework and that are used for specification-guided reinforcement learning. Their technique produces a provable refinement of the original specification (a trace satisfying the refined specification implies that the trace also satisfies the original specification). By using the refined specifications to retrain the RL policies, the authors observe that the newly trained policies have higher specification satisfaction rates. In other words, better specifications result in better policies.", "questions": "Please address and discuss weaknesses above.", "limitations": "", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 3, "strengths": "- Problem statement is relevant, interesting, and well defined.\n- The authors do a good job of explaining the preliminary material needed to understand their work.\n- The results show that their method significantly improves the performance of the re-trained policies to meet the original specification after refinement.", "weaknesses": "- Some of the presentation of the AutoSpec framework is lacking... specifically Figure 2 really doesn't clarify what the PastRefine refinement procedure does. What's the relationship between the two parts of the figure? It also leaves a ton of open whitespace, which looks sloppy.\n- It would be nice to have visuals on how each of the refinement procedures is working, not just PastRefine.\n- The experimentation and presentation of it is lacking significantly\n\t- Only use 2 experimental setups (n-Rooms and PandaGym)\n\t- There are 2 tunable hyperparameters (the probability threshold and the number of traces to sample) the details of which are never mentioned for their experiments.\n\t- They never discuss the cost of doing the specification refinement (how long does it take? does retraining the policy take as long?) This would mean training 2x since we have to train all over again to integrate specification refinement.\n\t- They never describe how many times the experiment was attempted. Did they train a bunch of different policies and try it multiple times? Or are the results they show just from training one policy for each of the specification-guided RL algorithms mentioned and trying their framework on it? I am assuming the former, which is limited experimentation in my opinion.\n\t- They don't compare to any other specification refinement or generation techniques for specification-guided RL.\n\t- Figure 4 is a plot of \"Best Path Cost\" on the y-axis vs. \"Number of Timesteps\" on the x-axis. They never introduce what path cost is or what it means to have best path cost. How should these plots be interpreted?\n\t- Figure 5 doesn't have any labels on the x and y axes, so it is unclear what results are being demonstrated.\n\nMinor comments / typos:\n- Missing space between guarantees and citation (Lechner et al.) on pg. 2, line 104\n- I believe the \"AddRefine: Introducing Waypoints.\" part should be given a new line in section 3.1. All of the other specification refinement procedures are given their own new lines when introduced.\n\nThe paper introduces a compelling strategy for improving specification-guided RL by refining the specifications, but it lacks strong experimentation to be convincing. While apparently theoretically sound, much more experimentation would be necessary (more experimental setups, try on more specification-guided RL algorithms and for multiple different trained policies, a stronger ablation study than shown in section 4.3 by again running more experiments, also experiments controlling the tunable hyperparameters, experiments comparing to other related methods, and better presentation of the results).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "Oqk1RvCYzo", "reviewer": "Reviewer_Ui5g", "summary": "Specification guided reinforcement learning often fails when initial logical task descriptions and their labeling functions are too coarse. The paper proposes $\\mathrm{AutoSpec}$, a framework that refines SpectRL specifications through an exploration driven loop and four refinement procedures, while guaranteeing that any trajectory that satisfies the refined specification also satisfies the original specification. The method integrates with existing algorithms and is demonstrated with $\\mathrm{DIRL}$ and $\\mathrm{LSTS}$, where refinements help recover learnability on tasks that were previously hard to solve.", "questions": "1. What is the computational overhead of $\\mathrm{AutoSpec}$ in the reported settings, relative to running $\\mathrm{DIRL}$  or $\\mathrm{LSTS}$  alone? A wall clock comparison and a complexity view in terms of the number of edges and sampled trajectories per refinement would help readers assess practical costs.\n2. How do the procedures behave when a specification needs several consecutive refinements? Is there an observed depth beyond which refinements fail to improve satisfaction probability or become unstable?", "limitations": "", "rating": 4, "confidence": 5, "soundness": 2, "presentation": 2, "contribution": 2, "strengths": "- The paper addresses an important challenge in formulating specifications for RL. Automatically refining predicates and specifications provided to the agent is a promising direction, particularly because crafting appropriate predicates is difficult and loosely defined specifications can be hard to satisfy.\n- The framework is integrated with established specification guided algorithms and the experiments illustrate how the refinements interact with the different exploration strategies of $\\mathrm{DIRL}$ and $\\mathrm{LSTS}$.", "weaknesses": "- The empirical scope is narrow. Only two domains are considered, n Rooms and PandaGym. This limits the evidence for scalability and diversity of specifications. A broader study that samples many predicate regions or includes a less contrived multi room world would strengthen the case.\n    - The specifications tested upon are quite limited (only 1 or 2 refinements per specification needed). A sample driven testing approach (say randomly chosen predicate regions) or a less contrived 100 room example would be more convincing of the scalability of the approach.\n    - I appreciate the carefully chosen experiments for an intuition of what is happening, but some further generalization studies would help (e.g. more than 2 refinements needed and whether $\\mathrm{AutoSpec}$ covers the search space appropriately).\n- When there are no successful samples, certain refinements cannot be computed, as observed for $\\mathrm{LSTS}$ on the complex specification. The approach is sound but not complete and it may fail to find a refinement even if one exists.\n- `AvoidRefine` only enlarges the avoid set or equivalently reduces the safe set, without permitting relaxations when the avoid region is overly conservative. Algorithm 3 defines the refined safe region by removing the convex hull of recent failure states, which can bias the learner away from potentially optimal paths if the initial avoid labeling is narrow or misaligned.  This is acceptable in most situations,  but the onus is on the user specifying the initial predicate regions to start with conservative definitions. A discussion of when to relax an avoid constraint would be valuable.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "n98FLGiZHg", "reviewer": "Reviewer_w6NH", "summary": "The paper considers the problem of automatically refining logical specifications in order to help specification guided reinforcement learning algorithms. The main intuition is that when the specification is very coarse, these algorithms find it hard to learn effective policies. So they propose identifying problematic specifications and refining them to help the algorithms converge faster and also help with guided exploration.\n\nThis work uses the SpectRL specification logic which can be represented as a graph that captures different ways to satisfy the specification. They present several types of refinement procedures that modify the graph and these procedures consist of refining goal/target regions, or adding additional intermediate target regions.\n\nIn their experiments they show that their method greatly helps specification guided RL algorithms to learn effective policies in large gridworld environments as well as robotic manipulation task with obstacles.", "questions": "1. Are there possible failure modes where the refinement procedure would follow a wrong chain of refinements that make the learning task much harder? Perhaps this deserves a short discussion?\n\n2. In the current algorithms, the different refinements are applied in a specific order. Do you imagine situations where this order can be detrimental? \n\n3. Why or why not dynamically choose which refinement to apply at each step?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "This is one of the first few works to consider the problem of automatic refinement of RL specifications based on collected feedback from the training of policies. This is a fundamental issue because if the specification is too coarse grained then algorithms would find it hard to effectively explore the state space and learn good policies.\n\nThe problem they consider is studied in depth and many refinement techniques are proposed that are sound. The benchmarks they consider are also interesting. This work also opens up many interesting related directions that can be explored.", "weaknesses": "While the contributions of the paper are substantive, they can be presented better. The introduction can be expanded to give further intuition with respect to the problem being solved. Specifically, the notion of abstract graph is never introduced informally even though it is central to the paper. Perhaps it would be helpful to take the example in figure 1, and present in some detail about what the refinement procedures would produce and how it would make the learning task easier. Similarly, logical specifications for RL are also never introduced.\n\nThe related work section can also be organized better into paragraphs.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "y6a1t359MB", "reviewer": "Reviewer_fNYW", "summary": "This paper introduces AutoSpec, a framework designed to automatically refine logical specifications for reinforcement learning (RL) tasks. While logical specifications can guide RL agents towards complex goals, a common issue is that coarse-grained or under-specified definitions may prevent agents from learning useful policies.\n\nThe core idea of AutoSpec is to use an \"exploration-guided strategy\" to automatically search for a more detailed specification. This \"refined\" specification is stricter than the original but provides additional guidance to the RL algorithm, making the learning process easier. Crucially, the framework guarantees \"soundness\": any trajectory satisfying the new specification must also satisfy the original coarse one. Theoretical justifications are provided. Experiments demonstrate that agents using specifications refined by AutoSpec can solve more complex control tasks than before.", "questions": "1. See weaknesses 2, please explain the search space and overhead of AutoSpec.\n2. See weaknesses 3, please explain the difficulty of refinement in AutoSpec.\n3. See weaknesses 4, can you discuss [1] and [2] in the paper, and provide some insights on whether AutoSpec can be applied to $ \\omega $-regular LTL specifications?\n4. It seems that AutoSpec detect the failures of a policy and perform refinement, this is good. However, it is possible to perform \"active\" refinement rather than \"passive\"? This could be very interesting.", "limitations": "", "rating": 6, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The issue of \"specification too coarse to learn from\" is a significant practical hurdle in specification-based RL. This paper tackles this problem directly, which is highly valuable.\n2. The primary contribution of AutoSpec is its ability to refine specifications without human intervention. This greatly lowers the barrier to using logical specifications, which might otherwise require extensive manual tuning by domain experts. Also, theoretical justifications are provided to show the framework doesn't just modify specifications arbitrarily; it guarantees that the refined specification is a valid \"subset\" of the original. This is crucial.\n3. The refinement processes to abstract graphs are clear and intuitive, the order of refinement are also reasonable. Overall, the algorithm is easy to follow.", "weaknesses": "1. I am not fully convinced by the name *SpectRL* specification logic. To me, they are just standard subset of Linear Temporal Logic (LTL), clarifying this in the paper clearly is sufficient. We do not really need a separate notation.\n2. The paper mentions that AutoSpec searches for a refinement in order. How large is this search space for each environment, and what is the overhead of this additional procedure? These are not mentioned in the paper.\n3. As discussed in the paper, the reliability of the AutoSpec are heavily dependent on its base algorithm. This limitation is understandable, yet it would be better if additional discussion and proposals can be provided.\n4. As I mentioned in weaknesses 1, this work only discusses a subset of LTL, while other works have already proposed some insights and solutions to the problem [1, 2]. Please consider add discussion of these works and give your own insights.\n5. This is minor, I noticed that two important concepts mentioned in the abstract never mentioned again in the main text. Please explain  what are \"under-specified\" and \"exploration-guided strategy\" in the main text. I know these are the summarizations of later component, but it is better to make them clear.\n\n[1] Qiu et al. Instructing goal-conditioned reinforcement learning agents with temporal logic objectives. NeurIPS 2023.\n\n[2] Jackermeier and Abate, DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL. ICLR 2025.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)