base_model: deepseek-ai/DeepSeek-Prover-V2-671B language:

• en library_name: transformers tags:
• deepseek
• unsloth
• transformers license: mit

Unsloth Dynamic 2.0は優れた精度を達成し、他の主要な量子化手法を凌駕します。

deepseek-ai/DeepSeek-Prover-V2-671B

1. はじめに

DeepSeek-Prover-V2を紹介します。これはLean 4における形式的定理証明のために設計されたオープンソースの大規模言語モデルで、DeepSeek-V3を活用した再帰的定理証明パイプラインを通じて収集された初期データを用いて構築されています。コールドスタートのトレーニング手順では、DeepSeek-V3に複雑な問題をサブゴールに分解するよう促すことから始めます。解決されたサブゴールの証明は、連鎖思考プロセスとして統合され、DeepSeek-V3の段階的な推論と組み合わされて、強化学習の初期コールドスタートを形成します。このプロセスにより、非形式的および形式的な数学的推論を統一されたモデルに統合することが可能になります。

2. モデル概要

再帰的証明探索によるコールドスタート推論データの合成

• コールドスタートデータセットを構築するために、DeepSeek-V3をサブゴール分解と形式化の統一ツールとして活用する、シンプルで効果的な再帰的定理証明パイプラインを開発しました。DeepSeek-V3に定理を高レベルの証明スケッチに分解させると同時に、これらの証明ステップをLean 4で形式化し、一連のサブゴールを生成します。

• 各サブゴールの証明探索には、より小規模な7Bモデルを使用し、計算負荷を軽減します。難しい問題の分解ステップが解決されると、完全な段階的形式証明をDeepSeek-V3の連鎖思考と組み合わせて、コールドスタート推論データを作成します。

合成コールドスタートデータを用いた強化学習

• 7B証明モデルがエンドツーエンドで解決できなかった難しい問題のサブセットを選定し、すべての分解されたサブゴールが解決されたものに焦点を当てます。すべてのサブゴールの証明を組み合わせることで、元の問題に対する完全な形式的証明を構築します。この証明は、対応する補題分解を概説するDeepSeek-V3の連鎖思考に追加され、非形式的推論とその後の形式化を統合した一貫性のある合成を生成します。

• 合成コールドスタートデータで証明モデルを微調整した後、非形式的推論と形式的証明構築を橋渡しする能力をさらに強化するために、強化学習ステージを実施します。推論モデルの標準的なトレーニング目標に従い、正解か不正解かの二値フィードバックを報酬監視の主要な形式として使用します。

• 結果として得られたモデル、DeepSeek-Prover-V2-671Bは、ニューラル定理証明において最先端の性能を達成し、MiniF2F-testで88.9%のパス率を達成し、PutnamBenchから658問中49問を解決しました。DeepSeek-Prover-V2がminiF2Fデータセットに対して生成した証明は、ZIPアーカイブとしてダウンロード可能です。

3. ProverBench: AIMEおよび教科書問題の形式化

ProverBenchを紹介します。これは325問からなるベンチマークデータセットです。このうち15問は、最近のAIMEコンペティション（AIME 24および25）で出題された数論と代数の問題から形式化されたもので、本格的な高校生レベルの競技問題を提供しています。残りの310問は、教科書の例題や教育チュートリアルから選ばれたもので、多様で教育的な形式化数学問題のコレクションを構成しています。このベンチマークは、高校生レベルの競技問題から大学レベルの数学まで、より包括的な評価を可能にするように設計されています。

4. モデルおよびデータセットのダウンロード

DeepSeek-Prover-V2を2つのサイズでリリースします：7Bおよび671Bパラメータです。DeepSeek-Prover-V2-671BはDeepSeek-V3-Baseをベースにトレーニングされています。DeepSeek-Prover-V2-7BはDeepSeek-Prover-V1.5-Baseをベースにしており、最大32Kトークンの拡張コンテキスト長を特徴とします。

5. クイックスタート

HuggingfaceのTransformersを直接使用してモデル推論を行うことができます。DeepSeek-Prover-V2-671BはDeepSeek-V3と同じアーキテクチャを共有しています。詳細な情報とサポートされる機能については、Hugging FaceのDeepSeek-V3ドキュメントを参照してください。

以下は、miniF2Fデータセットの問題に対する証明を生成する基本的な例です：

from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
torch.manual_seed(30)

model_id = "DeepSeek-Prover-V2-7B"  # またはDeepSeek-Prover-V2-671B
tokenizer = AutoTokenizer.from_pretrained(model_id)

formal_statement = """
import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- What is the positive difference between $120\%$ of 30 and $130\%$ of 20? Show that it is 10.-/
theorem mathd_algebra_10 : abs ((120 : ‚Ñù) / 100 * 30 - 130 / 100 * 20) = 10 := by
  sorry
""".strip()

prompt = """
次のLean 4コードを完成させてください：

```lean4
{}
```

与えられた定理を形式的に証明するLean 4コードを生成する前に、主要な証明ステップと戦略を概説する詳細な証明計画を提供してください。
この計画は、最終的な形式的証明の構築を導く主要なアイデア、中間補題、および証明構造を強調する必要があります。
""".strip()

chat = [
  {"role": "user", "content": prompt.format(formal_statement)},
]

model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True)
inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device)

import time
start = time.time()
outputs = model.generate(inputs, max_new_tokens=8192)
print(tokenizer.batch_decode(outputs))
print(time.time() - start)

6. ライセンス

DeepSeek-Prover-V2モデルの使用は、モデルライセンスに従います。

7. 連絡先

ご質問がある場合は、イシューを立てるか、service@deepseek.comまでご連絡ください。