Proving Theorems with Generative Language Models

Speaker(s): Ashwin Sreevatsa
Topic: Generative Language Modeling for Automated Theorem Proving Presentation

In the past decade, deep learning and artificial neural networks have been incredibly successful at a variety of tasks such as computer vision, translation, game playing, and robotics among others. However, there have been less examples of deep learning making progress with reasoning related tasks- such as automated theorem proving, the task of proving mathematical theorems using computer programs. This paper explores the use of transformer-based models to automated theorem proving and presents GPT-f, a deep learning-based automated prover and proof assistant.

Supplemental Resources

Papers:
Generative Language Modeling for Automated Theorem Proving Presentation