品玩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%一致性检查通过率，以四分之一参数体量反超ReForm-32B等更大模型，在高难度FATE-H和FATE-X子集中一致性检查成功率分别达63%和37%，展现出较强的推理与形式化纠错能力。