BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:POSTPONED till next week!!!! Work in progress: Making efficient us
 e of language models for theorem proving - Albert Qiaochu Jiang (Universit
 y of Cambridge)
DTSTART:20220222T131500Z
DTEND:20220222T141500Z
UID:TALK168419@talks.cam.ac.uk
CONTACT:Mateja Jamnik
DESCRIPTION:"Join us on Zoom":https://zoom.us/j/99166955895?pwd=SzI0M3pMVE
 kvNmw3Q0dqNDVRalZvdz09\n\nLanguage models are neural networks trained on b
 road data and adaptable to a wide range of downstream tasks. They have sho
 wn impressive capabilities in domains such as NLP\, vision\, robotics\, an
 d reasoning. For mathematical reasoning\, several SOTA results have been a
 chieved by language models\, but the huge computational cost prevents them
  from a wider adoption in the formal mathematics community. We introduce t
 wo methods to make efficient use of language models for theorem proving - 
 one based on augmenting the language model prompt with previous proof step
 s and the other based on sampling output candidates of larger quantity and
  diversity. Our model improved the state-of-the-art theorem proving succes
 s rate on the Archive of Formal Proofs from 33.2% to 39.6%\, without incur
 ring any further computational cost.
LOCATION:Zoom
END:VEVENT
END:VCALENDAR