metadata

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