🌟 به‌روزرسانی مدل Leanstral 1.5 از Mistral AI – پیشرفت در اثبات‌های صوری

میسترال‌ای‌آی از نسخه‌ی جدید مدل خود برای زبان Lean 4 رونمایی کرده است. این مدل به ریاضیدانان و توسعه‌دهندگان کمک می‌کند تا اثبات‌های صوری (Formal Proofs) بنویسند و آنها را به‌گونه‌ای تأیید کنند که کامپایلر Lean بپذیرد.

---

⚙️ مشخصات فنی:

- معماری Mixture of Experts (MoE) با ۱۱۹ میلیارد پارامتر کلی و ۶.۵ میلیارد پارامتر فعال
- پنجره‌ی متنی ۲۵۶ هزار توکنی
- قابلیت دریافت ورودی چندوجهی (Multimodal)
- مجوز Apache 2.0

---

🎯 روش آموزش پیشرفته:

نسخه‌ی ۱.۵ در دو محیط جداگانه آموزش مرحله‌ای دیده است:

۱. محیط اثبات قضیه – تعامل با کامپایلر Lean برای اثبات صحیح گزاره‌های ریاضی
۲. محیط برنامه‌نویسی واقعی – شبیه‌سازی رفتار یک برنامه‌نویس در مخازن کد

---

📊 نتایج چشمگیر در بنچمارک‌ها:

- امتیاز ۱۰۰٪ در بنچمارک miniF2F (هم در مجموعه‌ی اعتبارسنجی و هم آزمون)
- حل ۵۸۷ از ۶۷۲ مسئله در PutnamBench
- ثبت بهترین نتایج روز در مجموعه‌های FATE-H و FATE-X

---

💰 مزیت هزینه‌ای قابل‌توجه:

در بنچمارک PutnamBench، Leanstral 1.5 با ۷ مسئله بیشتر از سیستم Seed-Prover 1.5 موفق عمل کرده، در حالی که هزینه‌ی حل هر مسئله حدود ۴ دلار است (در مقابل ۳۰۰+ دلار برای رقیب).

---

🐛 کشف باگ‌های واقعی:

در آزمون کدنویسی روی ۵۷ مخزن نرم‌افزاری، این سیستم موفق به شناسایی ۴۷ نقض در ویژگی‌های کد شد که از این میان:
- ۱۱ مورد خطای واقعی بودند
- ۵ مورد قبلاً ناشناخته بودند

---

🔗 لینک‌های مفید:

📄 پست وبلاگ
https://mistral.ai/news/leanstral-1-5

🤖 مدل در Hugging Face
https://huggingface.co/mistralai/Leanstral-1.5

🎮 نسخه‌ی آزمایشی
https://huggingface.co/spaces/mistralai/Leanstral-1.5

---

#MistralAI #Leanstral #Lean4 #اثبات_صوري #هوش_مصنوعي #AI #ML

🆔 @asrgooyeshpardaz