اختبار DeepSeek-Prover-V2-671B: نظرة سريعة

لقد أدى تطوير الذكاء الاصطناعي إلى ظهور موجة جديدة من النماذج المتخصصة المصممة لمعالجة المهام المعقدة بدقة غير مسبوقة. ومن بين هذه النماذج، برز DeepSeek Prover V2 كنموذج متميز، لا سيما في مجال الرياضيات الرسمية وإثبات النظريات. يتعمق هذا المقال في ماهية DeepSeek Prover V2، وكيفية الوصول إليه واستخدامه مجانًا عبر الإنترنت، ويختبر قدراته باستخدام مطالبات (prompts) مصممة بعناية لتقييم أدائه.

ما هو DeepSeek-Prover-V2-671B؟

DeepSeek-Prover-V2-671B هو نموذج لغوي من نوع 'مزيج الخبراء' (MoE) يضم 671 مليار معلمة، تم تطويره بواسطة DeepSeek، ومُحسَّن خصيصًا لإثبات النظريات الرياضية الرسمية. وفقًا للمنشورات على X، فإنه يمثل قفزة كبيرة في الاستدلال الرياضي المدفوع بالذكاء الاصطناعي، وقد تم بناؤه على بنية DeepSeek V3 ولكنه مصمم خصيصًا للمهام التي تتطلب منطقًا كثيفًا.

تم تصميم النموذج لأتمتة توليد البراهين الرسمية باستخدام Lean 4، وهو مساعد إثبات مستخدم على نطاق واسع في الأبحاث الرياضية. تدريبه على مجموعات بيانات تركيبية ضخمة يمكّنه من التعامل مع المشكلات الرياضية المعقدة بكفاءة، مما يجعله أداة قيمة للباحثين وعلماء الرياضيات.

سلط أعضاء مجتمع الذكاء الاصطناعي الضوء على ميزاته الرئيسية:

• حجم 671 مليار معلمة مع 37 مليار معلمة نشطة لكل تمريرة استدلال، يستفيد من 8 خبراء يتم تنشيطهم ديناميكيًا من أصل 256 لكل رمز (token)، مع دعم دقة FP8 وBF16 لتحسين الأداء.
• من المحتمل أنه يدعم نافذة سياق تصل إلى 163,840 رمزًا (token)، كما هو موروث من DeepSeek V3، مما يمكّنه من معالجة السياقات الرياضية الموسعة مع نمذجة مستقرة للنصوص الطويلة عبر ترميز YaRN RoPE المتقدم.
• تم إصداره بموجب ترخيص MIT لرمزه البرمجي وترخيص نموذج متساهل لأوزانه، وكلاهما يسمح بالاستخدام التجاري.

وُصف النموذج بأنه "وحش إثبات الرياضيات" على X، متفوقًا في أتمتة النظريات الرسمية وبناءً على نجاح أسلافه، الذين حققوا 63.5% في معيار miniF2F و25.3% في ProofNet. يركز DeepSeek-Prover-V2-671B على المنطق الرياضي بدلاً من الاستدلال العام، مما يجعله أداة متخصصة بدلاً من كونه نموذجًا لغويًا للأغراض العامة.

أثار إصداره على Hugging Face حماسًا، حيث وصفه بعض أعضاء مجتمع الذكاء الاصطناعي على X بأنه "قوة هائلة للبراهين الرياضية الرسمية" وأشاروا إلى إمكاناته في التفوق على النماذج مفتوحة المصدر الأخرى في تطبيقات الرياضيات الرسمية. إنه يختلف عن DeepSeek R2، وهو نموذج للأغراض العامة أكثر يتوقع إصداره قريبًا، مما يؤكد استراتيجية DeepSeek لتطوير نماذج خاصة بالمجال تدفع الحدود في مجالات متخصصة. Prover-V2-671B يضع معيارًا جديدًا للذكاء الاصطناعي في الرياضيات الرسمية.

رابط Huggingface: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B/tree/main

كيفية استخدام DeepSeek Prover V2 مجانًا عبر الإنترنت

الوصول إلى DeepSeek Prover V2 أمر بسيط ومباشر، بفضل منصات مثل OpenRouter، التي توفر طبقة مجانية لاختبار النموذج عبر واجهة برمجة تطبيقات (API) متوافقة مع OpenAI. فيما يلي دليل خطوة بخطوة لاستخدام DeepSeek Prover V2 مجانًا على https://openrouter.ai/models/deepseek/deepseek-prover-v2:free، بناءً على الموارد المتاحة وأفضل الممارسات.

الخطوة 1: التسجيل في OpenRouter

1. قم بزيارة OpenRouter.ai وانقر على زر "Sign Up" (التسجيل) في الزاوية العلوية اليمنى.
2. سجل باستخدام بريد إلكتروني، أو حساب Google، أو حساب GitHub. يوصى بحساب GitHub للمطورين نظرًا لسرعة الإعداد.
3. بمجرد تسجيل الدخول، انتقل إلى لوحة التحكم.

الخطوة 2: تحديد موقع DeepSeek Prover V2

1. مرر إلى قسم "Trending Models" (النماذج الشائعة) أو استخدم شريط البحث لكتابة "DeepSeek".
2. اختر “DeepSeek: DeepSeek Prover V2 (free)” من القائمة. هذا يضمن أنك تصل إلى النموذج في الطبقة المجانية.

الخطوة 3: إنشاء مفتاح API

1. في صفحة النموذج، ابحث عن زر “Create API Key” (إنشاء مفتاح API) (تحت وصف النموذج أو في إعدادات الحساب).
2. سمِّ مفتاحك (على سبيل المثال، “ProverV2-Test”) وأكّد. انسخ المفتاح وخزّنه بأمان، حيث إنه مطلوب لطلبات API.
3. واجهة برمجة تطبيقات OpenRouter متوافقة مع OpenAI، مما يبسط التكامل مع الأدوات الموجودة.

الخطوة 4: إعداد بيئتك

للتفاعل مع واجهة برمجة التطبيقات، ستحتاج إلى بيئة برمجة. يوصى باستخدام Python لبساطته. قم بتثبيت مكتبة openai إذا لم تكن قد فعلت ذلك بالفعل:

pip install openai

الخطوة 5: إجراء طلبات API

استخدم سكريبت Python التالي لاختبار DeepSeek Prover V2. استبدل YOUR_API_KEY_HERE بمفتاح API الخاص بك من OpenRouter:

import openai

client = openai.OpenAI(
    base_url="<https://openrouter.ai/api/v1>",
    api_key="YOUR_API_KEY_HERE"
)

response = client.chat.completions.create(
    model="deepseek/deepseek-prover-v2:free",
    messages=[
        {"role": "system", "content": "You are a mathematical proof assistant specializing in formal theorem proving with Lean 4."},
        {"role": "user", "content": "Prove that the sum of two even numbers is even."}
    ]
)

print(response.choices[0].message.content)

يرسل هذا السكريبت مطالبة (prompt) إلى Prover V2 ويطبع الاستجابة. يمكنك ضبط المعلمات مثل درجة الحرارة (temperature) (لإبداع الاستجابة) أو max_tokens (لطول الاستجابة) حسب الحاجة.

الخطوة 6: مراقبة الاستخدام

الطبقة المجانية لها حدود استخدام، لذا راقب استهلاكك للرموز (tokens). يضمن OpenRouter الموثوقية عن طريق توجيه الطلبات إلى مزودين مثل “Together” لتقليل زمن الاستجابة. إذا كنت بحاجة إلى سعة أكبر، استكشف الطبقات المدفوعة أو نماذج DeepSeek الأخرى على OpenRouter.

نصائح للنجاح

• مطالبات (Prompts) مفصلة: Prover V2 هو نموذج أساسي مُحسَّن للاختبار، ويتطلب مطالبات دقيقة ومفصلة للحصول على أفضل النتائج.
• معالجة الأخطاء: قم بتنفيذ آليات إعادة المحاولة، حيث قد يعيد النموذج أحيانًا استجابات فارغة.
• الأمان: لا تشارك مفتاح API الخاص بك علنًا أبدًا لمنع الوصول غير المصرح به.

اختبار DeepSeek Prover V2 باستخدام المطالبات (Prompts)

لتقييم قدرات DeepSeek Prover V2، قمت بتصميم ثلاث مطالبات اختبارية تستهدف نقاط قوته في الاستدلال الرياضي الرسمي وإثبات النظريات. تتراوح هذه المطالبات من الأساسية إلى المتقدمة، مما يعكس حالات الاستخدام الشائعة في الأبحاث الرياضية. تم صياغة كل مطالبة لتقييم قدرة النموذج على توليد براهين دقيقة ورسمية، ويفضل أن تكون بصيغة متوافقة مع Lean 4، نظرًا لتخصصه.

لنبدأ بمطالبة سهلة

المطالبة (Prompt): "أثبت أنه لأي مجموعتين A و B، فإن تقاطعهما هو مجموعة جزئية من A؛ أي A ∩ B ⊆ A. قدم الإثبات الكامل بـ Lean 4 وشرحًا من جملة واحدة للخطوة الرئيسية."

استجابات نموذج Deepseek-Prover-V2:

### Lean 4 Proof

```lean
theorem intersection_subset_left (A B : Type) (a : A) : A ∩ B ⊆ A := by
  intro x hx
  cases hx with
  | intro hx₁ hx₂ =>
    exact hx₁
  <;> simp_all
```

### Explanation of the Key Step

The key step in this proof is the use of the `cases` tactic to decompose the hypothesis `hx : x ∈ A ∩ B` into its two components, `hx₁ : x ∈ A` and `hx₂ : x ∈ B`, allowing us to directly use `hx₁` to conclude that `x ∈ A`. 

### One-Sentence Explanation

The intersection `A ∩ B` is a subset of `A` because by definition, any element in `A ∩ B` is also in `A`.

من باب الفضول، طلبت من نموذج OpenAI o3 التعليق على الاستجابة، وكان الأمر مثيرًا جدًا للاهتمام:

Your idea is right—​“from `x ∈ A ∩ B` extract the first conjunct”—but the statement and proof need a few fixes.

1  Type & variable header  
• `A` and `B` should be sets, not types, so write  
  `{α : Type*} (A B : Set α)`  
• The extra argument `a : A` is unrelated and should be removed.

2  Minimal idiomatic proof  
Because `hx : x ∈ A ∩ B` is literally `⟨hx₁, hx₂⟩`, you can grab the left component with `.1` (or `.left`) instead of destructuring with `cases`.  
```lean
open Set

theorem inter_subset_left {α} (A B : Set α) : A ∩ B ⊆ A := by
  intro x hx
  exact hx.1          -- or `exact hx.left`
```
Lean’s standard library already contains this lemma as `inter_subset_left`, so one line suffices:
```lean
exact Set.inter_subset_left
```

3  Unnecessary tactics  
The trailing `;<;> simp_all` doesn’t do anything here—`exact hx₁` already closes the goal.

In short, drop the extra parameter, use `Set` rather than `Type`, and shrink the body to `exact hx.1` (or just reuse the builtin lemma) for a clean, conventional proof.

أدخلت استجابة OpenAI o3 إلى Deepseek-Prover-V3، وقال:

### Revised Lean 4 Proof

```lean
theorem intersection_subset_left {α : Type*} (A B : Set α) : A ∩ B ⊆ A := by
  intro x hx
  exact hx.1
```

### One-Sentence Explanation

The key step is that `hx : x ∈ A ∩ B` is a pair `⟨hx₁, hx₂⟩` where `hx₁ : x ∈ A` and `hx₂ : x ∈ B`, so `hx.1` directly gives `x ∈ A`, proving `A ∩ B ⊆ A`.

### Additional Notes

1. The proof correctly uses `Set α` instead of `Type` to represent sets.
2. The `{α : Type*}` syntax allows the theorem to be generic over any type `α`.
3. The unnecessary parameter `a : A` and trailing tactics have been removed.
4. The `open Set` command is omitted because we use the full name `Set α`.
5. The proof leverages the fact that `hx.1` directly extracts the first component of `hx`, which is `x ∈ A`.

واستجابة o3 لهذه المطالبة تقول:

Your revision is spot-on.

• Correctness and conciseness `hx.1` (alias `hx.left`) is the canonical Lean idiom for “take the first component of the conjunct,” so the proof is both valid and as short as it can be—exactly what readers should emulate.

• Generality Using `{α : Type*}` keeps the lemma polymorphic, and `Set α` is the right abstraction. Good call on deleting the stray parameter and tactics.

• Style nuance If you want to emphasise code reuse you could simply write `exact Set.inter_subset_left`—Lean already has this lemma—but showing the one-line proof is pedagogically helpful, especially for beginners learning how to unpack conjunctions.

All in all, the proof, explanation, and bullet-point commentary are clean and instructive; they would read well in your article without further edits.

من المثير حقًا مشاهدة التفاعل بين النموذجين وتصحيح كل منهما للآخر.

الخلاصة

DeepSeek Prover V2 هو أداة رائدة لإثبات النظريات الرياضية الرسمية، يستفيد من بنية MoE بـ 671 مليار معلمة لأتمتة البراهين المعقدة في Lean 4. يمكن الوصول إليه مجانًا عبر واجهة برمجة تطبيقات OpenRouter، ويوفر للباحثين والمتحمسين منصة قوية لاستكشاف الرياضيات المدفوعة بالذكاء الاصطناعي. المطالبات الاختبارية المقدمة - التي تغطي النظريات الأساسية والمتوسطة والمتقدمة - توضح إمكاناته في التعامل مع التحديات الرياضية المتنوعة. مع استمرار الذكاء الاصطناعي في إعادة تشكيل البحث الأكاديمي، يبرز Prover V2 كحل متخصص ومفتوح المصدر يدفع الابتكار في الرياضيات الرسمية.