University of Cambridge > Talks.cam > CCIMI Seminars > Machine learning and theorem proving

Machine learning and theorem proving

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

  • UserHenryk Michalewski
  • ClockWednesday 20 November 2019, 14:00-15:00
  • HouseCMS, 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity