Reviews: Reinforcement Learning of Theorem Proving

This paper presents a theorem proving algorithm that leverages Monte-Carlo simulations guided by reinforcement learning from previous proof searches. In particular, to guid the search, the authors use the UCT formula augmented by (1) learning prior probabilities of actions for certain proof states (policy learning), and (2) learning the values corresponding to the same proof states (policy evaluation). The proposed algorithm is using no domain engineering. The authors evaluate their proposal on two datasets: Miz40 and M2k. The evaluation shows the proposed solution outperforms state-of-the are by solving 40% more problems.