SHF: Small: Formal Symbolic Reasoning of Deep Reinforcement Learning Systems

Deep reinforcement learning, a type of artificial intelligence, has become pervasive and is being deployed in decision-making systems such as autonomous vehicles. Deep reinforcement learning models are, however, subject to instability in both their training process and their run-time performance. Despite much progress in boosting public trust amid rising concerns about the safety of artificial intelligence, there remain significant challenges to rigorously guarantee the safety of deep reinforcement learning in safety-critical systems. This project integrates a range of symbolic reasoning tasks – rigorous abstraction and verification – enabled by formal-methods technology into reinforcement learning to secure the public's trust in such systems. The project's impact is to establish new paradigms and lay foundations for provably safe deep reinforcement learning that is capable of making trustworthy decisions in complex real-world environments. The project's novelty is to augment the training loop of reinforcement learning with a formal-verification module that reasons about system-level safety properties. First, the project investigates techniques to construct formal and differentiable abstractions of reinforcement-learning agents and environments. By reducing the loss between safety properties and differentiable abstractions using optimization techniques, reinforcement learning can now provide formal assurances of correctness at training time. Second, the project develops environment-modeling and -monitoring algorithms to capture environment conditions at run-time. Reinforcement-learning agents are safely adapted to environment changes guaranteed by formal verification. Moreover, this project provides safety guarantees for vision-based deep-reinforcement-learning systems by encoding each high-dimensional visual input into a symbolic representation that is suitable for formal verification. 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.