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

主要观点总结

近期，大型推理模型如DeepSeek-R1备受关注，但它们主要执行非形式化推理，难以通过机器自动验证，影响了在实际应用中的可靠性。为此，普林斯顿大学的一个团队提出了形式化推理的解决方案，并开源了名为Goedel-Prover的形式化推理模型。该模型在数学问题的自动形式化证明生成任务上达到SOTA。文章介绍了形式化推理的概念、Goedel-Prover模型的原理、训练过程以及其在不同测试集上的表现。

关键观点总结

关键观点1: 大型推理模型如DeepSeek-R1面临的问题

这些模型主要进行非形式化推理，难以通过机器自动验证，导致在实际应用中的可靠性降低，并且研究者难以进一步改进。

关键观点2: 形式化推理和Goedel-Prover模型的引入

为了解决上述问题，普林斯顿大学团队引入了形式化推理，并开源了Goedel-Prover模型。该模型使用机器可验证的格式进行推理，达到了SOTA。

关键观点3: Goedel-Prover模型的数据集挑战和解决方案

形式化语言的数据集规模有限，且存在领域专业知识需求高的挑战。研究团队通过训练两个形式化转换器，成功构建了一个含有164万条形式语句的数据集。

关键观点4: 循环改进方法和专家迭代

研究团队采用循环改进方法和专家迭代，通过不断迭代训练模型，最终提高了模型的性能。

关键观点5: Goedel-Prover模型的表现

在多个测试集上，Goedel-Prover模型的性能表现优异，超过了之前的最佳模型。此外，该模型还解决了大量的数学题目，并在PutnamBench上位列第一。