| Model from the [neural theorem proving tutorial vII](https://github.com/cmu-l3/ntptutorial-II). | |
| A deepseek-coder 1.3B model finetuned on [ntp-mathlib-instruct-context](https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-context). | |
| It is specifically finetuned for Lean 4 tactic prediction given proof states and optional file contexts. See the tutorial for code and more information. | |
| #### Performance | |
| The model achieves 29.5% (72/244) on Lean 4 MiniF2F using the standard search setting (best-first search with beam search expansions and a beam size of 32). | |
| #### Citation | |
| Until an associated preprint is available, please cite the tutorial's repository: | |
| ``` | |
| @misc{ntptutorialII, | |
| author = {Sean Welleck}, | |
| title = {Neural theorem proving tutorial II}, | |
| year = {2024}, | |
| publisher = {GitHub}, | |
| journal = {GitHub repository}, | |
| howpublished = {\url{https://github.com/cmu-l3/ntptutorial-II}}, | |
| } | |
| ``` | |