File size: 894 Bytes
921d73a 5073d10 921d73a ce344c9 921d73a 8c3bd83 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 |
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-st](https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-st) for 3 epochs.
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}},
}
```
|