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