DeepSeek-Prover: 大規模合成データを用いたLLMにおける定理証明の進歩

証明アシスタントであるLeanは、数学の証明検証を革命化し、高い精度と信頼性を確保しています。大規模言語モデル（LLMs）は数学的推論において有望な結果を示していますが、形式的な定理証明における進歩は訓練データの不足により阻まれています。この問題に対処するため、高校レベルおよび大学初年レベルの数学コンテスト問題から派生した広範なLean 4証明データを生成する手法を提案します。この手法には、自然言語の問題を形式的な命題に翻訳し、低品質の命題を取り除き、証明を生成して合成データを作成するプロセスが含まれます。DeepSeekMath 7Bモデルを800万件の形式的な命題とその証明から構成されるこの合成データセットで微調整した後、当社のモデルは64サンプルで46.3%、累積では52%の全体証明生成精度を達成しました。これは、基準となるGPT-4が64サンプルで23.0%、木探索強化学習手法が41.0%という結果を上回っています。さらに、当社のモデルはLean 4 Formalized International Mathematical Olympiad (FIMO) ベンチマークにおける148問中5問を成功裏に証明しましたのに対し、GPT-4はどの問題も証明できませんでした。これらの結果は、大規模な合成データを利用することでLLMsの定理証明能力を向上させる可能性を示しています。合成データセットとモデルは公開され、この有望な分野でのさらなる研究を促進するために利用できます。