Mistral AI ने Lean 4 के लिए Leanstral ओपन-सोर्स प्रूफ एजेंट लॉन्च किया

Zach Anderson 16 मार्च, 2026 19:13

Mistral ने Leanstral जारी किया, जो Lean 4 फॉर्मल वेरिफिकेशन के लिए 6B पैरामीटर AI एजेंट है, जो Apache 2.0 लाइसेंस के तहत 1/15वीं लागत पर बड़े मॉडलों को मात देता है।

Mistral AI ने 16 मार्च, 2026 को Leanstral जारी किया—Lean 4 फॉर्मल वेरिफिकेशन के लिए विशेष रूप से बनाया गया पहला ओपन-सोर्स AI एजेंट। 120B पैरामीटर मॉडल केवल 6B सक्रिय पैरामीटर पर चलता है और Apache 2.0 लाइसेंसिंग के तहत आता है, जो एंटरप्राइज बजट के बिना प्रोडक्शन-ग्रेड थियोरम प्रूविंग को सुलभ बनाता है।

क्रिप्टो के लिए यह क्यों महत्वपूर्ण है? फॉर्मल वेरिफिकेशन—गणितीय प्रमाण कि कोड वही करता है जो वह दावा करता है—स्मार्ट कॉन्ट्रैक्ट्स और ब्लॉकचेन प्रोटोकॉल को सुरक्षित करने के लिए गोल्ड स्टैंडर्ड बन गया है। DeFi कोड में बग्स ने अरबों की लागत लगाई है। Leanstral सत्यापित सुरक्षा चाहने वाली परियोजनाओं के लिए बाधा को नाटकीय रूप से कम कर सकता है।

प्रदर्शन बनाम लागत ट्रेड-ऑफ

Mistral ने FLTEval का उपयोग करते हुए Leanstral को प्रोप्राइटरी और ओपन-सोर्स प्रतिस्पर्धियों के खिलाफ बेंचमार्क किया, जो Fermat's Last Theorem औपचारिकीकरण परियोजना से वास्तविक प्रूफ इंजीनियरिंग कार्यों का परीक्षण करने वाला एक नया मूल्यांकन सूट है।

संख्याएं चौंकाने वाली हैं। Leanstral ने pass@2 पर $36 की कंप्यूट लागत में 26.3 अंक स्कोर किए। Claude Sonnet 4.6 ने 23.7 अंक हासिल किए लेकिन $549 का बिल चलाया—खराब प्रदर्शन के लिए 15 गुना से अधिक लागत। यहां तक कि pass@16 पर, जहां Leanstral $290 में 31.9 अंक हासिल करता है, यह अभी भी Claude Opus 4.6 के $1,650 मूल्य टैग के एक-पांचवें से कम खर्च करता है (हालांकि Opus 39.6 पर गुणवत्ता में अग्रणी है)।

ओपन-सोर्स विकल्पों के खिलाफ, दक्षता का अंतर और बढ़ जाता है। GLM5-744B-A40B और Kimi-K2.5-1T-A32B 6-8 गुना अधिक सक्रिय पैरामीटर होने के बावजूद लगभग 16-20 अंक पर पठार पर पहुंचते हैं। Qwen3.5-397B-A17B को 25.4 अंक तक पहुंचने के लिए चार पास की आवश्यकता है—Leanstral दो के साथ इसे मात देता है।

तकनीकी आर्किटेक्चर

Leanstral प्रूफ इंजीनियरिंग वर्कफ़्लो के लिए अनुकूलित एक स्पार्स मिक्सचर-ऑफ-एक्सपर्ट्स आर्किटेक्चर का उपयोग करता है। मॉडल MCP (Model Context Protocol) के माध्यम से Lean के लैंग्वेज सर्वर प्रोटोकॉल के साथ एकीकृत होता है, विशेष रूप से lean-lsp-mcp टूलिंग के साथ अधिकतम प्रदर्शन के लिए प्रशिक्षित।

Lean 4 खुद सितंबर 2023 में स्थिर लॉन्च हुआ और गणित को औपचारिक बनाने के लिए तेजी से अपनाया गया है। Mathlib लाइब्रेरी—गणितीय प्रमाणों का एक विशाल संग्रह—उसी वर्ष Lean 4 में सफलतापूर्वक पोर्ट किया गया। Fermat's Last Theorem के औपचारिक प्रमाण जैसी परियोजनाएं गंभीर गणितीय कार्य के लिए प्लेटफॉर्म की क्षमता को प्रदर्शित करती हैं।

वास्तविक दुनिया के अनुप्रयोग

Mistral ने Leanstral को Lean 4.29.0-rc6 में ब्रेकिंग चेंजेस के बारे में एक वास्तविक Stack Exchange डिबगिंग प्रश्न को संभालते हुए प्रदर्शित किया। एजेंट ने टाइप एलियास के साथ एक परिभाषात्मक समानता मुद्दे का निदान किया और सही ढंग से पहचान की कि def को abbrev से बदलने से टैक्टिक मैचिंग बहाल हो जाएगी।

मॉडल ने क्रॉस-लैंग्वेज ट्रांसलेशन का भी प्रदर्शन किया, Rocq (पूर्व में Coq) परिभाषाओं को Lean 4 में परिवर्तित करते हुए प्रूफ सेमेंटिक्स को संरक्षित करते हुए और कस्टम नोटेशन को लागू करते हुए।

एक्सेस विकल्प

तीन डिप्लॉयमेंट पथ मौजूद हैं: Mistral Vibe में प्रत्यक्ष एकीकरण (शुरू करने के लिए /leanstall का उपयोग करें), सीमित समय की फीडबैक एकत्र करने के लिए labs-leanstral-2603 पर एक मुफ्त API एंडपॉइंट, या Apache 2.0 वेट्स के साथ सेल्फ-होस्टेड डिप्लॉयमेंट।

ब्लॉकचेन परियोजनाओं के लिए, गणना सीधी है। फॉर्मल वेरिफिकेशन के लिए पारंपरिक रूप से या तो महंगी ऑडिटिंग फर्मों या गहन इन-हाउस विशेषज्ञता की आवश्यकता होती है। एक ओपन-सोर्स एजेंट जो प्रति कार्य $36-290 पर कोड शुद्धता साबित कर सकता है, यह प्रोटोकॉल सुरक्षा के दृष्टिकोण को फिर से आकार दे सकता है—यह मानते हुए कि प्रमाण प्रोडक्शन स्थितियों में टिके रहते हैं।

• mistral ai
• leanstral
• lean 4
• formal verification
• open source