8月24日，aibase消息显示，openbmb团队近期正式对外开源了面向数学自动形式化的全新框架、配套数据集及基础模型——mathform，聚焦攻克当前数学形式化领域中“代码可编译但语义失准”这一关键难题。
该框架首次融合检索增强与验证驱动的数据构建范式：检索规划器负责从Mathlib知识库中精准提取定义，并调用已有形式化模型作为参考；生成器则依托Lean编译器的实时诊断反馈与语义一致性评估结果，执行最多三轮迭代优化，从而确保生成代码在语法正确性与数学严谨性两方面高度统一。
在数据建设方面，OpenBMB发布了规模达36.7万+条已人工校验Lean4示例的FormalVerse数据集。实测表明，基于该数据集训练的模型在一致性检查任务中达成60.32%的通过率，明显高于FineLeanCorpus（46.53%）与NuminaMath-LEAN（41.49%）。
其主干模型MathForm-8B在六项权威基准测试中表现亮眼，语法检查通过率达88.06%，一致性检查通过率达72.37%；更值得注意的是，在仅使用四分之一参数量的前提下，该模型性能全面超越参数规模达32B的ReForm-32B。尤其在极具挑战性的FATE-H与FATE-X子集上，一致性检查成功率分别达到63%和37%，充分验证了其在复杂推理与形式化错误修正方面的突出能力。
☞☞☞AI 智能聊天, 问答助手, AI 智能搜索, 多模态理解力帮你轻松跨越从0到1的创作门槛☜☜☜
