北京
分享至
面壁智能 OpenBMB 推出 MathForm，一个面向 Lean 4 数学自动形式化的开源框架、数据集与模型。该项目旨在降低数学证明形式化的门槛，让研究者能更高效地将自然语言数学命题转化为机器可验证的 Lean 4 代码。
其核心组件 FormalVerse 数据集包含 367K+ 个已验证示例，为模型训练提供了扎实的语料基础。在匹配 100K 预算的评测条件下，基于该数据集训练的模型在 Consistency Check 任务上达到 60.32% 的准确率。
这一成绩显著优于同类开源方案：FineLeanCorpus 为 46.53%，NuminaMath-LEAN 为 41.49%。
目前，MathForm 的框架、数据集与模型均已开源，可供社区使用与二次开发。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
