“`markdown
陈丹琦团队发布最强形式化推理模型：Goedel-Prover超越DeepSeek-Prover
摘要： 普林斯顿大学陈丹琦、Sanjeev Arora 和金驰领导的团队近日开源了形式化推理模型 Goedel-Prover（哥德尔证明器），该模型在数学问题的自动形式化证明生成任务上达到SOTA，超越了此前领先的DeepSeek-Prover。这一突破标志着人工智能在形式化推理领域取得了重要进展，为机器自动验证和改进推理模型提供了新的可能性。
引言：
在人工智能领域，大型语言模型（LLM）如DeepSeek-R1正日益成为焦点。然而，这些模型主要依赖于非形式化推理，即通过自然语言进行推理。这种方式虽然灵活，但存在一个根本性的缺陷：难以进行机器自动验证，从而限制了其在实际应用中的可靠性和进一步改进的可能性。为了解决这一难题，形式化推理应运而生。
形式化推理的必要性与挑战
形式化推理，顾名思义，是以机器可验证的格式进行推理。像Lean、Isabelle和Coq这样的证明助手，都拥有各自的形式语言，能够以机器可验证的方式表达推理过程。因此，训练LLM使用这些形式语言编写证明具有重要意义。
然而，训练LLM进行形式化定理证明面临着一个巨大的挑战：形式化数学陈述和证明的稀缺。用形式语言表达定理并编写证明需要大量的领域专业知识，导致目前公开的形式语言数据集规模非常有限。例如，Lean Workbook数据集虽然包含14万条形式化陈述，但只有15.7K条带有形式化证明。
Goedel-Prover：突破数据瓶颈的创新方法
为了克服数据稀缺的难题，陈丹琦团队采取了一种巧妙的策略：将海量的自然语言数学题转化为可用的形式语言。他们训练了两个形式化转换器，一个基于Lean Workbook中的非形式-形式语言对，另一个则采用Claude-sonnet-3.5标注的语言对。
这两个转换器将原始语句形式化后，团队还利用LLM进行验证，确保形式化后的语句准确保留了原始内容的含义。最终，他们成功构建了一个包含164万个形式语句的大规模数据集。
专家迭代：不断提升模型性能
有了大规模的数据集，研究团队采用了一种循环改进的方法，称为专家迭代（expert iteration）。他们先用现有的最好模型（DeepSeek-Prover-V1.5-RL）去尝试解答大量数学题目，把解对的答案收集起来训练新模型，然后用新模型再去解题，不断重复这个过程。经过8轮这样的“以老带新”训练后，他们的新模型变得更加强大。
Goedel-Prover的卓越表现
Goedel-Prover的表现令人瞩目。在miniF2F测试中，新模型的解题正确率比之前的最优模型（DeepSeek-Prover-V1.5-RL）提高了7.6%。在Lean Workbook数学题库中，新模型成功解决了29.7K道题目，几乎是其他顶尖模型（InternLM2.5-StepProver和InternLM-Math-Plus）的两倍。在PutnamBench上，新模型解决了7个问题（Pass@512），位列排行榜第一。
未来展望
论文共同一作、普林斯顿博士后Yong Lin表示，他们目前正在开发哥德尔证明器的强化学习版本，并且还会有一个比之前更强大的检查点模型。此外，他们还将进一步探索形式化推理在其他领域的应用。
结论：
陈丹琦团队开发的Goedel-Prover模型在形式化推理领域取得了重大突破，为机器自动验证和改进推理模型提供了新的可能性。通过巧妙地将自然语言数学题转化为形式语言，并采用专家迭代的方法不断提升模型性能，Goedel-Prover在多个基准测试中超越了以往的模型。这一成果不仅推动了人工智能技术的发展，也为未来的研究方向提供了新的思路。
参考文献：
- Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving. https://arxiv.org/abs/2502.07640v1
- Goedel-Prover GitHub Repository: https://github.com/Goedel-LM/Goedel-Prover
- Goedel-Prover Hugging Face: https://huggingface.co/Goedel-LM/Goedel-Prover-SFT
- 机器之心报道：哥德尔-Prover超过DeepSeek-Prover，陈丹琦团队造出当前最强形式化推理模型.
关键词： 人工智能，形式化推理，定理证明，Goedel-Prover，DeepSeek-Prover，陈丹琦，机器学习，专家迭代，数学，Lean Workbook。
“`
Views: 0