أطلقت Mistral AI نموذج Leanstral 1.5: نموذج ذكاء اصطناعي مجاني يحطم أرقامًا قياسية في التحقق الرسمي

قدمت Mistral AI في 2 يوليو 2026 Leanstral 1.5 — نموذج محدث للتحقق الرسمي مع 6 مليارات معامل نشط، موزع بحرية تحت رخصة Apache 2.0. تشبع النموذج تماماً معيار miniF2F، وحل 587 من 672 مهمة PutnamBench، وسجل أرقاماً قياسية في FATE-H (87%) و FATE-X (34%).

ماذا يستطيع Leanstral 1.5 أن يفعل

يتخصص النموذج في إثبات النظرية الرسمية بلغة Lean 4 والتحقق من الكود في المستودعات الحقيقية. النتائج الرئيسية للإصدار:

• 100% في miniF2F — تشبع كامل في مجموعات التحقق والاختبار
• 587 من 672 مهمة PutnamBench — 7 أكثر من المنافس Seed-Prover 1.5
• 87% في FATE-H و 34% في FATE-X — سجلات جديدة في مهام مستوى الدراسات العليا والدكتوراه
• حوالي $4 لكل مهمة مقارنة بـ $300 لـ Seed-Prover 1.5 في الوضع العالي
• 5 أخطاء كانت غير معروفة سابقاً في 57 مستودع مفتوح

تم اختبار النموذج بشكل منفصل على معيار FLTEval، بناءً على طلبات سحب حقيقية من مستودع برهان فيرما الأخير — مما يؤكد إمكانية التطبيق على المهام على نطاق صناعي.

كيف تم تدريب Leanstral 1.5

مرت Leanstral 1.5 بثلاث مراحل تحضير: التدريب المسبق، والتعلم الخاضع للإشراف، والتعلم المعزز باستخدام طريقة CISPO. في المرحلة الأخيرة، تدرب النموذج في بيئتين.

في البيئة متعددة الخطوات، تتلقى Leanstral بيان النظرية، وتقدم محاولة إثبات، وتتلقى تعليقات من مترجم Lean وتكرر حتى النجاح أو استنزاف الميزانية الحسابية.

في بيئة الوكيل، يعمل النموذج مثل المطور في نظام ملفات حقيقي: تحرير الملفات، وتنفيذ أوامر bash، والوصول إلى خادم لغة Lean في الوقت الفعلي لفحص الأهداف والأخطاء ومعلومات النوع. يتيح هذا الوضع حل المهام الطويلة: إكمال الأدلة الجزئية في المستودعات، وبناء اللمات المساعدة والحفاظ على التقدم عبر جولات متعددة من ضغط السياق.

لماذا هذا مهم

التحقق الرسمي هو واحد من أصعب المهام لنماذج اللغة: يتطلب النجاح الكمال الرياضي وسلاسل طويلة من التفكير. كانت الحلول القوية في هذا المجال في السابق إما باهظة الثمن أو مغلقة.

Leanstral 1.5 يغير هذه المعادلة. معمارية Mixture of Experts بمعاملات إجمالي 119 مليار ونشطة فقط 6 مليار تجعل الاستدلال اقتصادياً. رخصة Apache 2.0 تسمح بالاستخدام التجاري بدون قيود.

"يمكن أن تكون الطرق الرسمية الصارمة فعالة وعملية للاستخدام في العالم الحقيقي"، كما تقول فريق

Leanstral في Mistral AI.

ماذا يعني هذا

تفتح Mistral AI الوصول إلى أداة التحقق الرسمي التي تتفوق على المنافسين المغلقين في نسبة السعر إلى الجودة. يزيد النشر على Hugging Face وواجهة برمجية مجانية من سهولة الوصول للباحثين والمطورين ويمكن أن يسرع من اختراق الطرق الرسمية في تطوير البرامج الصناعية.

أسئلة يتكرر طرحها

أين يمكنني الحصول على إمكانية الوصول إلى Leanstral 1.5؟

يتم نشر النموذج على Hugging Face تحت رخصة Apache 2.0 ومتاح من خلال واجهة برمجية مجانية من Mistral AI. يُسمح بالاستخدام التجاري بدون شروط إضافية.

كم تكلفة العمل مع Leanstral 1.5؟

حوالي $4 لكل إثبات مهمة واحدة. يستهلك Seed-Prover 1.5 في الوضع العالي 10 أيام GPU على معالجات H20 ويكلف حوالي $300 لكل مهمة — فرق 75 مرة.