💡
原文中文，约2300字，阅读约需6分钟。
📝
内容提要
普林斯顿大学团队开源了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的强化学习版本。
➡️
