DeepSeek-Prover：通过大规模合成数据推进LLM中的定理证明 (arxiv.org)

为了解决大型语言模型（LLM）在形式定理证明方面训练数据缺乏的问题，DeepSeek-Prover方法利用高中和本科水平的数学竞赛问题生成大量的Lean 4证明数据。该方法将自然语言问题转化为形式语句，过滤掉低质量语句，并生成证明来创建合成数据。在包含800万个带有证明的形式语句的合成数据集上微调DeepSeekMath 7B模型后，该模型在Lean 4 miniF2F测试中实现了46.3%的完整证明生成准确率，优于基线GPT-4（23.0%）和树搜索强化学习方法（41.0%）。