أخبار ar.wedoany.com، أعلنت شركة الذكاء الاصطناعي الأوروبية Mistral AI، في الثاني من الشهر الجاري بالتوقيت المحلي، عن إطلاق نموذج Leanstral 1.5، المصمم خصيصًا للغة البرمجة الرسمية للإثباتات الرياضية Lean 4. يبلغ إجمالي معاملات هذا النموذج 119 مليار معامل، مع تفعيل 6 مليارات معامل، وهو متاح كمصدر مفتوح بموجب ترخيص Apache-2.0.
أوضحت Mistral AI أن نموذج Leanstral 1.5 حقق نسبة إنجاز 100% في كل من مجموعة التحقق ومجموعة الاختبار لمعيار الرياضيات الشكلي miniF2F؛ كما تمكن من حل 587 مسألة من أصل 672 مسألة بلغة Lean 4 في مجموعة مسائل مسابقة الرياضيات PutnamBench؛ وفي اختبارات سلسلة FATE للجبر التجريدي، حقق النموذج نسبة نجاح 87% على مستوى الماجستير FATE-H، ونسبة 34% على مستوى الدكتوراه FATE-X، وهي أفضل النتائج المسجلة. تشير هذه الاختبارات إلى أن القدرات الرياضية للنموذج قد بلغت مستوى الاستخدام العملي.
أكدت Mistral AI على الميزة التكلفية للنموذج الجديد: فبالنسبة للمسائل في مجموعة بيانات PutnamBench، يبلغ متوسط تكلفة الحل باستخدام Leanstral 1.5 أربعة دولارات فقط، بينما يتطلب نموذج Seed-Prover 1.5 أكثر من 300 دولار، ويحتاج Aleph Prover إلى ما بين 54 و68 دولارًا.
وفي التطبيقات العملية، حدد Leanstral 1.5 47 خاصية مخالفة في 57 مستودعًا برمجيًا تم اختبارها، منها 11 خاصية تشير إلى عيوب حقيقية، بما في ذلك 5 مشكلات لم يتم الإبلاغ عنها سابقًا على GitHub.
