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

Emily First
UCSD

Albert Q. Jiang
Cambridge

Kaiyu Yang
Caltech

Panelists

Anima Anandkumar
Caltech, NVIDIA

Zhangir Azerbayev
Princeton

Noah Goodman
Stanford

Alex Sanchez-Stern
UMass Amherst

Dawn Song
UC Berkeley

Sean Welleck
UW, AI2 -> CMU

Materials and Open-Source Tools

• Video Recording
• Slides
• Demo: Using LLMs in Lean
• Demo: Training LLMs for Tactic Generation and Combining with Proof Search
• A Survey on Deep Learning for Theorem Proving

Lean

• LeanDojo: Extracting data and interacting with Lean
• ReProver: Training and evaluating language models for theorem proving
• LLMStep: Using language models to suggest proof steps
• Lean Copilot: Using language models to suggest proof steps, search for proofs, and select premises

Isabelle

• PISA: Extracting data and interacting with Isabelle
• Draft, Sketch, and Prove: Implementation of “Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs”

Coq

• CoqGym: Extracting data and interacting with Coq
• Tactician: KNNs and random forests + online learning for synthesizing proofs
• Proverbot9001: RNNs for synthesizing proofs.
• coq-synthesis: Coq plugin for using Proverbot9001 in the proof assistant

Others

• HOList: Extracting data and interacting with HOL Light
• INT: Synthetic theorem proving benchmark on inequalities

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.