Monte Carlo Connection Prover

Monte Carlo Tree Search (MCTS) is a technique to guide search in a large decision space by taking random samples and evaluating their outcome. In this work, we study MCTS methods in the context of the connection calculus and implement them on top of the leanCoP prover. This includes proposing useful proof-state evaluation heuristics that are learned from previous proofs, and proposing and automatically improving suitable MCTS strategies in this context. 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. To our knowledge, this is the first time MCTS has been applied to theorem proving.