DeepSeek-Prover-V2-671BがNovita AIで利用可能に

DeepSeek-Proverモデルシリーズとは？
DeepSeek-Prover-V2-671Bとは？
Novita AIでDeepSeek-Prover-V2-671Bにアクセスする方法
まとめ

DeepSeekは、数学関連の証明や定理を解くために設計されたAIモデル「Prover」をひっそりとアップデートしました。DeepSeek-Prover-V2-671BモデルがNovita AIのModel APIプラットフォームで利用可能になりました！期間限定で、新規ユーザーは$10の無料クレジットを請求して、この最先端の自動定理証明モデルを試すことができます。

以下がNovita AIでのDeepSeek-Prover-V2-671Bの現在の料金です：

DeepSeek-Prover-V2-671B: 入力トークン100万あたり0.7ドル、出力トークン100万あたり2.5ドル

これまでにリリースされた中で最も高度な形式定理証明モデルの1つで、数学のワークフロー、研究、教育ツールを強化しましょう。今すぐAPI呼び出しで利用可能です。

DeepSeek-Proverモデルシリーズとは？

DeepSeek-Proverモデルシリーズは、数学における自動定理証明の課題に取り組むために設計された、最先端の大規模言語モデル（LLM）ファミリーです。DeepSeek-AIによって開発され、これらのモデルは特に形式数学証明の生成、検証、推論に最適化されています。特にLean 4証明アシスタント環境内での使用を想定しています。

DeepSeek-Proverが作られた理由は？

GPT-4のような現代のLLMは数学的推論に優れていますが、形式言語での高品質で大規模なトレーニングデータが不足しているため、形式証明タスクには苦戦します。DeepSeek-Proverは、数学コンテストの問題から数百万の合成Lean 4証明を自動生成し、このユニークなデータセットでモデルを微調整することでこれを解決します。

DeepSeek-Proverはどのように動作するのか？

DeepSeek-Proverのパイプラインは次のとおりです：

自動形式化（Autoformalization）： LLMを使用して、自然言語の数学問題を形式なLean 4ステートメントに変換します。
品質フィルタリング： モデルのスコアリングと仮説棄却を通じて、論理的正確性と数学的関心に基づきステートメントをフィルタリングします。
証明生成と検証： フィルタリングされたステートメントの証明を試み、正しく検証可能な証明のみを保持します。
反復学習： このプロセスを繰り返し、毎回新しい高品質の証明データを使用してモデルをさらに改善します。

このアプローチにより、DeepSeek-Proverシリーズは継続的に改善されるモデルを生み出し、世界最大級の形式数学証明コレクションでサポートされています。

以前のDeepSeek-Proverモデルのハイライトとマイルストーン

規模： 800万以上の形式なLean 4ステートメントとその証明が生成されました。
技術基盤： DeepSeekMath 7Bなどの大規模トランスフォーマーモデルをベースに、膨大な数学データで事前学習し、さらに合成証明で微調整されています。
最先端のパフォーマンス： 形式定理証明ベンチマーク（例：miniF2F、FIMO）でトップクラスの結果を達成し、GPT-4や他の専門モデルを凌駕しています。

DeepSeek-Prover-V2-671Bとは？

DeepSeek-Prover-V2-671B は、DeepSeek-Proverシリーズのフラッグシップモデルです。以下の点が際立っています：

圧倒的な規模： 約6710億のパラメータを持ち、形式数学と定理証明のために設計された最大級のモデルです。
FP8精度： DeepSeek-Prover-V2-671Bは、当初FP8（浮動小数点8ビット）精度でトレーニングおよびリリースされました。これは、高いパフォーマンスを維持しながら、効率的な計算とより高速なモデルサービス、メモリ使用量の削減を可能にする最新の形式です。
高度な機能： 最先端のトランスフォーマーアーキテクチャを採用し、BF16、FP8_E4M3、F32などの最新のテンソル型をサポートしており、高性能な研究および本番環境に適しています。
定理証明に特化： 大規模で高品質な合成証明データでトレーニングされており、複雑な数学的推論と形式なLean 4証明生成に優れています。

Novita AIでDeepSeek-Prover-V2-671Bにアクセスする方法

Novita AIでDeepSeek-Prover-V2-671Bを使い始めるのは、迅速、簡単、そしてリスクフリーです。紹介プログラムにより、$10の無料クレジット が受け取れます。これでDeepSeek-Prover-V2-671Bの性能を存分に試し、プロトタイプを構築し、最初のユースケースを立ち上げるまで、初期費用なしで行えます。

プレイグラウンドを使用する（コーディング不要）

インスタントアクセス： サインアップして無料クレジットを請求し、すぐにDeepSeek-Prover-V2-671Bや他のトップモデルを試せます。
インタラクティブUI： プロンプト、思考連鎖推論をテストし、結果をリアルタイムで可視化できます。
モデル比較： DeepSeek-Prover-V2-671B、Llama 4、DeepSeekなどを簡単に切り替えて、ニーズに最適なモデルを見つけられます。

API経由で統合する（開発者向け）

Novita AIの統合REST APIを使用して、DeepSeek-Prover-V2-671Bをアプリケーション、ワークフロー、チャットボットにシームレスに接続できます。モデルのウェイトやインフラを管理する必要はありません。Novita AIは多言語SDK（Python、Node.js、cURLなど）と、パワーユーザー向けの高度なパラメータ制御を提供しています。

オプション1：直接API統合（Python例）

始めるには、以下のコードスニペットを使用してください：

from openai import OpenAI
  
client = OpenAI(
    base_url="https://api.novita.ai/v3/openai",
    api_key="<YOUR Novita AI API Key>",
)

model = "deepseek/deepseek-prover-v2-671b"
stream = True # or False
max_tokens = 2048
system_content = """Be a helpful assistant"""
temperature = 1
top_p = 1
min_p = 0
top_k = 50
presence_penalty = 0
frequency_penalty = 0
repetition_penalty = 1
response_format = { "type": "text" }

chat_completion_res = client.chat.completions.create(
    model=model,
    messages=[
        {
            "role": "system",
            "content": system_content,
        },
        {
            "role": "user",
            "content": "Hi there!",
        }
    ],
    stream=stream,
    max_tokens=max_tokens,
    temperature=temperature,
    top_p=top_p,
    presence_penalty=presence_penalty,
    frequency_penalty=frequency_penalty,
    response_format=response_format,
    extra_body={
      "top_k": top_k,
      "repetition_penalty": repetition_penalty,
      "min_p": min_p
    }
  )

if stream:
    for chunk in chat_completion_res:
        print(chunk.choices[0].delta.content or "", end="")
else:
    print(chat_completion_res.choices[0].message.content)

主な機能：

統合エンドポイント： /v3/openai はOpenAIのChat Completions API形式をサポートしています。
柔軟な制御： temperature、top-p、ペナルティなどを調整して、結果をカスタマイズできます。
ストリーミングとバッチ処理： 好みの応答モードを選択できます。

オプション2：OpenAI Agents SDKによるマルチエージェントワークフロー

Novita AIをOpenAI Agents SDKと統合して、高度なマルチエージェントシステムを構築できます：

プラグアンドプレイ： 任意のOpenAI AgentsワークフローでNovita AIのLLMを使用できます。
ハンドオフ、ルーティング、ツール使用をサポート： 委任、トリアージ、関数実行が可能なエージェントを設計できます。すべてNovita AIのモデルを搭載しています。
Python統合： SDKをNovitaのエンドポイント（https://api.novita.ai/v3/openai）に向け、APIキーを使用するだけです。

サードパーティプラットフォームでDeepSeek-Prover-V2-671B APIに接続する

Hugging Face： Novita AIのエンドポイントを介して、Spaces、パイプライン、またはTransformersライブラリでDeepSeek-Prover-V2-671Bを使用できます。
エージェント＆オーケストレーションフレームワーク： 公式コネクタとステップバイステップの統合ガイドを通じて、Continue、AnythingLLM、LangChain、Dify、Langflowなどのパートナープラットフォームと簡単に接続できます。
OpenAI互換API： OpenAI API標準向けに設計されたClineやCursorなどのツールとの統合も、手間なく移行・統合できます。

まとめ

DeepSeek-Prover-V2-671Bは、研究者、開発者、教育者を問わず、世界クラスの自動定理証明をすぐに利用できるようにします。試してみませんか？Novita AIにサインアップして無料クレジットを請求し、形式数学とAI駆動の証明生成の未来を体験してください！

Novita AIについて

Novita AIは、開発者がシンプルなAPIを使ってAIモデルを簡単にデプロイできるクラウドプラットフォームであり、手頃で信頼性の高いGPUクラウドも提供しています。

DeepSeek-Prover-V2-671BがNovita AIで利用可能に