DeepSeek-Prover-V2-7B هو نموذج لغوي كبير مفتوح المصدر تم إنشاؤه للغة برمجة الذكاء الاصطناعي الرياضية Lean 4، والتي أصدرها فريق DeepSeek في 1 مايو 2025. تتمثل أهم ميزاته في قدرته على الجمع بسلاسة بين التفكير الرياضي غير الرسمي (أي طريقة التفكير التي يستخدمها البشر عادةً) مع البراهين الرسمية الصارمة، مما يسمح للنموذج بالتفكير بمرونة مثل البشر والجدال بدقة مثل أجهزة الكمبيوتر، وبالتالي تحقيق اندماج متكامل للتفكير الرياضي. نتائج الورقة ذات الصلة هيDeepSeek-Prover-V2: تطوير التفكير الرياضي الرسمي من خلال التعلم التعزيزي لتحليل الأهداف الفرعية".
يستخدم هذا البرنامج التعليمي بطاقة واحدة A6000 كمورد. هذا النموذج يدعم فقط مشاكل التفكير الرياضي.
2. أمثلة المشاريع
3. خطوات التشغيل
1. بعد بدء تشغيل الحاوية، انقر فوق عنوان API للدخول إلى واجهة الويب
إذا لم يتم عرض "النموذج"، فهذا يعني أنه يتم تهيئة النموذج. نظرًا لأن النموذج كبير الحجم، يرجى الانتظار لمدة 1-2 دقيقة وتحديث الصفحة.
2. بعد الدخول إلى صفحة الويب، يمكنك بدء محادثة مع النموذج
كيفية الاستخدام
4. المناقشة
🖌️ إذا رأيت مشروعًا عالي الجودة، فيرجى ترك رسالة في الخلفية للتوصية به! بالإضافة إلى ذلك، قمنا أيضًا بتأسيس مجموعة لتبادل الدروس التعليمية. مرحبًا بالأصدقاء لمسح رمز الاستجابة السريعة وإضافة [برنامج تعليمي SD] للانضمام إلى المجموعة لمناقشة المشكلات الفنية المختلفة ومشاركة نتائج التطبيق↓
دعم المشاريع
شكرًا لمستخدم Github xxxجججج1 نشر هذا البرنامج التعليمي.
