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

DeepSeek-Prover-V2-7Bは、DeepSeekチームによって2025年5月1日に開発されたオープンソースの大規模言語モデルであり、Lean 4数学AIプログラミング言語向けに特別に設計されています。その最大の特徴は、非公式な数学的推論（つまり、人間が一般的に用いる推論手法）と厳密な形式的証明をシームレスに統合していることです。これにより、人間のような柔軟な思考とコンピュータのような厳密な証明が可能になり、数学的推論の統合的な融合を実現しています。関連研究論文も公開されています。 DeepSeek-Prover-V2: サブゴール分解のための強化学習による形式数学的推論の進歩 。

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

2. プロジェクト例

3. 操作手順

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

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

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

利用手順

4. 議論

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

プロジェクトサポート

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