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
Panelists
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
- CoqPyt: Interacting with Coq
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.