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:Formalisation of mathematics with interactive theo
rem provers
SUMMARY:Towards Autoformalization and Mathematical Reasoni
ng using language models - Professor Siddhartha Ga
dgil (Indian Institute of Science)
DTSTART;TZID=Europe/London:20240117T130000
DTEND;TZID=Europe/London:20240117T140000
UID:TALK210154AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/210154
DESCRIPTION:Language models have shown remarkable abilities: p
rocessing natural language\, analogical reasoning\
, even generating mathematical proofs. However\, t
he arguments they generate often have logical flaw
s\, and they are poor at judging correctness. It i
s thus natural to hope that pairing them with a fo
rmal proof system like Lean will be useful.\n\nIn
this talk we first discuss using Large Language Mo
dels (LLMs) to generate Lean code from natural lan
guage statements. We then discuss extending this t
o more complex tasks using intertwined informal an
d formal mathematics using LLMs and the Lean prove
r. The latter part will be informal and will consi
st for the most part of examples of uses of langua
ge models and their limitations.\n\n—-\n\nWATCH ON
LINE HERE : https://www.microsoft.com/en-gb/micros
oft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771
279 261 Passcode: iCo7a5
LOCATION:MR14 Centre for Mathematical Sciences
CONTACT:Anand Rao Tadipatri
END:VEVENT
END:VCALENDAR