🔥 把数学题翻成 Lean 4，难点不只是“翻译”：代码能编译，也可能漏掉假设、改了量词。MathForm 瞄准的就是“形式正确、语义跑偏”。

它把自动形式化从一次生成改成闭环：先检索 Mathlib 知识，再生成 Lean 4，用编译报错和语义检查反复修正；由此构建约 36.7 万条已验证样本 FormalVerse。

流程上，检索规划器先判断需要哪些定义，从 LeanExplore 为每个查询取前 2 个结果；候选经过格式、编译与语义三道检查，失败后带反馈重试，最多 3 轮。后两轮额外贡献 31% 的保留数据，说明定向修错确实突破了单次生成上限。

训练出的 MathForm-8B 在六个基准上，Pass@8 的语法检查和一致性检查均值达到 88.06% 和 72.37%，超过多款专用 32B 模型；在更抽象的 FATE-H、FATE-X 上，一致性通过率分别为 63% 和 37%。

对从业者最实用的启发，是把“能运行”和“意思对”拆成两道闸门，再把失败原因喂回下一轮。延伸来看，可以尝试用于教材题批量形式化或定理库迁移，为证明模型生产可信训练集。喜欢形式化数学的同学可以细读。

📚 论文地址：https://arxiv.org/pdf/2608.14221

#人工智能 #AI#论文 #大模型微调 #深度学