OpenBMB开源MathForm，以小参数突破数学自动形式化难题

OpenBMB团队近日发布了数学自动形式化开源框架MathForm，旨在解决通用人工智能（AGI）在严谨数学推理方面的关键挑战。该框架通过检索增强与验证引导机制，解决了Lean4语言形式化过程中概念映射不准、编译通过但语义错误等技术痛点。

核心模型MathForm-8B展现了惊人的推理效率。在FormalVerse数据集的训练下，该模型在多项基准测试中表现出色，其语法和一致性检查通过率反超了体量为其四倍的竞争对手。在处理FATE-H和FATE-X等高难度数学问题时，该模型表现出了极强的纠错能力，体现了其在数学逻辑推理上的深度。

MathForm的开源不仅为数学自动化提供了新的技术范式，也为科研人员提供了包含36.7万个已验证Lean4示例的数据集。随着这一框架的推广，有望进一步降低机器验证数学证明的难度，从而推动人工智能在科学计算领域的深度应用。