readme: ---
  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
  