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:Artificial Intelligence Research Group Talks (Comp
uter Laboratory)
SUMMARY:Draft\, Sketch\, and Prove: Guiding Formal Theorem
Provers with Informal Proofs - Albert Qiaochu Jia
ng (University of Cambridge)
DTSTART;TZID=Europe/London:20221115T130000
DTEND;TZID=Europe/London:20221115T140000
UID:TALK183461AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/183461
DESCRIPTION:Join us in Lecture Theatre 2 or on "Zoom":https://
zoom.us/j/99166955895?pwd=SzI0M3pMVEkvNmw3Q0dqNDVR
alZvdz09\n\nThe formalization of existing mathemat
ical proofs is a notoriously difficult process. De
spite decades of research on automation and proof
assistants\, writing formal proofs remains arduous
and only accessible to a few experts.\nWhile prev
ious studies to automate formalization focused on
powerful search algorithms\, no\nattempts were mad
e to take advantage of available informal proofs.\
nIn this work\, we introduce _Draft\, Sketch\, and
Prove (DSP)_\, a method that \nmaps informal proo
fs to formal proof sketches\, and uses the sketche
s to guide an automated prover by directing its se
arch to easier sub-problems.\nWe investigate two r
elevant setups where informal proofs are either wr
itten by humans or generated by a language model.\
nOur experiments and ablation studies show that la
rge language models are able to produce well-struc
tured formal sketches that follow the same reasoni
ng steps as the informal proofs. Guiding an automa
ted prover with these sketches enhances its perfor
mance from 20.9% to 39.3% on a collection of mathe
matical competition problems.
LOCATION:Lecture Theatre 2 and Zoom
CONTACT:Mateja Jamnik
END:VEVENT
END:VCALENDAR