README_zh.md

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 训练，训练过程包括监督微调以及基于 Lean 编译和语义一致性反馈的强化学习。

图 1：MathForm 数据构造与训练流程概览。系统结合 Mathlib 知识检索、编译与语义验证以及迭代式优化，生成可靠的形式化数据，随后进行轨迹重构并训练 MathForm-8B。

结果

图 2：专用自动形式化模型在六个基准上的 Syntax Check（SC）和 Consistency Check（CC）Pass@8 通过率（%）。AVG 是六个基准等权重的宏平均。每一列中，最佳结果以粗体显示，次佳结果以下划线显示。

使用方法

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。

推荐参数

参数	值
temperature	0.6
top_p	0.95
max_new_tokens	16384

评测

评测流程、基准文件和 Pass@k 脚本位于 MathForm 仓库。编译检查需要运行 Kimina Lean Server。实验使用 Lean 4.21.0。

许可证

本项目采用 Apache License 2.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}, 
}