BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:CCIMI Seminars
SUMMARY:Machine learning and theorem proving - Henryk Mich
alewski
DTSTART;TZID=Europe/London:20191120T140000
DTEND;TZID=Europe/London:20191120T150000
UID:TALK127957AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/127957
DESCRIPTION:In my talk I will describe how theorem proving can
be phrased as a\nreinforcement learning problem a
nd provide experimental results with\nregard to va
rious datasets consisting of mathematical problems
ranging\nfrom SAT problems to simple arithmetic p
roblems involving addition and\nmultiplication\, t
o theorem proving inspired by simplifications and\
nrewritings of SQL queries and finally to general
mathematical problems\nsuch as included in the Miz
ar Mathematical library\nhttps://en.wikipedia.org/
wiki/Mizar_system. The talk will cover in\nparticu
lar the following topics:\n\n- two reinforcement l
earning algorithms designed for theorem proving\;\
none of them presented at NeurIPS 2018 in the pape
r "Reinforcement\nlearning of Theorem Proving"\n(h
ttps://papers.nips.cc/paper/8098-reinforcement-lea
rning-of-theorem-proving.pdf)\nruns Monte-Carlo si
mulations guided by policy and value functions\ngr
adually updated using previous proof attempts. The
other algorithm\nis based on curriculum learning
and is described in the paper "Towards\nFinding Lo
nger Proofs" (https://arxiv.org/abs/1905.13100\, p
roject\nwebpage: https://sites.google.com/view/atp
curr). It complements the\nMonte Carlo method in t
wo respects: it may be deployed to solve just\none
mathematical problem and overall it is capable to
produce longer\nproofs.\n\n- a graph network arch
itecture which includes sigmoidal attention\n(http
s://rlgm.github.io/papers/32.pdf) with an empirica
l study which\nshows that this kind of graph repre
sentation helps neural guidance of\nSAT solving al
gorithms.\n\n- I will show how rewriting of SQL qu
eries can be phrased as a theorem\nproving problem
\, explain why reinforcement learning is a suitabl
e\nframework for optimization of queries and prese
nt initial experimental\nresults obtained with Mic
hael Benedikt and Cezary Kaliszyk.
LOCATION:CMS\, MR14
CONTACT:Hamza Fawzi
END:VEVENT
END:VCALENDAR