|
--- |
|
license: apache-2.0 |
|
--- |
|
|
|
# GPT-NEO-Model for Lean Tactics |
|
|
|
|
|
In the project, we used an HuggingFace GPT-NEO small model and fine-tuned the tactic dataset. The Input should be of the form |
|
``` |
|
<GOAL> Goal <PROOFSTEP> |
|
``` |
|
|
|
The model can easily be accessed using the following code. |
|
|
|
``` |
|
from transformers import GPT2Tokenizer, GPTNeoForCausalLM |
|
import torch |
|
|
|
tokenizer = GPT2Tokenizer.from_pretrained("Saisam/gpt-neo-math-small") |
|
model = GPTNeoForCausalLM.from_pretrained("Saisam/gpt-neo-math-small") |
|
``` |
|
|
|
More Information can be found at https://github.com/saisurbehera/mathProof. |
|
|
|
The current model beats the GPT-F for minif2f benchmark |
|
|
|
Worked along with Xihao Xhang and Moya Zhu |
|
|
