哥德尔-Prover超过DeepSeek-Prover，金驰、陈丹琦团队造出当前最强形式化推理模型

机器之心2025年02月13日约 4 分钟

机器之心报道

编辑：佳琪、Panda

最近一段时间，以 DeepSeek-R1 为代表的大型推理模型可谓是「当红炸子鸡」，不过整体来说，这些模型所做的推理都属于非形式化推理（informal reasoning）。也就是说，它们主要是通过自然语言执行推理。

但是，这种推理模式有个缺点：难以通过机器来自动验证。也因此，非形式化推理在实际应用中的可靠性就大打折扣了。这还会让研究者更加难以进一步对推理模型进行改进。

解决方案也很直观：形式化推理（formal reasoning）。

近日，普林斯顿大学金驰、陈丹琦、Sanjeev Arora 领导的团队开源了一个用于自动定理证明的形式化推理模型 Goedel-Prover（哥德尔证明器），并且该模型在数学问题的自动形式化证明生成任务上达到了 SOTA。代码、模型还有在 Lean Workbook 中发现的新证明都已开源！

论文标题：Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
论文链接：https://arxiv.org/abs/2502.07640v1
项目地址：https://github.com/Goedel-LM/Goedel-Prover
Hugging Face：https://huggingface.co/Goedel-LM/Goedel-Prover-SFT

首先，先简单解释一下什么是形式化推理：简单来说，形式化推理就是以机器可验证的格式进行推理。这一类别中，比较知名的证明助手包括 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 轮这样的「以老带新」训练后，他们的新模型变得更加厉害了。下图展示了专家迭代的过程。