BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Towards Autoformalization and Mathematical Reasoning using languag
 e models - Professor Siddhartha Gadgil (Indian Institute of Science)
DTSTART:20240117T130000Z
DTEND:20240117T140000Z
UID:TALK210154@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:Language models have shown remarkable abilities: processing na
 tural language\, analogical reasoning\, even generating mathematical proof
 s. However\, the arguments they generate often have logical flaws\, and th
 ey are poor at judging correctness. It is thus natural to hope that pairin
 g them with a formal proof system like Lean will be useful.\n\nIn this tal
 k we first discuss using Large Language Models (LLMs) to generate Lean cod
 e from natural language statements. We then discuss extending this to more
  complex tasks using intertwined informal and formal mathematics using LLM
 s and the Lean prover. The latter part will be informal and will consist f
 or the most part of examples of uses of language models and their limitati
 ons.\n\n—-\n\nWATCH ONLINE HERE : https://www.microsoft.com/en-gb/micros
 oft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a
 5
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR