Monte Carlo Tableau Proof Search

TL;DR

This paper explores the use of Monte Carlo Tree Search with heuristics, including learned ones, to improve proof search in tableau calculi, demonstrating its effectiveness with the leanCoP prover on Mizar problems.

Contribution

It introduces Monte Carlo Tree Search guided proof search with novel heuristics, including learned strategies, for tableau calculi, and implements it in leanCoP.

Findings

Capable of finding new and different proofs.

Effective proof search guidance through Monte Carlo Tree Search.

Heuristics, including learned ones, enhance proof discovery.

Abstract

We study Monte Carlo Tree Search to guide proof search in tableau calculi. This includes proposing a number of proof-state evaluation heuristics, some of which are learnt from previous proofs. We present an implementation based on the leanCoP prover. The system is trained and evaluated on a large suite of related problems coming from the Mizar proof assistant, showing that it is capable to find new and different proofs.