Download as iCal file

Special Seminar

Advancing Theorem Proving with AI: The Power of Large Language Models

Amitayush Thakur

Location:  Zoom:
Date & time: Friday, 23 February 2024 at 4:00PM - 5:00PM

Abstract: This presentation explores the dynamic fusion of language models with the field of automated theorem proving, stretching across both general mathematics and software verification landscapes. It highlights the transformative potential of large language models (LLMs) to redefine formal mathematics, by framing theorem proving as a nuanced task of sequence generation. We will dive into the latest breakthroughs, showcasing projects like GPT-f, PACT, DSP, ReProver, and AlphaGeometry. A special focus will be placed on COPRA, an innovative methodology that empowers LLMs to autonomously craft formal proofs, leveraging the subtleties of in-context learning without needing domain-specific training. This discussion underscores the crucial synergy between LLMs and interactive theorem provers (ITPs), setting the stage for new approaches that involve close interactions between ITPs and LLMs.