OpenBMB团队近日开源数学自动形式化框架、数据集与模型MathForm，面向Lean4数学定理形式化验证任务。该框架引入检索增强与验证引导的数据构建机制，通过检索Mathlib定义、结合Lean编译诊断和语义一致性反馈进行多轮修正。同期发布的FormalVerse数据集包含超36.7万个已验证Lean4示例。实验显示，基于该数据集训练的模型一致性检查率为60.32%。MathForm-8B在六项基准中语法检查通过率达88.06%，一致性检查通过率达72.37%，超过部分32B模型。
OpenBMB团队近日开源数学自动形式化框架、数据集与模型MathForm，面向Lean4数学定理形式化验证任务。该框架引入检索增强与验证引导的数据构建机制，通过检索Mathlib定义、结合Lean编译诊断和语义一致性反馈进行多轮修正。同期发布的FormalVerse数据集包含超36.7万个已验证Lean4示例。实验显示，基于该数据集训练的模型一致性检查率为60.32%。MathForm-8B在六项基准中语法检查通过率达88.06%，一致性检查通过率达72.37%，超过部分32B模型。