Goedel-Formalizer-V2-32B

This is the formalizer for translating informal 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 accuracy of the translation. The model is compatible with both Transformers and vLLM for inference.

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 are examples for using the model with both Transformers and vLLM:

Using with Transformers

from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
import re
torch.manual_seed(30)

model_id = "KellyJDavis/Goedel-Formalizer-V2-32B"
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)

# Extract only the generated tokens (skip the input prompt)
input_length = inputs.shape[1]
generated_tokens = outputs[0][input_length:]
model_output_text = tokenizer.decode(generated_tokens, skip_special_tokens=False)

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)

Using with vLLM

The model is now compatible with vLLM for faster inference:

from vllm import LLM, SamplingParams
from transformers import AutoTokenizer
import re

model_id = "KellyJDavis/Goedel-Formalizer-V2-32B"
tokenizer = AutoTokenizer.from_pretrained(model_id)

# Initialize vLLM
llm = LLM(model=model_id, dtype="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},
]

# Apply chat template
prompt = tokenizer.apply_chat_template(chat, tokenize=False, add_generation_prompt=True)

# Configure sampling parameters
sampling_params = SamplingParams(
    temperature=0.9,
    top_k=20,
    top_p=0.95,
    max_tokens=16384
)

# Generate
import time
start = time.time()
outputs = llm.generate([prompt], sampling_params)
model_output_text = outputs[0].outputs[0].text

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)