BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Draft\, Sketch\, and Prove: Guiding Formal Theorem Provers with In
 formal Proofs - Albert Qiaochu Jiang (University of Cambridge)
DTSTART:20221115T130000Z
DTEND:20221115T140000Z
UID:TALK183461@talks.cam.ac.uk
CONTACT:Mateja Jamnik
DESCRIPTION:Join us in Lecture Theatre 2 or on "Zoom":https://zoom.us/j/99
 166955895?pwd=SzI0M3pMVEkvNmw3Q0dqNDVRalZvdz09\n\nThe formalization of exi
 sting mathematical proofs is a notoriously difficult process. Despite deca
 des of research on automation and proof assistants\, writing formal proofs
  remains arduous and only accessible to a few experts.\nWhile previous stu
 dies to automate formalization focused on powerful search algorithms\, no\
 nattempts were made to take advantage of available informal proofs.\nIn th
 is work\, we introduce _Draft\, Sketch\, and Prove (DSP)_\, a method that 
 \nmaps informal proofs to formal proof sketches\, and uses the sketches to
  guide an automated prover by directing its search to easier sub-problems.
 \nWe investigate two relevant setups where informal proofs are either writ
 ten by humans or generated by a language model.\nOur experiments and ablat
 ion studies show that large language models are able to produce well-struc
 tured formal sketches that follow the same reasoning steps as the informal
  proofs. Guiding an automated prover with these sketches enhances its perf
 ormance from 20.9% to 39.3% on a collection of mathematical competition pr
 oblems.
LOCATION:Lecture Theatre 2 and Zoom
END:VEVENT
END:VCALENDAR