MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

想象一下，你正试图教一个聪明但有点笨拙的机器人学习纯逻辑语言。这个机器人是一个大语言模型（LLM），它擅长读故事、写诗和用普通英语解数学谜题。但问题在于：要以绝对的确定性证明一个数学定理，你不能只用文字；你需要用一种极其严格的计算机语言来编写，这种语言叫做 Lean 4。你可以把 Lean 4 想象成一个高安全性的保险库，在这里，每一个单词、符号和规则都必须完美无缺，否则保险库的大门将无法开启。问题是，虽然这个机器人懂数学，但它并不了解 Lean 4 所使用的特定“规则手册”（称为 Mathlib）。这就像是要求一位能做出完美牛排的厨师去遵循一份用他们从未见过的语言编写的食谱，而且食谱中使用的食材名称他们也并不知晓。他们可能会靠猜，但很可能会出错。

这就是“自动形式化”（autoformalization）发挥作用的地方：即把人类的数学转化为这种严格计算机代码的艺术。长期以来，研究人员一直试图直接让机器人去“翻译”数学，希望它能凭借训练时记住的规则来完成任务。但机器人总是出错，比如用错了食材，或者漏掉了关键步骤，因为它试图仅凭记忆来完成工作。这项研究名为 MathForm，它指出这种“猜测并希望”的方法是行不通的。相反，他们构建了一个系统，允许机器人在开始写作之前先查阅规则手册；如果它犯了错，一个严格的编辑不会直接丢弃作品，而是会精确地告诉机器人哪里错了，并让它重试直到正确为止。

开发 MathForm 的研究人员意识到，要让机器人完美地使用形式化数学语言，你不能只是让它写一个草稿然后听天由命。他们建立了一个三步走的流水线来优化机器人的工作流。首先，在机器人写下第一行代码之前，一个“研究员”（Researcher）智能体就会扫描庞大的 Mathlib 库，为该特定问题寻找精确的定义和规则。这就像是在厨师拿起刀之前，先给了他那页关于“牛排”的特定食谱。第二，机器人编写代码，然后由一个“检查员”（Inspector）进行检查。如果代码有语法错误（比如漏掉了一个逗号），检查员会指出它。如果代码可以编译通过但意思不对（比如在题目要求“仅限正数”时却说“所有数字”），检查员会解释其语义错误。第三，机器人不会放弃，而是利用这些反馈来重写代码。它会在这个“编写-检查-修复”的循环中不断迭代，直到代码完美无缺。

通过这个巧妙的循环，团队创建了一个名为 FormalVerse 的大规模新数据集，其中包含约 36.7 万个经过验证的数学示例。随后，他们基于这些数据训练了一个新模型 MathForm-8B。结果令人惊喜：这个规模相对较小（80 亿参数）的模型，在形式化数学方面的表现竟然优于许多依赖旧有“猜测并希望”方法的更大规模专业模型（320 亿参数）。在六个不同的困难数学测试中，MathForm-8B 通过严格“一致性检查”（即代码确实表达了人类题目所表达的意思）的成功率约为 72.4%，击败了之前的最强模型。即使是在最难、最抽象的代数问题上，它的表现也显著超过了那些体量更大的对手。这篇论文表明，通过给模型提供查找信息的工具以及从错误中学习的机会，你并不需要一个巨大的大脑来成为数学天才；你只需要一个聪明的流程。