Text Generation
Transformers
Safetensors
English
qwen3
lean4
autoformalization
mathematics
formal-verification
reasoning
conversational
text-generation-inference
Instructions to use openbmb/MathForm-8B with libraries, inference providers, notebooks, and local apps. Follow these links to get started.
- Libraries
- Transformers
How to use openbmb/MathForm-8B with Transformers:
# Use a pipeline as a high-level helper from transformers import pipeline pipe = pipeline("text-generation", model="openbmb/MathForm-8B") messages = [ {"role": "user", "content": "Who are you?"}, ] pipe(messages)# Load model directly from transformers import AutoTokenizer, AutoModelForCausalLM tokenizer = AutoTokenizer.from_pretrained("openbmb/MathForm-8B") model = AutoModelForCausalLM.from_pretrained("openbmb/MathForm-8B", device_map="auto") messages = [ {"role": "user", "content": "Who are you?"}, ] inputs = tokenizer.apply_chat_template( messages, add_generation_prompt=True, tokenize=True, return_dict=True, return_tensors="pt", ).to(model.device) outputs = model.generate(**inputs, max_new_tokens=40) print(tokenizer.decode(outputs[0][inputs["input_ids"].shape[-1]:])) - Notebooks
- Google Colab
- Kaggle
- Local Apps Settings
- vLLM
How to use openbmb/MathForm-8B with vLLM:
Install from pip and serve model
# Install vLLM from pip: pip install vllm # Start the vLLM server: vllm serve "openbmb/MathForm-8B" # Call the server using curl (OpenAI-compatible API): curl -X POST "http://localhost:8000/v1/chat/completions" \ -H "Content-Type: application/json" \ --data '{ "model": "openbmb/MathForm-8B", "messages": [ { "role": "user", "content": "What is the capital of France?" } ] }'Use Docker
docker model run hf.co/openbmb/MathForm-8B
- SGLang
How to use openbmb/MathForm-8B with SGLang:
Install from pip and serve model
# Install SGLang from pip: pip install sglang # Start the SGLang server: python3 -m sglang.launch_server \ --model-path "openbmb/MathForm-8B" \ --host 0.0.0.0 \ --port 30000 # Call the server using curl (OpenAI-compatible API): curl -X POST "http://localhost:30000/v1/chat/completions" \ -H "Content-Type: application/json" \ --data '{ "model": "openbmb/MathForm-8B", "messages": [ { "role": "user", "content": "What is the capital of France?" } ] }'Use Docker images
docker run --gpus all \ --shm-size 32g \ -p 30000:30000 \ -v ~/.cache/huggingface:/root/.cache/huggingface \ --env "HF_TOKEN=<secret>" \ --ipc=host \ lmsysorg/sglang:latest \ python3 -m sglang.launch_server \ --model-path "openbmb/MathForm-8B" \ --host 0.0.0.0 \ --port 30000 # Call the server using curl (OpenAI-compatible API): curl -X POST "http://localhost:30000/v1/chat/completions" \ -H "Content-Type: application/json" \ --data '{ "model": "openbmb/MathForm-8B", "messages": [ { "role": "user", "content": "What is the capital of France?" } ] }' - Docker Model Runner
How to use openbmb/MathForm-8B with Docker Model Runner:
docker model run hf.co/openbmb/MathForm-8B
update readme (#1)
Browse files- update readme: add arXiv and GitHub links, update citation (3d1732038a9f32cd64ee839290db3a36993c1e6e)
- link paper: add arxiv:2608.14221 tag (1f708d57063faf5a3a7da67eb70f53eb6a6e2bb2)
- fix rendering: force inline-block for badges (c0fbfac8e293dc5128e6d61edebb9bbf3d86ef26)
Co-authored-by: Lushi Pu <daypu@users.noreply.huggingface.co>
- README.md +15 -10
- README_zh.md +14 -10
README.md
CHANGED
|
@@ -9,6 +9,7 @@ datasets:
|
|
| 9 |
pipeline_tag: text-generation
|
| 10 |
library_name: transformers
|
| 11 |
tags:
|
|
|
|
| 12 |
- lean4
|
| 13 |
- autoformalization
|
| 14 |
- mathematics
|
|
@@ -20,11 +21,11 @@ tags:
|
|
| 20 |
<h1>MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement</h1>
|
| 21 |
</div>
|
| 22 |
|
| 23 |
-
<
|
| 24 |
-
<img src="https://img.shields.io/badge/Paper-arXiv-b31b1b.svg" alt="Paper">
|
| 25 |
-
<a href="
|
| 26 |
-
<a href="https://huggingface.co/datasets/openbmb/FormalVerse"><img src="https://img.shields.io/badge/
|
| 27 |
-
</
|
| 28 |
|
| 29 |
**MathForm-8B** is an autoformalization model that translates natural-language
|
| 30 |
mathematical statements into Lean 4. It is released with the paper *MathForm:
|
|
@@ -112,7 +113,7 @@ Both servers expose an OpenAI-compatible API at
|
|
| 112 |
## Evaluation
|
| 113 |
|
| 114 |
The evaluation pipeline, benchmark files, and Pass@k scripts are available in
|
| 115 |
-
the [MathForm repository](
|
| 116 |
Kimina Lean Server. The experiments use Lean 4.21.0.
|
| 117 |
|
| 118 |
## License
|
|
@@ -122,9 +123,13 @@ This project is licensed under the Apache License 2.0.
|
|
| 122 |
## Citation
|
| 123 |
|
| 124 |
```bibtex
|
| 125 |
-
@misc{
|
| 126 |
-
|
| 127 |
-
|
| 128 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
| 129 |
}
|
| 130 |
```
|
|
|
|
| 9 |
pipeline_tag: text-generation
|
| 10 |
library_name: transformers
|
| 11 |
tags:
|
| 12 |
+
- arxiv:2608.14221
|
| 13 |
- lean4
|
| 14 |
- autoformalization
|
| 15 |
- mathematics
|
|
|
|
| 21 |
<h1>MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement</h1>
|
| 22 |
</div>
|
| 23 |
|
| 24 |
+
<div align="center" style="line-height: 1;">
|
| 25 |
+
<a href="https://arxiv.org/abs/2608.14221" style="margin: 2px;"><img src="https://img.shields.io/badge/Paper-arXiv-b31b1b.svg" alt="Paper" style="display: inline-block; vertical-align: middle;" /></a>
|
| 26 |
+
<a href="https://github.com/OpenBMB/MathForm" style="margin: 2px;"><img src="https://img.shields.io/badge/GitHub-MathForm-181717.svg" alt="Code" style="display: inline-block; vertical-align: middle;" /></a>
|
| 27 |
+
<a href="https://huggingface.co/datasets/openbmb/FormalVerse" style="margin: 2px;"><img src="https://img.shields.io/badge/%F0%9F%A4%97%20Dataset-FormalVerse-yellow.svg" alt="FormalVerse Dataset" style="display: inline-block; vertical-align: middle;" /></a>
|
| 28 |
+
</div>
|
| 29 |
|
| 30 |
**MathForm-8B** is an autoformalization model that translates natural-language
|
| 31 |
mathematical statements into Lean 4. It is released with the paper *MathForm:
|
|
|
|
| 113 |
## Evaluation
|
| 114 |
|
| 115 |
The evaluation pipeline, benchmark files, and Pass@k scripts are available in
|
| 116 |
+
the [MathForm repository](https://github.com/OpenBMB/MathForm). Compilation checks require a running
|
| 117 |
Kimina Lean Server. The experiments use Lean 4.21.0.
|
| 118 |
|
| 119 |
## License
|
|
|
|
| 123 |
## Citation
|
| 124 |
|
| 125 |
```bibtex
|
| 126 |
+
@misc{pu2026mathformscalingmathematicalautoformalization,
|
| 127 |
+
title={MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement},
|
| 128 |
+
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},
|
| 129 |
+
year={2026},
|
| 130 |
+
eprint={2608.14221},
|
| 131 |
+
archivePrefix={arXiv},
|
| 132 |
+
primaryClass={cs.AI},
|
| 133 |
+
url={https://arxiv.org/abs/2608.14221},
|
| 134 |
}
|
| 135 |
```
|
README_zh.md
CHANGED
|
@@ -2,11 +2,11 @@
|
|
| 2 |
<h1>MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement</h1>
|
| 3 |
</div>
|
| 4 |
|
| 5 |
-
<
|
| 6 |
-
<img src="https://img.shields.io/badge/Paper-arXiv-b31b1b.svg" alt="论文">
|
| 7 |
-
<a href="
|
| 8 |
-
<a href="https://huggingface.co/datasets/openbmb/FormalVerse"><img src="https://img.shields.io/badge/
|
| 9 |
-
</
|
| 10 |
|
| 11 |
**MathForm-8B** 是一个将自然语言数学陈述转换为 Lean 4 的自动形式化模型,随论文 *MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement* 发布。
|
| 12 |
|
|
@@ -88,7 +88,7 @@ OpenAI 的 API。
|
|
| 88 |
|
| 89 |
## 评测
|
| 90 |
|
| 91 |
-
评测流程、基准文件和 Pass@k 脚本位于 [MathForm 仓库](
|
| 92 |
|
| 93 |
## 许可证
|
| 94 |
|
|
@@ -97,9 +97,13 @@ OpenAI 的 API。
|
|
| 97 |
## 引用
|
| 98 |
|
| 99 |
```bibtex
|
| 100 |
-
@misc{
|
| 101 |
-
|
| 102 |
-
|
| 103 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
| 104 |
}
|
| 105 |
```
|
|
|
|
| 2 |
<h1>MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement</h1>
|
| 3 |
</div>
|
| 4 |
|
| 5 |
+
<div align="center" style="line-height: 1;">
|
| 6 |
+
<a href="https://arxiv.org/abs/2608.14221" style="margin: 2px;"><img src="https://img.shields.io/badge/Paper-arXiv-b31b1b.svg" alt="论文" style="display: inline-block; vertical-align: middle;" /></a>
|
| 7 |
+
<a href="https://github.com/OpenBMB/MathForm" style="margin: 2px;"><img src="https://img.shields.io/badge/GitHub-MathForm-181717.svg" alt="代码" style="display: inline-block; vertical-align: middle;" /></a>
|
| 8 |
+
<a href="https://huggingface.co/datasets/openbmb/FormalVerse" style="margin: 2px;"><img src="https://img.shields.io/badge/%F0%9F%A4%97%20Dataset-FormalVerse-yellow.svg" alt="FormalVerse 数据集" style="display: inline-block; vertical-align: middle;" /></a>
|
| 9 |
+
</div>
|
| 10 |
|
| 11 |
**MathForm-8B** 是一个将自然语言数学陈述转换为 Lean 4 的自动形式化模型,随论文 *MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement* 发布。
|
| 12 |
|
|
|
|
| 88 |
|
| 89 |
## 评测
|
| 90 |
|
| 91 |
+
评测流程、基准文件和 Pass@k 脚本位于 [MathForm 仓库](https://github.com/OpenBMB/MathForm)。编译检查需要运行 Kimina Lean Server。实验使用 Lean 4.21.0。
|
| 92 |
|
| 93 |
## 许可证
|
| 94 |
|
|
|
|
| 97 |
## 引用
|
| 98 |
|
| 99 |
```bibtex
|
| 100 |
+
@misc{pu2026mathformscalingmathematicalautoformalization,
|
| 101 |
+
title={MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement},
|
| 102 |
+
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},
|
| 103 |
+
year={2026},
|
| 104 |
+
eprint={2608.14221},
|
| 105 |
+
archivePrefix={arXiv},
|
| 106 |
+
primaryClass={cs.AI},
|
| 107 |
+
url={https://arxiv.org/abs/2608.14221},
|
| 108 |
}
|
| 109 |
```
|