Learning Theorem Proving from Scratch

Learning Theorem Proving from Scratch

Cezary Kaliszyk

University of Innsbruck

2019/02/26 (Tue) 14:30 to 15:30
I-56 (Collaboration Room 7) on 5F of IS Building III at JAIST
Logic Unit

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.

Nao Hirokawa