MathForm-8B is an autoformalization model that translates natural-language mathematical statements into Lean 4. It is released with the paper MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement.
The model is trained on FormalVerse through supervised fine-tuning followed by reinforcement learning using Lean compilation and semantic-consistency feedback.
Figure 1: Overview of the MathForm data construction and training pipeline. The system combines Mathlib knowledge retrieval, compilation and semantic verification, and iterative refinement to generate reliable formal data, followed by trajectory reconstruction and training of MathForm-8B.
Figure 2: Pass@8 pass rates (%) under Syntax Check (SC) and Consistency Check (CC) for specialized autoformalizers on six benchmarks. AVG is the equally weighted macro-average across all six benchmarks. For each column, the best result is shown in bold and the second best is underlined.
import torch
from transformers import AutoModelForCausalLM, AutoTokenizer
model_id = "openbmb/MathForm-8B"
tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(
model_id, torch_dtype=torch.bfloat16, device_map="auto"
)
prompt = (
"Please convert the following informal math problem to a formal one in Lean 4 with a header. "
"Use the following theorem names: my_favorite_theorem.\n\n"
"Show that for every real number x, x^2 is non-negative."
)
messages = [{"role": "user", "content": prompt}]
text = tokenizer.apply_chat_template(messages, tokenize=False, add_generation_prompt=True)
inputs = tokenizer(text, return_tensors="pt").to(model.device)
outputs = model.generate(
**inputs, max_new_tokens=16384, temperature=0.6, top_p=0.95
)
print(tokenizer.decode(outputs[0][inputs.input_ids.shape[-1]:], skip_special_tokens=True))
The evaluation pipeline, benchmark files, and Pass@k scripts are available in the MathForm repository. Compilation checks require a running Kimina Lean Server. The experiments use Lean 4.21.0.
@misc{pu2026mathformscalingmathematicalautoformalization,
title={MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement},
author={Lushi Pu and Weiming Zhang and Xinheng Xie and Zixuan Fu and Bingxiang He and Hengyu Zhao and Hongya Lyu and Xin Li and Jie Zhou and Yudong Wang},
year={2026},
eprint={2608.14221},
archivePrefix={arXiv},
primaryClass={cs.AI},
url={https://arxiv.org/abs/2608.14221},
}
Files
20 files · 16.4 GBWeights 16.4 GB (safetensors). Sizes and sha256 from the signed manifest.
import os
os.environ["HF_ENDPOINT"] = "https://freeweights.allternit.com"
from transformers import AutoModelForCausalLM, AutoTokenizer
tok = AutoTokenizer.from_pretrained("openbmb/MathForm-8B", revision="8f6d09e66bd5821d985a2150ba3f09ba42e028ba")
model = AutoModelForCausalLM.from_pretrained("openbmb/MathForm-8B", revision="8f6d09e66bd5821d985a2150ba3f09ba42e028ba", device_map="auto")
