from transformers import AutoModelForCausalLM, AutoTokenizer
model = AutoModelForCausalLM.from_pretrained("awhecmu/have-prover-haveDraft11")
tokenizer = AutoTokenizer.from_pretrained("awhecmu/have-prover-haveDraft11")
state = """α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)"""
# Tactic generation
sep = ":::"
prompt = state + sep
inputs = tokenizer(prompt, return_tensors="pt", add_special_tokens=False)
outputs = model.generate(**inputs, temperature=1.0, max_new_tokens=300)
tactic = tokenizer.decode(outputs[0], skip_special_tokens=False).split(sep)[1]
print(tactic)
Output
have rw: a \ (b ⊔ c) ⊔ b \ (a ⊔ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) := by sorry
<|endoftext|>
This is the model card of a 🤗 transformers model that has been pushed on the Hub. This model card has been automatically generated.
Developed by: [More Information Needed]
Funded by [optional]: [More Information Needed]
Shared by [optional]: [More Information Needed]
Model type: [More Information Needed]
Language(s) (NLP): [More Information Needed]
License: [More Information Needed]
Finetuned from model [optional]: [More Information Needed]
Model Sources [optional]
Repository: [More Information Needed]
Paper [optional]: [More Information Needed]
Demo [optional]: [More Information Needed]
Uses
Direct Use
[More Information Needed]
Downstream Use [optional]
[More Information Needed]
Out-of-Scope Use
[More Information Needed]
Bias, Risks, and Limitations
[More Information Needed]
Recommendations
Users (both direct and downstream) should be made aware of the risks, biases and limitations of the model. More information needed for further recommendations.
