Learning Theorem Proving from Scratch

• Cezary Kaliszyk

• University of Innsbruck

• homepage

Machine learning can in some domains find algorithms that are better than human heuristics. In this talk we will look at various theorem proving problems and their heuristics, and see which of those can be replaces by machine learned strategies. Instead of typical brute-force search, we will consider Monte-Carlo simulations guided by reinforcement learning from previous proof attempts. Various predictors for estimating the usefulness of proof steps and the likelihood of closing the open tableaux branches will be compared.