# Formally-Sharp DAgger for MCTS: Lower-Latency Monte Carlo Tree Search using Data Aggregation with Formal Methods

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 31 references that are in the map.
- First posted on arXiv 15 Aug 2023.

## Builds on (most cited first, 8 of 8)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [OpenAI Gym](https://mlsanity.com/paper/1606.01540/) (2016)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Learning an Approximate Model Predictive Controller with Guarantees](https://mlsanity.com/paper/1806.04167/) (2018)
- [Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes](https://mlsanity.com/paper/1809.03299/) (2018)
- [Monte Carlo Tree Search guided by Symbolic Advice for MDPs](https://mlsanity.com/paper/2006.04712/) (2020)

## Built on by (most cited first, 1 of 1)

- [Shields to Guarantee Probabilistic Safety in MDPs](https://mlsanity.com/paper/2605.10888/) (2026)

## Abstract (arXiv)

We study how to efficiently combine formal methods, Monte Carlo Tree Search (MCTS), and deep learning in order to produce high-quality receding horizon policies in large Markov Decision processes (MDPs). In particular, we use model-checking techniques to guide the MCTS algorithm in order to generate offline samples of high-quality decisions on a representative set of states of the MDP. Those samples can then be used to train a neural network that imitates the policy used to generate them. This neural network can either be used as a guide on a lower-latency MCTS online search, or alternatively be used as a full-fledged policy when minimal latency is required. We use statistical model checking to detect when additional samples are needed and to focus those additional samples on configurations where the learnt neural network policy differs from the (computationally-expensive) offline policy. We illustrate the use of our method on MDPs that model the Frozen Lake and Pac-Man environments -- two popular benchmarks to evaluate reinforcement-learning algorithms.