MathForm-8B

MathForm-8B 是一个自动形式化模型，可将自然语言数学命题转换为 Lean 4 代码。该模型随论文 MathForm：通过知识检索与验证引导的优化实现数学自动形式化规模化 一同发布。

该模型基于 FormalVerse 数据集，通过监督微调，并利用 Lean 编译和语义一致性反馈进行强化学习训练而成。

结果

使用方法

Transformers

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

vllm serve openbmb/MathForm-8B \
  --served-model-name MathForm-8B \
  --dtype bfloat16 \
  --max-model-len 16384

SGLang

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。

推荐设置

评估

评估流程、基准文件和 Pass@k 脚本可在 MathForm 仓库 中获取。编译检查需要运行中的 Kimina Lean Server。实验使用 Lean 4.21.0。

许可证

本项目采用 Apache License 2.0 许可证。

引用

@misc{pu2026mathform,
  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}
}