数学定理的自动形式化，一直是AI最难啃的硬骨头之一。说白了，就是让AI把一段自然语言写的数学命题，翻译成机器能严格验证的代码——比如Lean4语言。这可不是普通翻译，得把每个数学概念精准对应到工具库里的正确类型和定义，差一个符号都可能南辕北辙。
更麻烦的是，不少AI生成的“形式化语句”，编译能通过，数学上却完全是另一回事。就像抄答案抄对了格式，但过程根本不是原题。OpenBMB团队最新开源的MathForm框架，正是冲着这个痛点去的。
怎么解决？他们设计了一套“检索增强+验证引导”的生成机制。先用检索规划器从Mathlib工具库和现有形式化代码里找出需要用到的定义和模板，再让生成器基于Lean编译器给的“批改结果”和语义一致性反馈，反复修改，最多打磨三轮。相当于AI每次交卷，都有老师当面改错，改到对为止。
为了让AI有题可练，OpenBMB还发布了FormalVerse数据集，里面有超过36.7万个已验证的Lean4代码示例，横跨多个数学分支。用这份数据训练的模型，在一致性检查率上达到60.32%，远高于用现有数据集训练的46.53%和41.49%。
真正让人意外的是模型本身的实力。核心成果MathForm-8B，参数量只有对手的四分之一，却在六项基准测试里全面反超了ReForm-32B和Goedel-Formalizer-V2-32B这些32B大模型。语法检查通过率88.06%，一致性检查通过率72.37%。最难的FATE-H和FATE-X子集，分别拿下63%和37%的通过率，比原来最强的专项基准还高出10和12个百分点。
这传递的信号很明确：在数学形式化这个赛道上，模型大小不是决定因素，训练数据的质量和验证机制的设计才是破局关键。开源社区用8B的小体量证明了这一点，对大模型“唯参数论”的惯性思路是一次有力冲击。接下来值得关注的是，这套方法能否推广到Lean4之外的更多形式化语言上——如果可行，AI在数学研究中的角色，可能就从“工具”变成“协作者”了。