میسترال ایآی، ایجنت اثبات متنباز لینسترال را برای لین ۴ راهاندازی میکند
زک اندرسون ۱۴۰۵/۱۲/۲۶ ۱۹:۱۳
میسترال، لینسترال را منتشر میکند، یک AI Agent با ۶ میلیارد پارامتر برای تاییدیه رسمی لین ۴، که با هزینه ۱/۱۵ نسبت به مدلهای بزرگتر تحت مجوز آپاچی ۲.۰ عملکرد بهتری دارد.
میسترال ایآی، لینسترال را در ۲۶ اسفند ۱۴۰۴ منتشر کرد—اولین AI Agent متنباز که بهطور خاص برای تاییدیه رسمی لین ۴ ساخته شده است. مدل ۱۲۰ میلیارد پارامتری تنها با ۶ میلیارد پارامتر فعال اجرا میشود و تحت مجوز آپاچی ۲.۰ عرضه میشود، که اثبات قضیه در سطح تولید را بدون بودجههای سازمانی قابل دسترس میکند.
چرا این برای کریپتو اهمیت دارد؟ تاییدیه رسمی—اثبات ریاضی اینکه کد دقیقاً همان کاری را انجام میدهد که ادعا میکند—به استاندارد طلایی برای امنسازی قراردادهای هوشمند و پروتکلهای بلاکچین تبدیل شده است. باگها در کد دیفای میلیاردها دلار هزینه داشتهاند. لینسترال میتواند بهطور چشمگیری موانع را برای پروژههایی که به دنبال امنیت تایید شده هستند کاهش دهد.
مبادلات عملکرد در مقابل هزینه
میسترال، لینسترال را در مقابل رقبای اختصاصی و متنباز با استفاده از FLTEval، یک مجموعه ارزیابی جدید که وظایف مهندسی اثبات واقعی از پروژه رسمیسازی قضیه آخر فرما را آزمایش میکند، معیار سنجی کرد.
اعداد چشمگیر هستند. لینسترال در pass@2، ۲۶.۳ امتیاز با ۳۶ دلار هزینه محاسباتی کسب کرد. کلاد سونت ۴.۶ موفق به کسب ۲۳.۷ امتیاز شد اما صورتحساب ۵۴۹ دلاری داشت—بیش از ۱۵ برابر هزینه برای عملکرد بدتر. حتی در pass@16، جایی که لینسترال ۳۱.۹ امتیاز با ۲۹۰ دلار به دست میآورد، هنوز کمتر از یک پنجم قیمت ۱,۶۵۰ دلاری کلاد اوپوس ۴.۶ هزینه دارد (اگرچه اوپوس با ۳۹.۶ در کیفیت پیشتاز است).
در مقابل جایگزینهای متنباز، شکاف کارایی بیشتر گسترش مییابد. GLM5-744B-A40B و Kimi-K2.5-1T-A32B حدود ۱۶-۲۰ امتیاز دارند، علیرغم داشتن ۶-۸ برابر پارامترهای فعال بیشتر. Qwen3.5-397B-A17B به چهار پاس نیاز دارد تا به ۲۵.۴ امتیاز برسد—لینسترال آن را با دو پاس شکست میدهد.
معماری فنی
لینسترال از معماری ترکیب پراکنده متخصصان بهینهشده برای گردشهای کاری مهندسی اثبات استفاده میکند. این مدل از طریق MCP (پروتکل زمینه مدل) با پروتکل سرور زبان لین یکپارچه میشود، که بهطور خاص برای عملکرد حداکثری با ابزار lean-lsp-mcp آموزش دیده است.
خود لین ۴ در شهریور ۱۴۰۲ بهطور پایدار راهاندازی شد و برای رسمیسازی ریاضیات به سرعت پذیرفته شده است. کتابخانه Mathlib—مجموعه عظیمی از اثباتهای ریاضی—با موفقیت در همان سال به لین ۴ منتقل شد. پروژههایی مانند اثبات رسمی قضیه آخر فرما قابلیت پلتفرم را برای کار ریاضی جدی نشان میدهند.
کاربردهای دنیای واقعی
میسترال نشان داد که لینسترال یک سؤال اشکالزدایی واقعی Stack Exchange درباره تغییرات شکستآور در لین ۴.۲۹.۰-rc6 را مدیریت میکند. ایجنت یک مسئله برابری تعریفی با نامهای مستعار نوع را تشخیص داد و به درستی مشخص کرد که تعویض def با abbrev تطبیق تاکتیک را بازیابی میکند.
این مدل همچنین ترجمه بین زبانی را نشان داد، تعاریف Rocq (قبلاً Coq) را به لین ۴ تبدیل کرد در حالی که معناشناسی اثبات را حفظ و نمادگذاری سفارشی را پیادهسازی میکند.
گزینههای دسترسی
سه مسیر استقرار وجود دارد: یکپارچهسازی مستقیم در میسترال وایب (از /leanstall برای شروع استفاده کنید)، یک نقطه پایانی API رایگان در labs-leanstral-2603 برای جمعآوری بازخورد محدود، یا استقرار خودمیزبان با وزنهای آپاچی ۲.۰.
برای پروژههای بلاکچین، محاسبه ساده است. تاییدیه رسمی بهطور سنتی یا به شرکتهای حسابرسی گران یا تخصص عمیق داخلی نیاز داشته است. یک AI Agent متنباز که میتواند صحت کد را با ۳۶-۲۹۰ دلار به ازای هر وظیفه اثبات کند، میتواند نحوه رویکرد پروتکلها به امنیت را تغییر دهد—با فرض اینکه اثباتها تحت شرایط تولید پایدار بمانند.
منبع تصویر: Shutterstock- mistral ai
- leanstral
- lean 4
- تاییدیه رسمی
- متنباز
