DeepSeek-Prover：通过大规模合成数据推进大型语言模型中的定理证明

像Lean这样的证明助手已经彻底改变了数学证明的验证，确保了高精度和可靠性。尽管大型语言模型（LLMs）在数学推理方面展现出潜力，但它们在形式定理证明领域的进展受到缺乏训练数据的限制。为了解决这一问题，我们提出了一种方法，从高中和本科水平的数学竞赛题目中生成大量的Lean 4证明数据。该方法包括将自然语言问题转化为形式陈述，过滤掉低质量的陈述，并生成证明以创建合成数据。在使用包含800万个带有证明的形式陈述的合成数据集对DeepSeekMath 7B模型进行微调后，我们的模型在Lean 4 miniF2F测试中，使用64个样本时达到了46.3%的整体证明生成准确率，累计准确率为52%，超过了基线GPT-4在相同条件下23.0%的准确率以及基于树搜索的强化学习方法41.0%的准确率。此外，我们的模型成功地证明了Lean 4形式化国际数学奥林匹克竞赛（FIMO）基准中的148个问题中的5个，而GPT-4未能证明任何一个。这些结果表明，利用大规模合成数据可以增强大型语言模型的形式定理证明能力。我们将提供合成数据集和模型，以促进这一前景广阔领域的进一步研究。