Reinforcement Learning Modulo Formal Verification : A Synergistic Approach to High-Assurance Autonomous Agents
Abstract
Autonomous systems interacting with the physical world, collecting data, processing it using machine learning algorithms, and making decisions, have the potential to transform a wide range of applications including transportation. Realizing this potential requires that the system designers can provide high assurance regarding safe and predictable behavior. This proposal aims to develop design principles, learning algorithms, and analysis tools to build high assurance autonomous systems. The key novelty of the approach is a tight integration of Reinforcement Learning --- a dominant paradigm for training decision systems to take autonomous actions, and Formal Verification --- a mature set of tools and techniques to verify models of systems with respect tomathematically precise high-level correctness requirements. Our team brings together experts in machine learning, software analysis, formal verification, and control theory to execute this multidisciplinary research agenda.Central to the proposed approach is co-design of high-level specifications, learning algorithms, verification tools, and runtime assurance techniques. Research is divided into four thrusts: (1) Requirement specification for RL agents (development of novel notations for formally specifying correctness requirements for learning-enabled, autonomous cyber-physical systems); (2)Verification of neural-network-based policies (a set of new methods and tools for formally verifying closed-loop control systems containing (trained) neural policy modules); (3) Learning modulo verification (development of a new learning paradigm --- reinforcement learning modulo formal verification, that integrates the verification methods into the learning loop, and only learn policies that certifiably satisfy the relevant formal requirements); and (4) Dynamic policy selection via shielding (a set of dynamic methods that select among a set of policies that offer different trade-offs between safety and performance in the reward objective).To demonstrate the utility of the proposed techniques in different thrusts in an integrated manner, and to evaluate the effectiveness in ensuring safety of autonomous systems, robotic vehicles will be used as experimental testbed. In the first phase of the project we will use the F1/10 racing car for deployment, and in later years, more complex scenarios with autonomous sea surface vehiclesin a simulation environment will be used for evaluation.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Apr 29, 2020
- Source ID
- N000142012115
Entities
People
- Rajeev Alur
Organizations
- Office of Naval Research
- United States Navy
- University of Pennsylvania