In Reinforcement Learning (RL) agents rely on rewards that promote the achievement of given objectives. Widespread use of RL-enabled systems, such as swarm robots, autonomous vehicles, Internet-of-Things, and social networks, will dramatically improve the quality of modern life. However, their applications in safety-critical settings imply that methods to ensure their correctness are of paramount importance. This project develops a rigorous approach to the design and verification of RL-enabled systems that addresses issues of safety, efficiency, and scalability. Logic provides a foundation for the rigorous specification of learning objectives. Model-free RL, which is the type of learning supported by neural networks, promises scalability. Hence this project is about translating logic-based requirements into the scalar reward form that is needed in model-free RL.
Bridging the gap between logic specifications and model-free RL requires a translation that is faithful (greater reward means higher probability of satisfying the objective) and effective (the reward should help RL algorithms to learn quickly and reliably). This project develops foundations for faithful and effective translations of omega-regular specifications and explores their applications to synthesis of RL-enabled systems. The transition from theory to practice will be measured by the success of an open-source tool for the synthesis of interpreters that translate environment observations into rewards for state-of-the-art, off-the-shelf RL algorithms. Both the formal-methods and the RL communities will benefit from this project. The PIs will extend their record of technology transfer with the release of software and educational materials.
This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.
