## Machine learning and theorem proving

### With Henryk Michalewski

# 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.