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, which is used to plan and analyze compositions of subsystems,
and of the collection of low-level subsystems themselves. The subsystems are
implemented as deep RL agents operating under partial observability. 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. We present theoretical
results guaranteeing that if each subsystem learns a policy satisfying its
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 high-level model, 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. Experimental
results demonstrate the presented framework's novel capabilities in
environments with both full and partial observability, discrete and continuous
state and action spaces, as well as deterministic and stochastic dynamics.

我们提出了一个可验证和组合的强化学习框架，其中一组强化学习子系统被组合起来以实现整体任务，子系统之间通过定义接口和部分可观察性相互交互。实验结果展示了该框架在各种环境中的新颖功能。