最近一段时间，以 DeepSeek-R1 为代表的大型推理模型可谓是「当红炸子鸡」，不过整体来说，这些模型所做的推理都属于非形式化推理（informal reasoning）。也就是说，它们主要是通过自然语言执行推理。
但是，这种推理模式有个缺点：难以通过机器来自动验证。也因此，非形式化推理在实际应用中的可靠性就大打折扣了。这还会让研究者更加难以进一步对推理模型进行改进。
解决方案也很直观：形式化推理（formal reasoning）。
近日，普林斯顿大学陈丹琦、Sanjeev Arora 和金驰领导的一个团队开源了一个用于自动定理证明的形式化推理模型Goedel-Prover（哥德尔证明器），并且该模型在数学问题的自动形式化证明生成任务上达到了 SOTA。代码、模型还有在 Lean Workbook 中发现的新证明都已开源！
首先，先简单解释一下什么是形式化推理：简单来说，形式化推理就是以机器可验证的格式进行推理。这一类别中，比较知名的证明助手包括 Lean、Isabelle 和 Coq，它们都具备各自的形式语言（formal language），能以可被机器验证的方式表达推理。因此，训练 LLM 用这些形式语言编写证明具有重要意义。
不过，训练 LLM 用形式化语言进行定理证明还存在一个重大挑战，即缺少形式化数学陈述和证明。
对于用形式语言表达的定理，为其编写证明的要求很高，需要相当多的领域专业知识。
正因如此，目前公开的形式语言数据集规模都很有限。例如，Lean Workbook 数据集共有 140K 条形式化陈述，其中的形式化陈述使用了 Lean 来陈述问题，但没有证明。这些陈述中，只有 15.7K 条带有形式化证明，这些证明是由 InternLM2.5-StepProver 和 InternLM-Math-Plus 发现的。此外，Open Bootstrapped Theorems 数据集包含 107K 条陈述，其证明来自 Mathlib44。
然而，该团队观察到 Mathlib4 的分布与一般的问题求解基准（例如广泛使用的 miniF2F）的分布存在显著差异。例如，miniF2F 中的陈述主要来自高中数学，需要复杂的推理能力才能解决，而 Mathlib4 中的陈述则侧重于对高级数学概念的简单操作。此外，他们还发现将 Mathlib4 数据纳入训练并不能持续提高模型在 miniF2F 上的性能。
与形式语言的数据稀缺相比，用自然语言书写的数学题却有着海量数据储备，高中生桌子上堆满的「五三」就是一座座富矿。Numina 数据集更是收录了 86 万个高质量的问答对，囊括国内外的中小学数学题、国际奥数竞赛题以及合成数据等等。
为了将这些数据转化为可用的形式语言，研究团队训练了两个形式化转换器。其中一个基于 Lean Workbook 中的非形式 - 形式语言对训练，另一个则采用 Claude-sonnet-3.5 标注的语言对进行训练。下图展示了这些形式化转换器的训练过程。
这两个转换器完成对原始语句的形式化后，团队还用 LLM 加了一道验证，确保形式化后的语句准确保留了原始内容的含义，成功构建了一个含有 164 万个形式语句的数据集。
利用这个大规模形式化定理数据集，研究团队采用了一种循环改进的方法，称为专家迭代（expert iteration）：先用现有的最好模型（DeepSeek-Prover-V1.5-RL）去尝试解答大量数学题目，把解对的答案收集起来训练新模型，然后用新模型再去解题，不断重复这个过程。经过 8 轮这样的「以老带新」训练后，他们的新模型变得更加厉害了。下图展示了专家迭代的过程。
Goedel-Prover 表现如何？
具体有多厉害呢？如下图所示，在 miniF2F 上，新模型的解题正确率比之前的最优模型（DeepSeek-Prover-V1.5-RL）提高了 7.6%。在 Pass@32、64 直至 25600 测试中，都始终优于 DeepSeek-Prover-V1.5-RL。
新模型在 Lean Workbook 数学题库中成功解决了 29.7K 道题目，这个成绩差不多是其他顶尖模型（InternLM2.5-StepProver 和 InternLMMath-Plus）的两倍。在 PutnamBench 上，新模型解决了 7 个问题（Pass@512），位列排行榜第一。
论文共同一作、普林斯顿博士后 Yong Lin 在 上表示他们目前正在开发这个哥德尔证明器的强化学习版本，并且还会有一个比之前更强大的检查点模型。此外，他们还将在开源这个强化学习版本的同时附带 164 万条形式化陈述。
真是让人期待。
还没有评论，来说两句吧...