OpenBMB 开源数学自动形式化框架 MathForm

OpenBMB 团队开源数学自动形式化框架、数据集与模型 MathForm，以解决数学形式化中代码可编译但语义不准确的痛点。该框架采用检索增强与验证引导的数据构建机制，经最多三轮修正保障代码与语义统一。推出含超 36.7 万个已验证 Lean4 示例的 FormalVerse 数据集，基于其训练的模型一致性检查率显著优于同类。核心模型 MathForm-8B 以四分之一参数体量反超更大模型，在多项基准测试中表现出较强推理与形式化纠错能力。