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

文章预览

机器之心报道 编辑：佳琪、Panda 最近一段时间，以 DeepSeek-R1 为代表的大型推理模型可谓是「当红炸子鸡」，不过整体来说，这些模型所做的推理都属于非形式化推理（informal reasoning）。也就是说，它们主要是通过自然语言执行推理。 但是，这种推理模式有个缺点：难以通过机器来自动验证。也因此，非形式化推理在实际应用中的可靠性就大打折扣了。这还会让研究者更加难以进一步对推理模型进行改进。 解决方案也很直观： 形式化推理（formal reasoning） 。 近日，普林斯顿大学陈丹琦、Sanjeev Arora 和金驰领导的一个团队开源了一个用于自动定理证明的形式化推理模型 Goedel-Prover（哥德尔证明器） ，并且该模型在数学问题的自动形式化证明生成任务上达到了 SOTA。代码、模型还有在 Lean Workbook 中发现的新证明都已开源！ 论文标题：Goedel-Prover: A Fronti ………………………………