Leanstral 1.5: औपचारिक सत्यापन में नई उपलब्धि
मूल शीर्षक: Leanstral 1.5: Proof abundance for all
यह क्यों महत्वपूर्ण है
ओपन-सोर्स औपचारिक verification में यह प्रगति AI-आधारित code safety और mathematical proof की पहुँच को व्यापक बनाती है।
Mistral AI ने 2 जुलाई 2026 को Leanstral 1.5 जारी किया। यह Apache-2.0 लाइसेंस के तहत मुफ़्त उपलब्ध 6B सक्रिय पैरामीटर वाला मॉडल है, जो miniF2F को संतृप्त करता है और PutnamBench के 587/672 प्रश्न हल करता है।
Mistral AI ने Leanstral 1.5 लॉन्च किया है, जो Lean 4 में proof engineering के लिए एक ओपन-सोर्स मॉडल है। इसमें कुल 119B पैरामीटर हैं, लेकिन सक्रिय रूप से केवल 6B पैरामीटर उपयोग होते हैं। यह मॉडल Apache-2.0 लाइसेंस के अंतर्गत निःशुल्क उपलब्ध है और Hugging Face तथा एक मुफ़्त API के माध्यम से एक्सेस किया जा सकता है।
प्रदर्शन के मोर्चे पर, Leanstral 1.5 ने miniF2F बेंचमार्क को संतृप्त किया, PutnamBench के 672 में से 587 समस्याएं हल कीं, और FATE-H पर 87% तथा FATE-X पर 34% के साथ state-of-the-art परिणाम प्राप्त किए। इसके अलावा, मॉडल ने 57 ओपन-सोर्स repositories में परीक्षण के दौरान 5 पहले से अज्ञात bugs की खोज की।
Training प्रक्रिया तीन चरणों में हुई: mid-training, supervised fine-tuning, और CISPO के साथ reinforcement learning। मॉडल को दो RL वातावरणों में प्रशिक्षित किया गया — एक multiturn environment जहाँ मॉडल को theorem statement दिया जाता है और उसे सिद्ध या खंडन करना होता है।
Leanstral 1.5 agentic proof engineering और real-world code verification में भी सक्षम है, जो यह दर्शाता है कि औपचारिक verification विधियाँ व्यावहारिक उपयोग के लिए प्रभावी हो सकती हैं।