l3lab/ntp-mathlib-st-deepseek-coder-1.3b

Model from the neural theorem proving tutorial vII.

A deepseek-coder 1.3B model finetuned on ntp-mathlib-instruct-st.

It is specifically finetuned for Lean 4 tactic prediction given proof states. See the tutorial for code and more information.

Performance

The model achieves 29.1% (71/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}},
}