vLLM+Open WebUIを使用してDeepSeek-Prover-V2-7Bをデプロイする

1. チュートリアルの概要

DeepSeek-Prover-V2-7Bは、2025年5月1日にDeepSeekチームによってリリースされた、数学AIプログラミング言語Lean 4用に構築されたオープンソースの大規模言語モデルです。その最も重要な特徴は、非公式な数学的推論（つまり、人間が一般的に使用する推論方法）と厳密な形式的証明をシームレスに組み合わせる能力であり、モデルは人間と同じくらい柔軟に考え、コンピュータと同じくらい厳密に議論することができ、数学的推論の統合融合を実現します。関連する論文の結果は以下の通りである。DeepSeek-Prover-V2: サブゴール分解のための強化学習による形式数学的推論の進歩”。

このチュートリアルでは、リソースとして 1 枚のカード A6000 を使用します。このモデルは数学的推論問題のみをサポートします。

2. プロジェクト例

3. 操作手順

1. コンテナを起動した後、API アドレスをクリックして Web インターフェイスに入ります

「モデル」が表示されない場合は、モデルが初期化中であることを意味します。モデルが大きいため、1〜2分ほど待ってからページを更新してください。

2. Web ページに入ると、モデルと会話を開始できます。

利用手順

4. 議論

🖌️ 高品質のプロジェクトを見つけたら、メッセージを残してバックグラウンドで推奨してください。さらに、チュートリアル交換グループも設立しました。お友達はコードをスキャンして [SD チュートリアル] に参加し、さまざまな技術的な問題について話し合ったり、アプリケーションの効果を共有したりできます。

プロジェクトサポート

Githubユーザーに感謝 xxxjjjyyy1  このチュートリアルの展開。