File size: 587 Bytes
921d73a |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
### Neural theorem proving (`ntp`) `mathlib-tactic-instruct`
Model from the [neural theorem proving tutorial vII]().
A deepseek-coder 1.3B model finetuned on [ntp-mathlib-tactic-instruct](https://huggingface.co/datasets/wellecks/ntp-lean-mathlib-tactic-instruct) 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).
|