OpenBMB团队于2026年8月24日正式开源数学自动形式化框架、数据集与8B参数模型MathForm，该体系基于Lean4语言开发，可将自然语言数学概念精准映射至Mathlib库的规范定义中，解决了过往形式化语句编译通过但语义不符的行业痛点，为数学与AI交叉研究及AGI核心能力突破提供了全新底层工具。
在过去数年的通用人工智能技术研发中，数理逻辑推理能力被业内公认为AGI落地的核心门槛之一，而数学自动形式化更是门槛中的门槛——此前行业内仅有参数规模超过70B的头部大模型能实现尚可的形式化准确率，中小团队和个人研究者几乎没有低成本可用的成熟工具。
数学自动形式化的核心价值，是把用自然语言表述的数学定理、推导过程，转换为Lean4语言这类可被编译器直接验证的形式化代码，小到数论命题的正确性校验，大到航天控制算法、芯片设计逻辑的漏洞排查，都能用到这项技术。
但长期以来，行业一直面临两大核心痛点：一是形式化转换的“伪正确”问题，很多模型输出的代码虽然能通过编译器编译，但语义上和原始的数学命题完全不符，没有实际应用价值；二是好用的模型参数规模过大，推理成本高，普通科研团队很难负担。
登录后解锁全文，体验收藏、点赞、评论等完整功能
立即登录
滇公网安备 53252802528133号