Video Recording

Overview

Machine learning, especially large language models (LLMs), has shown promise in proving formal theorems using proof assistants such as Coq, Isabelle, and Lean. Theorem proving is an important challenge for machine learning: Formal proofs are computer programs whose correctness can be verified. Therefore, theorem proving is a form of code generation with rigorous evaluation and no room for the model to hallucinate, opening up a new avenue for addressing LLMs’ flaws in factuality.

Despite its potential, learning-based theorem proving has significant entry barriers, primarily due to the steep learning curve for proof assistants. This tutorial aims to bridge this gap and make theorem proving accessible to researchers with a general machine learning background. To that end, our presentation will contextualize theorem proving from a machine learning perspective and demonstrate how to develop LLMs for theorem proving, using newly available open-source tools that provides interfaces to proof assistants without requiring in-depth knowledge of their internals. Furthermore, we will cover advanced topics and open problems in learning-based theorem proving, including its synergies with natural language processing and software verification.

Throughout the presentation, we will highlight several conceptual themes recurring in theorem proving that are also critical for machine learning, such as mathematical reasoning, code generation, and hallucination prevention. The panel will complement the presentation through a broader discussion of related topics such as trustworthy machine learning, LLMs for code, reasoning, and program synthesis.


Presenters

Albert Q. Jiang
Albert Q. Jiang
Cambridge
Kaiyu Yang
Kaiyu Yang
Caltech

Panelists

Anima Anandkumar
Anima Anandkumar
Caltech, NVIDIA
Zhangir Azerbayev
Zhangir Azerbayev
Princeton
Noah Goodman
Noah Goodman
Stanford
Alex Sanchez-Stern
Alex Sanchez-Stern
UMass Amherst
Dawn Song
Dawn Song
UC Berkeley
Sean Welleck
Sean Welleck
UW, AI2 -> CMU

Materials and Open-Source Tools

Lean

Isabelle

Coq

Others

Citation

If you find this tutorial useful, please cite:

@misc{ml4tptutorial2023,
  author = {First, Emily and Jiang, Albert and Yang, Kaiyu},
  title = {{NeurIPS} Tutorial on Machine Learning for Theorem Proving},
  year = {2023},
  howpublished = {\url{https://machine-learning-for-theorem-proving.github.io}},
}

Contact: machine.learning.4.theorem.proving@gmail.com.