BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Machine learning and theorem proving - Henryk Michalewski
DTSTART:20191120T140000Z
DTEND:20191120T150000Z
UID:TALK127957@talks.cam.ac.uk
CONTACT:Hamza Fawzi
DESCRIPTION:In my talk I will describe how theorem proving can be phrased 
 as a\nreinforcement learning problem and provide experimental results with
 \nregard to various datasets consisting of mathematical problems ranging\n
 from SAT problems to simple arithmetic problems involving addition and\nmu
 ltiplication\, to theorem proving inspired by simplifications and\nrewriti
 ngs of SQL queries and finally to general mathematical problems\nsuch as i
 ncluded in the Mizar Mathematical library\nhttps://en.wikipedia.org/wiki/M
 izar_system. The talk will cover in\nparticular the following topics:\n\n-
  two reinforcement learning algorithms designed for theorem proving\;\none
  of them presented at NeurIPS 2018 in the paper "Reinforcement\nlearning o
 f Theorem Proving"\n(https://papers.nips.cc/paper/8098-reinforcement-learn
 ing-of-theorem-proving.pdf)\nruns Monte-Carlo simulations guided by policy
  and value functions\ngradually updated using previous proof attempts. The
  other algorithm\nis based on curriculum learning and is described in the 
 paper "Towards\nFinding Longer Proofs" (https://arxiv.org/abs/1905.13100\,
  project\nwebpage: https://sites.google.com/view/atpcurr). It complements 
 the\nMonte Carlo method in two respects: it may be deployed to solve just\
 none mathematical problem and overall it is capable to produce longer\npro
 ofs.\n\n- a graph network architecture which includes sigmoidal attention\
 n(https://rlgm.github.io/papers/32.pdf) with an empirical study which\nsho
 ws that this kind of graph representation helps neural guidance of\nSAT so
 lving algorithms.\n\n- I will show how rewriting of SQL queries can be phr
 ased as a theorem\nproving problem\, explain why reinforcement learning is
  a suitable\nframework for optimization of queries and present initial exp
 erimental\nresults obtained with Michael Benedikt and Cezary Kaliszyk.
LOCATION:CMS\, MR14
END:VEVENT
END:VCALENDAR