Machine learning and theorem proving

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.

• Speaker: Henryk Michalewski
• Wednesday 20 November 2019, 14:00–15:00
• Venue: CMS, MR14.
• Series: CCIMI Seminars; organiser: Hamza Fawzi.