He Zhu, Ph.D. - US grants

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.

Deep reinforcement learning (RL) has recently gained tremendous popularity in numerous decision-making systems. However, deploying RL techniques in safety-critical domains such as autonomous driving has drawn concerns about its trustworthiness. RL applications can behave unexpectedly because such systems are characterized by intractably large state spaces and only a small fraction of states are explored during training. Lack of trust in a deep neural RL policy is further exacerbated by the difficulty of identifying how logical notions of safety relate to the uninterpretable policy network structure. The project's novelty is to explore domain-specific programs as a new learning representation for trustworthy RL. It allows an RL system to be interpreted, formally verified, and debugged as an ordinary programming system. The project's impact is to shape new methodologies to design highly interpretable and verifiable RL systems that are capable of making reliable decisions.


The main contribution of the project is a programmatic RL framework for synthesizing policies that meet both formal correctness specifications and quantitative performance objectives. Firstly, the project develops program synthesis techniques to compose primitive RL policies into composite and interpretable programs to solve sophisticated RL environments. To explore novel compositions, it applies efficient policy gradient methods to search in a continuous relaxation of the discrete space of language grammar rules. Secondly, the project reconciles programmatic policy synthesis with program verification in a correct-by-construction RL loop, constraining policy performance optimization in provably safe state space. Moreover, this project investigates the transferability of programmatic RL by lifting the synthesis and verification framework to first-order relational environments, leveraging relational abstractions to transfer programmatic policies to unseen environments with formal guarantees.

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.