Färber, Michael, Kaliszyk, Cezary, Urban, Josef

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.

A new tableau-based calculus for first-order intuitionistic logic is proposed. The calculus is obtained from the tableau calculus for classical logic by extending its rules by A-terms. A-terms are seen as compact representation of natural deduction proofs. The benefits from that approach are twofold. First, proof search methods known for classical logic can be adopted: Run-time-Skolemization and unification.

Kaliszyk, Cezary, Urban, Josef, Michalewski, Henryk, Olšák, Mirek

We introduce a theorem proving algorithm that uses practically no domain heuristics for guiding its connection-style proof search. Instead, it runs many Monte-Carlo simulations guided by reinforcement learning from previous proof attempts. We produce several versions of the prover, parameterized by different learning and guiding algorithms. The strongest version of the system is trained on a large corpus of mathematical problems and evaluated on previously unseen problems. The trained system solves within the same number of inferences over 40% more problems than a baseline prover, which is an unusually high improvement in this hard AI domain. To our knowledge this is the first time reinforcement learning has been convincingly applied to solving general mathematical problems on a large scale.

Kaliszyk, Cezary, Urban, Josef, Michalewski, Henryk, Olšák, Miroslav

Kaliszyk, Cezary, Urban, Josef, Michalewski, Henryk, Olšák, Miroslav