Verifiable and Compositional Reinforcement Learning Systems

Abstract

However, there remain significant barriers to their deploy- ment in safety-critical engineering applications. Autonomous We propose a framework for verifiable and compositional vehicles, manufacturing robotics, and power systems manage- reinforcement learning (RL) in which a collection of RL sub- ment are examples of complex application domains that re- systems, each of which learns to accomplish a separate sub- quire strict adherence of the system’s behavior to stakeholder task, are composed to achieve an overall task. The framework consists of a high-level model, represented as a parametric requirements. However, the verification of RL systems is dif- Markov decision process (pMDP) which is used to plan and ficult. This is particularly true of monolithic end-to-end RL to analyze compositions of subsystems, and of the collection approaches; many model-free RL algorithms, for instance, of low-level subsystems themselves. By defining interfaces only output the learned policy and its estimated value func- between the subsystems, the framework enables automatic tion, rendering them opaque for verification purposes. The decompositions of task specifications, e.g., reach a target set difficulty of verification is compounded in engineering appli- of states with a probability of at least 0.95, into individual cation domains, which often require large observation and subtask specifications, i.e. achieve the subsystem’s exit con- action spaces, and complicated reward functions. ditions with at least some minimum probability, given that its entry conditions are met. This in turn allows for the inde- How do we build complex engineering systems we can pendent training and testing of the subsystems; if they each trust? Engineering design principles have long prescribed learn a policy satisfying the appropriate subtask specification, system modularity as a means to reduce the complexity of then their composition is guaranteed to satisfy the overall task individ