University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Towards Autoformalization and Mathematical Reasoning using language models

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Towards Autoformalization and Mathematical Reasoning using language models

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Stephenson Seminar Room, Hopkins Building, Downing Site Webinar & GN06, Computer Laboratory, William Gates Building. rc781

Other talks

LCLU Annual Talk: The Early Aqueous Environment of Mars Inferred From Mission Lifetime Results by the Curiosity Rover at Gale Crater The rise of local cartography in Europe, 12th-14th century Tea and Coffee Break Task performance predicts the substitution of feedforward by feedback drive in visual cortex Tea and Coffee Break Polar Oceans Seminar Talk
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity