Verifiable and Compositional Reinforcement Learning Systems

TL;DR

This paper introduces a framework for verifiable, compositional reinforcement learning that enables independent training of subsystems with guarantees on overall task satisfaction through formal interfaces and iterative specification refinement.

Contribution

The framework combines a high-level pMDP model with low-level RL subsystems, allowing automatic decomposition, independent training, and iterative adjustment of subtask specifications for compositional RL.

Findings

Guarantees overall task satisfaction if subsystems meet subtask specs.

Automatic decomposition of complex tasks into manageable subtasks.

Iterative refinement improves subsystem policies and task success.

Abstract

We propose a framework for verifiable and compositional reinforcement learning (RL) in which a collection of RL subsystems, each of which learns to accomplish a separate subtask, are composed to achieve an overall task. The framework consists of a high-level model, represented as a parametric Markov decision process (pMDP) which is used to plan and to analyze compositions of subsystems, and of the collection of low-level subsystems themselves. By defining interfaces between the subsystems, the framework enables automatic decompositions of task specifications, e.g., reach a target set of states with a probability of at least 0.95, into individual subtask specifications, i.e. achieve the subsystem's exit conditions with at least some minimum probability, given that its entry conditions are met. This in turn allows for the independent training and testing of the subsystems; if they each learn a policy satisfying the appropriate subtask specification, then their composition is guaranteed to satisfy the overall task specification. Conversely, if the subtask specifications cannot all be satisfied by the learned policies, we present a method, formulated as the problem of finding an optimal set of parameters in the pMDP, to automatically update the subtask specifications to account for the observed shortcomings. The result is an iterative procedure for defining subtask specifications, and for training the subsystems to meet them. As an additional benefit, this procedure allows for particularly challenging or important components of an overall task to be determined automatically, and focused on, during training. Experimental results demonstrate the presented framework's novel capabilities.