English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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

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