Neural theorem proving tutorial II

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]

Part I : Next-step suggestion

Builds a neural next-step suggestion tool, introducing concepts and past work in neural theorem proving along the way.

Notebooks:

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).

Artifacts:

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

Setup:

Please follow the setup instructions in partI_nextstep/README.md.

Part II : Language cascades

Chain together language models to guide formal proof search with informal proofs.

Notebooks:

Topic	Notebook
1. Language model cascades	notebook
2. Draft, Sketch, Prove	notebook

All notebooks are in (partII_dsp/notebooks).

Setup:

Please follow the setup instructions in partII_dsp/README.md.

---

History

This is an updated version of A tutorial on neural theorem proving (https://github.com/wellecks/ntptutorial).
Please see the repository for more details.

Citation

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}},
}