# Neurosymbolic Reinforcement Learning with Formally Verified Exploration

arXiv: https://arxiv.org/abs/2009.12612 · HTML: https://mlsanity.com/paper/2009.12612/

## Key facts

- Cited by 49 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Sep 2020.

## Built on by (most cited first, 30 of 49)

- [A Review of Safe Reinforcement Learning: Methods, Theory and Applications](https://mlsanity.com/paper/2205.10330/) (2022)
- [A Survey on Interpretable Reinforcement Learning](https://mlsanity.com/paper/2112.13112/) (2021)
- [Compositional Reinforcement Learning from Logical Specifications](https://mlsanity.com/paper/2106.13906/) (2021)
- [Safe Reinforcement Learning Using Advantage-Based Intervention](https://mlsanity.com/paper/2106.09110/) (2021)
- [Safe Reinforcement Learning via Probabilistic Logic Shields](https://mlsanity.com/paper/2303.03226/) (2023)
- [Learning Barrier Certificates: Towards Safe Reinforcement Learning with Zero Training-time Violations](https://mlsanity.com/paper/2108.01846/) (2021)
- [Provably Safe Reinforcement Learning: Conceptual Analysis, Survey, and Benchmarking](https://mlsanity.com/paper/2205.06750/) (2022)
- [HardNet: Hard-Constrained Neural Networks with Universal Approximation Guarantees](https://mlsanity.com/paper/2410.10807/) (2024)
- [Neurosymbolic Reinforcement Learning and Planning: A Survey](https://mlsanity.com/paper/2309.01038/) (2023)
- [BertNet: Harvesting Knowledge Graphs with Arbitrary Relations from Pretrained Language Models](https://mlsanity.com/paper/2206.14268/) (2022)
- [Neural Network Repair with Reachability Analysis](https://mlsanity.com/paper/2108.04214/) (2021)
- [MONA: Myopic Optimization with Non-myopic Approval Can Mitigate Multi-step Reward Hacking](https://mlsanity.com/paper/2501.13011/) (2025)
- [Dynamic Model Predictive Shielding for Provably Safe Reinforcement Learning](https://mlsanity.com/paper/2405.13863/) (2024)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)
- [A Survey on Verification and Validation, Testing and Evaluations of Neurosymbolic Artificial Intelligence](https://mlsanity.com/paper/2401.03188/) (2024)
- [Neuro-Symbolic AI: Explainability, Challenges, and Future Trends](https://mlsanity.com/paper/2411.04383/) (2024)
- [Do Androids Dream of Electric Fences? Safety-Aware Reinforcement Learning with Latent Shielding](https://mlsanity.com/paper/2112.11490/) (2021)
- [Program Synthesis Guided Reinforcement Learning for Partially Observed Environments](https://mlsanity.com/paper/2102.11137/) (2021)
- [Writing as a testbed for open ended agents](https://mlsanity.com/paper/2503.19711/) (2025)
- [Reinforcement Learning with Adaptive Regularization for Safe Control of Critical Systems](https://mlsanity.com/paper/2404.15199/) (2024)
- [Formal Explanations for Neuro-Symbolic AI](https://mlsanity.com/paper/2410.14219/) (2024)
- [Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning](https://mlsanity.com/paper/2104.10219/) (2021)
- [Strategy Synthesis for Zero-Sum Neuro-Symbolic Concurrent Stochastic Games](https://mlsanity.com/paper/2202.06255/) (2022)
- [Survey on Applications of Neurosymbolic Artificial Intelligence](https://mlsanity.com/paper/2209.12618/) (2022)
- [Reinforcement Learning with Knowledge Representation and Reasoning: A Brief Survey](https://mlsanity.com/paper/2304.12090/) (2023)
- [Learning of Generalizable and Interpretable Knowledge in Grid-Based Reinforcement Learning Environments](https://mlsanity.com/paper/2309.03651/) (2023)
- [Automaton Distillation: Neuro-Symbolic Transfer Learning for Deep Reinforcement Learning](https://mlsanity.com/paper/2310.19137/) (2023)
- [Uncertainty Quantification for Neurosymbolic Programs via Compositional Conformal Prediction](https://mlsanity.com/paper/2405.15912/) (2024)
- [Guiding Safe Exploration with Weakest Preconditions](https://mlsanity.com/paper/2209.14148/) (2022)
- [A Survey on Explainable Reinforcement Learning: Concepts, Algorithms, Challenges](https://mlsanity.com/paper/2211.06665/) (2022)

## Abstract (arXiv)

We present Revel, a partially neural reinforcement learning (RL) framework for provably safe exploration in continuous state and action spaces. A key challenge for provably safe deep RL is that repeatedly verifying neural networks within a learning loop is computationally infeasible. We address this challenge using two policy classes: a general, neurosymbolic class with approximate gradients and a more restricted class of symbolic policies that allows efficient verification. Our learning algorithm is a mirror descent over policies: in each iteration, it safely lifts a symbolic policy into the neurosymbolic space, performs safe gradient updates to the resulting policy, and projects the updated policy into the safe symbolic subset, all without requiring explicit verification of neural networks. Our empirical results show that Revel enforces safe exploration in many scenarios in which Constrained Policy Optimization does not, and that it can discover policies that outperform those learned through prior approaches to verified exploration.
