MathForm通过知识检索和验证引导迭代提升数学自动形式化能力
MathForm是一套用于构建验证训练数据的框架，旨在将数学命题转换为Lean 4等机器可验证的形式语言。系统在生成前从Mathlib检索相关定义和已有形式化内容，并利用编译器诊断与语义一致性反馈对结果进行迭代修订。由此构建的FormalVerse数据集包含约36.7万个经过验证的示例。经过监督微调和强化学习训练后，MathForm-8B在六项基准测试中取得了88.06%的平均Pass@8语法检查通过率和72.37%的一致性检查通过率，超过了多个拥有320亿参数的专业自动形式化模型。在FATE-H和FATE-X等高难度子集上，该模型也取得了更高的一致性通过率。
本文来源：Hugging Face，仅供学习参考，版权归原作者所有。