DeepSeek-Prover

https://arxiv.org/abs/2408.08152 DeepSeek-Prover-V1.5 は、Lean 4 上での定理証明のために開発されたオープンソースの大規模言語モデル (LLM) で、以下の方法で進化しています：

アプローチの革新

• 全体証明生成とステップ証明の融合
  • 従来の「全体証明生成（全ての証明コードを一括生成）」と「ステップ証明生成（1つずつステップを検証）」の利点を統合する「truncate-and-resume 機構」を導入。エラー箇所でコードを分割し、次のステップを生成する。
• Monte-Carlo Tree Search (MCTS)
  • 証明探索を効率化するため、新たなアルゴリズム「RMaxTS」を導入。エラー箇所での探索と「好奇心報酬」を活用し、解法パスの多様性を促進。

学習手法

• 事前学習
  • 数学とコードデータでLLMを強化。
• 教師あり微調整
  • データセットを拡張し、証明の途中状態（tactic state）をモデルに取り込む。
• 強化学習 (RL)
  • Lean 4 の証明フィードバックを報酬として利用し、モデルを最適化。

評価結果

• miniF2F (高校レベル数学問題): 達成率63.5%（従来最高の54.5%を上回る）。
• ProofNet (大学レベル数学問題): 達成率25.3%（従来最高の18.1%を上回る）。

結論と意義

• 全体生成とステップ生成のハイブリッドによって効率性と柔軟性を両立。
• 数学的推論能力が向上し、最先端の結果を達成。
• 今後、さらなる探索戦略やマルチ定理証明への応用が期待される。
• 本研究は、証明支援システムとLLMを統合する新しい可能性を示した。