数学自动形式化取得重大进展：OpenBMB开源MathForm，8B模型超越更大模型
OpenBMB开源了MathForm，这是一套用于将自然语言数学表述自动形式化为Lean4的框架、数据集和模型。系统结合检索机制与编译器、语义一致性引导的验证流程，并根据Lean的诊断结果最多进行三轮修正。FormalVerse数据集包含超过36.7万个经过验证的Lean4示例。根据公开测试，使用FormalVerse训练的模型一致性检查率达到60.32%，高于FineLeanCorpus的46.53%和NuminaMath-LEAN的41.49%。MathForm-8B的语法检查通过率为88.06%，一致性检查率为72.37%。在难度较高的FATE-H和FATE-X子集上，该模型仅使用四分之一的参数量，却据称分别领先更大的32B模型10和12个百分点。
本文来源：AIbase，仅供学习参考，版权归原作者所有。