Machine learning and theorem proving

Add to your list(s) Download to your calendar using vCal

• Henryk Michalewski
• Wednesday 20 November 2019, 14:00-15:00
• CMS, MR14.

If you have a question about this talk, please contact Hamza Fawzi.

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.

This talk is part of the CCIMI Seminars series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CCIMI
• CCIMI Seminars
• CMS Events
• CMS, MR14
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• DPMMS Lists
• DPMMS info aggregator
• DPMMS lists
• Guy Emerson's list
• Hanchen DaDaDash
• Interested Talks
• School of Physical Sciences
• Statistical Laboratory info aggregator
• Trust & Technology Initiative - interesting events
• bld31
• custom
• ndk22's list
• ob366-ai4er
• rp587

Note that ex-directory lists are not shown.