Abstract

In my talk I will describe how theorem proving can be phrased as a reinforcement learning problem and provide experimental results with regard to various datasets consisting of mathematical problems ranging from SAT problems to simple arithmetic problems involving addition and multiplication, to theorem proving inspired by simplifications and rewritings of SQL queries and finally to general mathematical problems such as included in the Mizar Mathematical library https://en.wikipedia.org/wiki/Mizar_system. The talk will cover in particular the following topics:

- two reinforcement learning algorithms designed for theorem proving; one of them presented at NeurIPS 2018 in the paper “Reinforcement learning of Theorem Proving” (https://papers.nips.cc/paper/8098-reinforcement-learning-of-theorem-proving.pdf) runs Monte-Carlo simulations guided by policy and value functions gradually updated using previous proof attempts. The other algorithm is based on curriculum learning and is described in the paper “Towards Finding Longer Proofs” (https://arxiv.org/abs/1905.13100, project webpage: https://sites.google.com/view/atpcurr). It complements the Monte Carlo method in two respects: it may be deployed to solve just one mathematical problem and overall it is capable to produce longer proofs.

- a graph network architecture which includes sigmoidal attention (https://rlgm.github.io/papers/32.pdf) with an empirical study which shows that this kind of graph representation helps neural guidance of SAT solving algorithms.

- I will show how rewriting of SQL queries can be phrased as a theorem proving problem, explain why reinforcement learning is a suitable framework for optimization of queries and present initial experimental results obtained with Michael Benedikt and Cezary Kaliszyk.