SHF: Formal Reasoning of Reinforcement Learning Policies

Artificial intelligence (AI) systems trained through reinforcement learning (RL) are increasingly deployed in safety-critical settings such as self-driving cars, robotic surgery, and autonomous trading, yet these systems operate without any formal guarantees that they will behave correctly. A core problem is that RL systems learn from numerical rewards that can be gamed by the agent in unintended ways — a phenomenon known as reward hacking — leading to dangerous failures even when the system appears to perform well in training. This project addresses this gap by developing theoretical foundations, provably correct algorithms, and open-source tools needed to build RL systems that are guaranteed to satisfy precise, human-readable behavioral specifications expressed in temporal logic. The project's novelties are the first provably convergent learning algorithms that operate directly on temporal logic objectives without translating them into numerical rewards, a compositional framework for learning over long-horizon tasks with correctness guarantees, and a certification framework that produces externally verifiable proof artifacts for arbitrary RL policies using only black-box access. The project's impacts are enabling safe deployment of RL in regulated industries such as autonomous vehicles and medical robotics, establishing a community-standard open-source platform for specification-guided RL research and education, and training the next generation of researchers at the intersection of formal methods and machine learning. This project develops a three-thrust framework for trustworthy specification-guided RL. Thrust I establishes the first asymptotically convergent direct learning algorithms for RL from temporal logic specifications, bypassing an established impossibility result for probably approximately correct (PAC) guarantees by developing multi-stage stochastic approximation techniques over satisfaction probabilities rather than proxy reward functions; model-free Q-learning and policy gradient variants with neural integration extend these guarantees to high-dimensional continuous environments. Thrust II addresses long-horizon temporal specifications through Maximal End Component (MEC) decomposition, which reduces intractable temporally complex objectives to sequences of reachability problems while preserving specification equivalence and optimality; this thrust additionally develops automated specification refinement and principled unrealizability detection for unknown Markov Decision Processes. Thrust III develops learning-theoretic foundations and model-free algorithms for black-box certification, exploiting the structural insight that any policy satisfying a temporal specification is itself a certificate, so that convergence results from Thrusts I and II lift directly to ranking function and barrier function learning for reachability and safety specifications respectively. All three thrusts are unified in a single open-source tool platform, providing shared infrastructure for direct learning, compositional synthesis, and certification that lowers the barrier for AI and machine learning researchers to build and evaluate formally verified RL systems. 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.