Verifiable and Compositional Reinforcement Learning Systems

Summary

Neary, Verginis, Cubuktepe, and Topcu propose a framework for verifiable and compositional RL in which a high-level parametric MDP (pMDP) plans over partially instantiated RL subsystems. Each subsystem has entry conditions, exit conditions, and a time horizon; low-level RL learns policies for the subtasks, while the high-level model decomposes a system-level probabilistic reachability requirement into minimum subtask success probabilities.

The framework is useful for the wiki because it sits between Safe Reinforcement Learning, Probabilistic Model Checking, and compositional task-structured RL. Unlike ordinary hierarchical RL, the high-level model is built specifically to verify reachability guarantees and refine subtask specifications when some subsystem cannot meet its target.

Key Claims

• A modular RL system can be verified compositionally when subsystem interfaces expose entry and exit conditions and when subsystem success probabilities lower-bound the pMDP parameters.
• Task specifications such as “reach the target with probability at least 1-delta” can be automatically decomposed into subtask specifications p_c.
• If every learned subsystem policy satisfies its subtask specification, then the composed meta-policy satisfies the overall task specification.
• The framework can iteratively refine subtask specifications using empirical estimates of subsystem performance, thereby avoiding subsystems that cannot meet their required probability targets within a training budget.
• In labyrinth experiments, the compositional method trains only the needed subsystems, changes route when a lava-room subsystem cannot satisfy its target, and satisfies the overall probability requirement with far fewer training steps than a monolithic PPO baseline.

Methods / Formalism

• The low-level environment is an MDP M=(S,A,P). For policy pi, P^M,pi_s(Diamond S_targ) is the probability of eventually reaching a target set from state s; finite-horizon reachability is written P^M,pi_s(Diamond_{<=T} S_targ).
• A subsystem is c=(I_c,F_c,T_c,pi_c), where I_c is its entry set, F_c its exit set, T_c its time horizon, and pi_c its learned policy.
• A subtask specification requires:

$${\sigma }_c^{{\pi }_c}(s)=P_s^{M,{\pi }_c}({◊}_{\le T_c}{F}_c)\ge p_c\text{for every }s\in I_c.$$

• The collection of subsystems must be composable: for every pair, an exit set is either contained in another subsystem’s entry set or disjoint from it. This makes the high-level successor of a subsystem well-defined.
• The high-level model is a pMDP whose abstract states are equivalence classes over environment states induced by shared subsystem-entry membership and target membership. Each action corresponds to executing a subsystem.
• A high-level transition for subsystem c succeeds with parameter p_c and moves to succ(c), or fails with probability 1-p_c and moves to an absorbing failure state.
• Theorem 1 states that if every subsystem’s true success probability lower-bounds its pMDP parameter p_c, then the real composed system reaches the target with probability at least the high-level model’s predicted probability.
• Subtask specification decomposition is posed as a bilinear optimization problem over pMDP parameters p_c and Bellman-flow variables x(s,c), minimizing required subtask thresholds subject to a high-level reachability constraint.
• ICRL pMDP Specification Decomposition records the pMDP construction, theorem shape, optimization constraints, and iterative refinement loop.

Evidence / Experiments

• The paper evaluates the framework on discrete and continuous labyrinth navigation tasks where subsystems correspond to room-navigation skills.
• In the discrete MiniGrid labyrinth, the state space has 1600 states, actions are turn-left, turn-right, and move-forward, and a 10 percent slip probability makes the environment stochastic.
• Subsystem policies are trained with PPO via Stable-Baselines3; subtask and task success estimates use 300 rollouts; the bilinear program is solved with Gurobi.
• The high-level model’s predicted task success tracks empirical task success in the discrete labyrinth experiments.
• The algorithm initially tries a shorter route through lava rooms, then refines subtask specifications when one subsystem cannot meet its required success probability, and switches to an alternate route avoiding the lava.
• The paper reports that ICRL satisfies the task specification in less than two million training steps, while a monolithic PPO treatment of the whole task takes roughly thirty million steps. The authors caution that this comparison favors ICRL because it receives subsystem entry/exit information.
• A continuous Unity labyrinth with continuous state/action dynamics shows qualitatively similar behavior: the high-level model again shifts training toward an alternate safe route after refinement.

Connections

• Seeds Compositional Reinforcement Learning as the wiki page for modular RL systems whose components are connected by explicit interfaces and high-level task structure.
• Connects to Probabilistic Model Checking because the high-level pMDP is used for probabilistic reachability planning and verification.
• Connects to Safe Reinforcement Learning because the system-level requirement is a probabilistic task/safety guarantee rather than only reward maximization.
• Complements Reward Machines and hierarchical reward-machine notes: those decompose temporal reward/task structure, while Neary et al. decompose probabilistic subtask success requirements over subsystem interfaces.
• Complements Brorholt2025 - Compositional Shielding and Reinforcement Learning for Multi-Agent Systems: both use modularity for assurance, but this paper composes learned subsystems through a pMDP rather than composing shields through assume-guarantee obligations.

Open Questions

• How should the empirical rollout estimates sigma_hat_c be replaced by high-confidence statistical or formal lower bounds in safety-critical deployments?
• Can the framework be combined with temporal-logic product MDPs without making the high-level pMDP too large?
• What design process supplies subsystem entry and exit conditions, and how robust is the guarantee if those interfaces are misspecified?
• How should this pMDP approach interact with shields: should shields enforce each subsystem interface, or should the high-level model plan around shielded subsystem performance?

Citation

Neary, C., Verginis, C., Cubuktepe, M., & Topcu, U. (2022). Verifiable and Compositional Reinforcement Learning Systems. In Proceedings of the Thirty-Second International Conference on Automated Planning and Scheduling (ICAPS 2022), 615-623.