哥德尔-Prover超过DeepSeek-Prover，陈丹琦团队造出当前最强形式化推理模型
内容提要
普林斯顿大学团队开源了Goedel-Prover形式化推理模型，成功解决非形式化推理验证问题。该模型在自动定理证明中表现优异，准确率提高7.6%，解决了29.7K道题目，推动了形式化推理的发展。
关键要点
-
普林斯顿大学团队开源了Goedel-Prover形式化推理模型。
-
Goedel-Prover成功解决了非形式化推理验证问题。
-
该模型在自动定理证明中表现优异，准确率提高7.6%。
-
Goedel-Prover解决了29.7K道题目，推动了形式化推理的发展。
-
形式化推理是以机器可验证的格式进行推理，知名证明助手包括Lean、Isabelle和Coq。
-
训练LLM用形式化语言进行定理证明面临缺少形式化数学陈述和证明的挑战。
-
目前公开的形式语言数据集规模有限，Lean Workbook数据集仅有15.7K条带有形式化证明。
-
研究团队训练了两个形式化转换器，将自然语言数学题转化为形式语言。
-
利用大规模形式化定理数据集，采用专家迭代方法不断改进模型。
-
新模型在miniF2F上的解题正确率比之前的最优模型提高了7.6%。
-
新模型在Lean Workbook数学题库中成功解决了29.7K道题目，成绩是其他顶尖模型的两倍。
-
普林斯顿博士后Yong Lin表示正在开发Goedel-Prover的强化学习版本。
延伸解读
形式化推理的重要性
形式化推理通过机器可验证的方式进行推理，解决了非形式化推理在自动验证上的局限性。这使得形式化推理在实际应用中更具可靠性，尤其在自动定理证明领域，能够推动相关技术的进步。
数据集的挑战与机遇
尽管形式化推理模型如Goedel-Prover取得了显著进展，但仍面临数据集稀缺的问题。现有的形式语言数据集规模有限，而自然语言数学题的数据量庞大，这为模型训练提供了新的机遇。研究团队通过训练形式化转换器，将自然语言转化为形式语言，成功构建了一个包含164万个形式语句的数据集。
专家迭代方法的优势
研究团队采用的专家迭代方法，通过不断循环改进模型，显著提升了Goedel-Prover的性能。这种方法不仅提高了解题正确率，还能有效利用已有模型的优势，为未来的模型开发提供了可借鉴的思路。
延伸问答
Goedel-Prover是什么？
Goedel-Prover是普林斯顿大学团队开源的形式化推理模型，用于自动定理证明。
Goedel-Prover在自动定理证明中的表现如何？
Goedel-Prover在miniF2F上的解题正确率比之前的最优模型提高了7.6%，并成功解决了29.7K道题目。
形式化推理与非形式化推理有什么区别？
形式化推理是以机器可验证的格式进行推理，而非形式化推理主要通过自然语言执行，难以自动验证。
Goedel-Prover是如何训练的？
Goedel-Prover通过专家迭代方法训练，利用现有模型解题并收集正确答案来不断改进新模型。
Goedel-Prover解决了多少道数学题？
Goedel-Prover成功解决了29.7K道数学题。
Goedel-Prover的未来发展方向是什么？
研究团队正在开发Goedel-Prover的强化学习版本，并计划开源164万条形式化陈述。
