搜索
OpenBMB开源数学自动形式化框架MathForm
1 小时前
据AIBASE报道，OpenBMB团队近日正式开源了数学自动形式化框架、数据集与模型MathForm，以解决数学形式化中代码可编译但语义不准确的问题。该框架引入检索增强与验证引导的数据构建机制，通过检索规划器提取Mathlib定义，生成器结合Lean编译器诊断结果与语义一致性反馈进行修正。数据集FormalVerse包含超36.7万个已验证Lean4示例。实验显示，基于该数据集训练的模型一致性检查率达60.32%，核心模型MathForm-8B在六项基准测试中实现88.06%语法检查通过率和72.37%一致性检查通过率。
