DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

证明助手（如Lean）已经彻底改变了数学证明验证的方式，确保了高准确性和可靠性。虽然大型语言模型（LLMs）在数学推理方面表现出了很大的潜力，但是它们在正式定理证明方面的发展受到了缺乏训练数据的限制。为了解决这个问题，我们引入了一种方法来生成源自高中和本科级别数学竞赛问题的广泛的Lean 4证明数据。这种方法包括将自然语言问题转化为正式陈述，过滤掉低质量的陈述，并生成证明以创建合成数据。在将DeepSeekMath 7B模型微调到这个由800万个带有证明的正式陈述组成的合成数据集上之后，我们的模型在整个证明生成准确性上达到了46.3%（64个样本）和52%（累计）的Lean 4 miniF2F测试，超过了基线GPT-4（23.0%）和树搜索强化学习方法（41.0%）。此外，我们的模型成功地证明了Lean 4正式国际数学奥林匹克竞赛（FIMO）基准测试中的5个问题中的所有问题，而GPT-4则无法证明任何一个问题。这些结果展示了利用大规模合成数据来增强LLMs定理证明能力的潜力。合成数据集和模型都将被提供，以促进在这个有前途的领域进一步的研究。

如何利用大规模合成数据增强LLMs在形式化定理证明中的能力？

利用高中和本科数学竞赛问题生成大规模的Lean 4证明数据，并在此基础上对DeepSeekMath 7B模型进行微调，以提高其在整个证明生成和Lean 4 FIMO基准测试中的准确性。

该方法生成了包含800万个形式化陈述和证明的合成数据集，并在Lean 4 miniF2F测试中取得了46.3％的整个证明生成准确率和52％的累积准确率。此外，该模型成功证明了Lean 4 FIMO基准测试中的5个问题。

最近的相关研究包括使用不同的大规模数据集和模型进行形式化证明，如GPT-4和强化学习方法。