Neural theorem proving combines neural language models with formal proof assistants.
This tutorial introduces two research threads in neural theorem proving via interactive Jupyter notebooks.
This is an updated version of https://github.com/wellecks/ntptutorial.
[slides]
Builds a neural next-step suggestion tool, introducing concepts and past work in neural theorem proving along the way.
| Topic | Notebook |
|---|---|
| 0. Intro | notebook |
| 1. Data | notebook |
| 2. Learning | notebook |
| 3. Proof Search | notebook |
| 4. Evaluation | notebook |
| 5. Context | notebook |
6. LLMLean tool |
notebook |
All notebooks are in (partI_nextstep/notebooks).
| Name | Huggingface |
|---|---|
| Data: mathlib extractions | l3lab/ntp-mathlib |
| Data: instructions (state-tactic) | l3lab/ntp-mathlib-instruct-st |
| Data: instructions (+context) | l3lab/ntp-mathlib-instruct-ctx |
| Model: state-tactic | l3lab/ntp-mathlib-st-deepseek-coder-1.3b |
| Model: +context | l3lab/ntp-mathlib-context-deepseek-coder-1.3b |
Please follow the setup instructions in partI_nextstep/README.md.
Chain together language models to guide formal proof search with informal proofs.
| Topic | Notebook |
|---|---|
| 1. Language model cascades | notebook |
| 2. Draft, Sketch, Prove | notebook |
All notebooks are in (partII_dsp/notebooks).
Please follow the setup instructions in partII_dsp/README.md.
This is an updated version of A tutorial on neural theorem proving (https://github.com/wellecks/ntptutorial).
Please see the repository for more details.
Until there is an associated preprint, please cite this repository:
@misc{ntptutorial,
author = {Sean Welleck},
title = {Neural theorem proving tutorial II},
year = {2023},
publisher = {GitHub},
journal = {GitHub repository},
howpublished = {\url{https://github.com/cmu-l3/ntptutorial-II}},
}