面壁智能 OpenBMB·· 2026-08-21精选AI 评分69
面壁智能 OpenBMB 推出 MathForm，面向 Lean 4 数学自动形式化的开源框架、数据集与模型
🧮 Introducing MathForm, an open-source framework, dataset, and model for mathematical autoformaliza...
AI 导读
面壁智能 OpenBMB 推出 MathForm，一个面向 Lean 4 数学自动形式化的开源框架、数据集与模型。其 FormalVerse 数据集含 367K+ 已验证示例；在匹配 100K 预算下，基于其训练的模型 Consistency Check 达 60.32%，优于 FineLeanCorpus（46.53%）与 NuminaMath-LEAN（41.49%）。
推荐理由
数学形式化的难点是编译通过但语义漂移，该框架用检索规划和语义一致性反馈迭代修正，并开源数据集和 8B 模型，给小模型做形式化提供了可复用路径。
来源：面壁智能 OpenBMB · x.com