GLM-5.3 is live. Run Z.ai's latest model on Friendli Model APIs. Try it today ➜
openbmb
Available on FriendliAI
Run this model inference on single tenant GPU with unmatched speed and reliability at scale.
Run this model inference with full control and performance in your environment.
Model Details
Model Provider
openbmb
Model Tree
Qwen/Qwen3-8B
Input Modalities
Output Modalities
Supported Functionality
python
import torchfrom transformers import AutoModelForCausalLM, AutoTokenizermodel_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))
bash
vllm serve openbmb/MathForm-8B \--served-model-name MathForm-8B \--dtype bfloat16 \--max-model-len 16384
bash
python -m sglang.launch_server \--model-path openbmb/MathForm-8B \--served-model-name MathForm-8B \--dtype bfloat16 \--context-length 16384
Both servers expose an OpenAI-compatible API at
http://localhost:8000/v1/chat/completions.
| Setting | Value |
|---|---|
temperature | 0.6 |
top_p | 0.95 |
max_new_tokens | 16384 |
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.
This project is licensed under the Apache License 2.0.
bibtex
@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},}