OpenBMB 团队近日发布 MathForm-8B，一个专门用于数学自动形式化的 8B 参数模型，能够将自然语言描述的数学命题转换为 Lean 4 形式化代码。该模型基于 Qwen3-8B 底座，采用 Apache 2.0 许可开源，并随附论文《MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement》。

MathForm-8B 的训练数据来自团队构建的 FormalVerse 数据集，训练流程分为两个阶段：先进行监督微调，再通过强化学习优化，其中强化学习的奖励信号来自 Lean 编译检查和语义一致性反馈。这种“验证引导”的机制旨在减少形式化过程中的错误，提高生成代码的可靠性。

在技术架构上，MathForm 系统整合了 Mathlib 知识检索、编译与语义验证，以及迭代精炼三个环节，以生成高质量的形式化数据，随后通过轨迹重建训练出 MathForm-8B。论文报告了模型在六个基准上的 Pass@8 通过率（分别经过语法检查和一致性检查），并给出了平均成绩，但摘要中未列出具体数值。

模型的使用方式较为灵活，支持 Transformers、vLLM 和 SGLang 三种推理框架，并可通过 OpenAI 兼容 API 调用。官方推荐设置温度为 0.6、top_p 为 0.95，最大生成长度为 16384 token。评估代码、基准文件和脚本均已公开在 MathForm 仓库中，编译检查依赖 Kimina Lean Server，实验基于 Lean 4.21.0。

从产业角度看，MathForm-8B 的发布是自动形式化领域的一次开源尝试，其“检索+验证”的范式可能为 AI 在数学推理、定理证明乃至安全关键代码生成方面提供新思路。对于关注 AI 模型应用层的投资者而言，这类模型展示了将大语言模型与形式验证工具结合的可能性，或可推动 AI 在科研、教育等场景的落地，但当前仍处于研究阶段，实际应用效果有待观察。