MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
**MathForm-8B** 是一个将自然语言数学陈述转换为 Lean 4 的自动形式化模型，随论文 *MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement* 发布。
该模型基于 [FormalVerse](https://huggingface.co/datasets/openbmb/FormalVerse) 训练，训练过程包括监督微调以及基于 Lean 编译和语义一致性反馈的强化学习。
图 1：MathForm 数据构造与训练流程概览。系统结合 Mathlib 知识检索、编译与语义验证以及迭代式优化，生成可靠的形式化数据，随后进行轨迹重构并训练 MathForm-8B。
## 结果
图 2：专用自动形式化模型在六个基准上的 Syntax Check（SC）和 Consistency Check（CC）Pass@8 通过率（%）。AVG 是六个基准等权重的宏平均。每一列中，最佳结果以粗体显示，次佳结果以下划线显示。
## 使用方法
### Transformers
```python
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))
```
### vLLM
```bash
vllm serve openbmb/MathForm-8B \
--served-model-name MathForm-8B \
--dtype bfloat16 \
--max-model-len 16384
```
### SGLang
```bash
python -m sglang.launch_server \
--model-path openbmb/MathForm-8B \
--served-model-name MathForm-8B \
--dtype bfloat16 \
--context-length 16384
```
两个服务均会在 `http://localhost:8000/v1/chat/completions` 提供兼容
OpenAI 的 API。
### 推荐参数
| 参数 | 值 |
| --- | --- |
| `temperature` | 0.6 |
| `top_p` | 0.95 |
| `max_new_tokens` | 16384 |
## 评测
评测流程、基准文件和 Pass@k 脚本位于 [MathForm 仓库](https://github.com/OpenBMB/MathForm)。编译检查需要运行 Kimina Lean Server。实验使用 Lean 4.21.0。
## 许可证
本项目采用 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},
}
```
