67 lines
2.4 KiB
Markdown
67 lines
2.4 KiB
Markdown
|
---
|
||
|
|
license: apache-2.0
|
||
|
|
base_model:
|
||
|
|
- Qwen/Qwen3-8B
|
||
|
|
---
|
||
|
|
This is the formalizer for translating infromal math problem into formal statement in Lean 4. In Goedel-Prover-V2 project we use this formalizer in generating lean4 statements.
|
||
|
|
Different from all previous open-source formalizers, this formalizer has the ability to think before generating the lean4 statements, which significantly increases the acurracy of the translation.
|
||
|
|
In our internal evaluation, we test the performance of formalizers on a eval set containing 300 informal statements from Omni-MATH. Kimina-formalizer-8B successfully translates 161/300 statements, while Goedel-Formalizer-V2-32B success in 228 statements.
|
||
|
|
|
||
|
|
Here is an example code to use this formalizer:
|
||
|
|
|
||
|
|
```
|
||
|
|
from transformers import AutoModelForCausalLM, AutoTokenizer
|
||
|
|
import torch
|
||
|
|
import re
|
||
|
|
torch.manual_seed(30)
|
||
|
|
|
||
|
|
model_id = "Goedel-LM/Goedel-Formalizer-V2-8B"
|
||
|
|
tokenizer = AutoTokenizer.from_pretrained(model_id)
|
||
|
|
model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True)
|
||
|
|
|
||
|
|
|
||
|
|
problem_name = "test_problem"
|
||
|
|
informal_statement_content = "Prove that 3 cannot be written as the sum of two cubes."
|
||
|
|
|
||
|
|
|
||
|
|
# Construct the prompt for the model
|
||
|
|
user_prompt_content = (
|
||
|
|
f"Please autoformalize the following natural language problem statement in Lean 4. "
|
||
|
|
f"Use the following theorem name: {problem_name}\n"
|
||
|
|
f"The natural language statement is: \n"
|
||
|
|
f"{informal_statement_content}"
|
||
|
|
f"Think before you provide the lean statement."
|
||
|
|
)
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
chat = [
|
||
|
|
{"role": "user", "content": user_prompt_content},
|
||
|
|
]
|
||
|
|
|
||
|
|
inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device)
|
||
|
|
|
||
|
|
import time
|
||
|
|
start = time.time()
|
||
|
|
outputs = model.generate(inputs, max_new_tokens=16384, temperature = 0.9, do_sample = True, top_k=20, top_p=0.95)
|
||
|
|
|
||
|
|
|
||
|
|
model_output_text = tokenizer.batch_decode(outputs)[0]
|
||
|
|
|
||
|
|
def extract_code(text_input):
|
||
|
|
"""Extracts the last Lean 4 code block from the model's output."""
|
||
|
|
try:
|
||
|
|
matches = re.findall(r'```lean4\n(.*?)\n```', text_input, re.DOTALL)
|
||
|
|
return matches[-1].strip() if matches else "No Lean 4 code block found."
|
||
|
|
except Exception:
|
||
|
|
return "Error during code extraction."
|
||
|
|
|
||
|
|
|
||
|
|
extracted_code = extract_code(model_output_text)
|
||
|
|
|
||
|
|
print(time.time() - start)
|
||
|
|
print("output:\n", model_output_text)
|
||
|
|
print("lean4 statement:\n", extracted_code)
|
||
|
|
|
||
|
|
|
||
|
|
```
|