كشفت شركة ميسترال للذكاء الاصطناعي عن نموذج لغوي ضخم، يُدعى ديفسترال، مصمم لتطوير التطبيقات (البرمجة التفاعلية) ومُحسَّن للتحقق الرسمي من صحة التعليمات البرمجية. من المتوقع أن يُستخدم ديفسترال لإنشاء مساعدين ذكاء اصطناعي لا يقتصر دورهم على توليد التعليمات البرمجية فحسب، بل يضمنون أيضًا خلوها من الأخطاء.
أصبح Devstral أول نموذج مفتوح المصدر يدعم لغة البرمجة Lean 4 ومجموعة أدوات التحقق الرياضي المرتبطة بها. توفر Lean 4 إمكانية إثبات صحة الكود رياضيًا ومدى توافقه مع المواصفات، وهو ما يسمح، في سياق برمجة Vibe، بالتأكد من أن الكود الذي يولده نموذج الذكاء الاصطناعي يؤدي وظيفته على أكمل وجه.
يغطي النموذج 119 مليار مُعامل (6.5 مليار مُعامل مُفعّل لكل رمز)، ويأخذ في الاعتبار سياقات تضم 256 رمز، وهو منشور بموجب ترخيص Apache 2.0. يبلغ حجم الأرشيف القابل للتنزيل مع Leanstral 121 جيجابايت، وهو مناسب للاستخدام على الأنظمة المحلية. يمكن استخدام مكتبات vllm و transformers و SGLang للتنفيذ المحلي.
من بين مزايا أخرى، يمكن استخدام هذا النموذج لتطوير خوارزمية vibe في وكيل mistral-vibe مفتوح المصدر، ودمجه مع مجموعة أدوات Aeneas للتحقق من صحة كود Rust. يقبل النموذج النصوص والصور كمدخلات، وينتج نصوصًا فقط كمخرجات. كما يدعم تحليل محتوى الصور.
لتقييم قدرات نماذج الذكاء الاصطناعي، مع الأخذ في الاعتبار جودة التحقق الرسمي من الكود وكتابة البراهين الرياضية، تم تطوير مجموعة معايير FLTEval جديدة. في الاختبارات، تفوق نموذج Leanstral بشكل ملحوظ على نماذج المصادر المفتوحة الحالية Qwen3.5 397B-A17B وKimi-K2.5 1T-A32B وGLM5 744B-A40B. أظهر نتائج مماثلة لنموذجي Claude Haiku 4.5 وClaude Sonnet 4.6 من Anthropic، ولكنه كان أقل أداءً من نموذج Claude Opus 4.6. على وجه التحديد، سجل نموذج Opus 39.6 نقطة، بينما سجل Leanstral 21.9 نقطة في تمريرة واحدة و31.9 نقطة في 16 تمريرة. بلغت تكلفة استخدام Opus 1650 دولارًا، بينما بلغت تكلفة Leanstral 18 دولارًا في تمريرة واحدة و290 دولارًا في 16 تمريرة. حصلت قصيدة الهايكو على 23 نقطة بسعر 184 دولارًا، بينما حصلت قصيدة السونيت على 23.7 نقطة بسعر 549 دولارًا.
المصدر: opennet.ru
