DeepSeek-Prover: 大規模合成データによるLLMの定理証明能力の向上

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

May 23, 2024

著者: Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, Xiaodan Liang

cs.AI

要旨

Leanのような証明アシスタントは、数学的証明の検証に革命をもたらし、高い精度と信頼性を確保しています。大規模言語モデル（LLM）は数学的推論において有望ですが、形式的定理証明における進展は、訓練データの不足によって妨げられています。この問題を解決するため、高校および大学レベルの数学競技問題から派生したLean 4の証明データを大規模に生成するアプローチを提案します。このアプローチでは、自然言語の問題を形式的な命題に変換し、低品質な命題をフィルタリングし、証明を生成して合成データを作成します。この合成データセット（800万の形式的命題とその証明を含む）でDeepSeekMath 7Bモデルをファインチューニングした結果、Lean 4 miniF2Fテストにおいて、64サンプルで46.3%、累積で52%の全証明生成精度を達成し、ベースラインのGPT-4（64サンプルで23.0%）や木探索強化学習手法（41.0%）を上回りました。さらに、Lean 4 Formalized International Mathematical Olympiad（FIMO）ベンチマークでは、148問中5問の証明に成功し、GPT-4は1問も証明できませんでした。これらの結果は、大規模な合成データを活用してLLMの定理証明能力を向上させる可能性を示しています。今後の研究を促進するため、合成データセットとモデルを公開する予定です。

English

Proof assistants like Lean have revolutionized mathematical proof verification, ensuring high accuracy and reliability. Although large language models (LLMs) show promise in mathematical reasoning, their advancement in formal theorem proving is hindered by a lack of training data. To address this issue, we introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. This approach involves translating natural language problems into formal statements, filtering out low-quality statements, and generating proofs to create synthetic data. After fine-tuning the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs, our model achieved whole-proof generation accuracies of 46.3% with 64 samples and 52% cumulatively on the Lean 4 miniF2F test, surpassing the baseline GPT-4 at 23.0% with 64 samples and a tree search reinforcement learning method at 41.0%. Additionally, our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any. These results demonstrate the potential of leveraging large-scale synthetic data to enhance theorem-proving capabilities in LLMs. Both the synthetic dataset and the model will be made available to facilitate further research in this promising field.