Towards Autoformalization and Mathematical Reasoning using language models

Add to your list(s) Download to your calendar using vCal

• Professor Siddhartha Gadgil (Indian Institute of Science)
• Wednesday 17 January 2024, 13:00-14:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

Note unusual time

Language models have shown remarkable abilities: processing natural language, analogical reasoning, even generating mathematical proofs. However, the arguments they generate often have logical flaws, and they are poor at judging correctness. It is thus natural to hope that pairing them with a formal proof system like Lean will be useful.

In this talk we first discuss using Large Language Models (LLMs) to generate Lean code from natural language statements. We then discuss extending this to more complex tasks using intertwined informal and formal mathematics using LLMs and the Lean prover. The latter part will be informal and will consist for the most part of examples of uses of language models and their limitations.

—-

WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.