#AI
面壁开源 MathForm 8B，形式化压过 32B
面壁智能与清华 NLP 实验室支持的 OpenBMB 团队把数学自动形式化方案 MathForm 整体开源：8B 模型权重、约 36.7 万条验证过的 Lean 4 数据集 FormalVerse,外加评测代码与 Pass@k 脚本一并放出，Apache 2.0 许可，基座是 Qwen3-8B。
这套方案的核心不是堆参数，而是把 Mathlib 检索（LeanExplore 工具）加编译器反馈迭代做进流水线。结果 MathForm-8B 在最难的 FATE X 上拿到 37% 一致性通过率，越过多款 32B 专用形式化模型。BF16 下 8B 只需约 16GB 显存，单张消费级显卡就能跑，形式化验证的门槛从集群落到单机。
💡 为什么值得看8B 模型靠检索 Mathlib 击败 32B 对手，单卡可跑。
查证
来源档案
CocoLoop（中文科技媒体）
中文科技行业媒体综述稿，聚合 OpenBMB 项目仓库、arXiv 预印本与 Hugging Face 数据页信息，并标注了核验口径
单源二手综述，tier-2,但文内给出具体数字与引用出处，可信度中等；关键结论（37% 通过率、36.7 万样本、许可证）尚未见官方一手渠道独立确认，建议以单源线索看待
延伸阅读
文章论证了为什幺检索 Mathlib 让 8B 能与 32B 掰手腕，对理解形式化模型的差异化路线有价值