FMitF: Track I: Safe Multi-Agent Reinforcement Learning with Shielding

This project combines expertise from formal methods (FM) and reinforcement learning (RL) to develop a novel methodology for building safe multi-agent RL (MARL) systems. RL methods are good at solving complex tasks in real-world environments (e.g., robots learning to navigate unknown environments), but cannot provide "hard" guarantees on safety (e.g., robots guaranteed to never collide with each other). Formal methods provide rigorous safety guarantees, but are difficult to scale to real-world settings. This project seeks to combine the best of both worlds in order to devise methods that are capable of learning to solve complex tasks in real-world environments, while at the same time ensuring safety. The project's novelties are a combination of techniques such as shield synthesis from FM and directed exploration from RL into a novel safety-focused methodology, as well as its implementation into a tool suite and its evaluation on a set of benchmarks. The project's impacts are in transforming the way RL systems are developed and deployed so that they can be used in safety-critical settings. Broader impacts include broadening participation in research to diverse groups and involving undergraduate students. Key concepts of the project are safety shields and safety coaches. Safety shields are to be used in safety-critical situations, where safety is paramount (either during training or during execution). Shields prevent safety violations by intercepting (and modifying) potentially unsafe actions by the agents. Safety coaches are to be used when safety violations can be tolerated (e.g., in virtual training or simulated execution). Coaches train for safety by encouraging agents to make mistakes, and to learn from them. Shields are a known concept, but have not been studied in the most common MARL settings—decentralized execution or partial observability. Coaches are a novel concept introduced in this project, which will teach agents to be safe while solving the task. The project will develop (1) new formal methods and concepts, specifically decentralized shield synthesis and safety coaches, (2) new MARL techniques, specifically, safety-directed exploration, training for safety, and hardwiring safety information directly into agent policies, and (3) novel applications of model learning and abstraction refinement to the MARL setting. 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.