Leanstral 1.5

 (docs.mistral.ai)
1 पॉइंट द्वारा GN⁺ 3 시간 전 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • Leanstral 1.5 Lean 4 formal proof engineering के लिए अनुकूलित updated model है, जिसका लक्ष्य automated theorem proving और automated formalization है
  • model scale कुल 119B parameters और 6.5B active parameters के कॉन्फ़िगरेशन वाला है, और इसे लंबे proofs व document context को संभालने की धारणा पर बनाया गया है
  • दिया गया identifier labs-leanstral-1-5 है, और documentation में इसे Labs v1.5 model के रूप में दिखाया गया है
  • context length 256k है, और pricing item $0 दिखाया गया है, जिससे experimentation और evaluation के लिए accessibility पर जोर मिलता है
  • इसे Chat Completions, function calling, agents, structured outputs, OCR, Document QnA, FIM, embeddings, moderation, audio और batch processing APIs के साथ इस्तेमाल किया जा सकता है

Lean 4 formal proofs के लिए अनुकूलित model

  • Leanstral 1.5 Lean 4 formal proof engineering model का updated version है
  • इसके मुख्य optimization targets automated theorem proving और automated formalization हैं
  • model identifier labs-leanstral-1-5 के रूप में उपलब्ध है

Model scale और basic attributes

  • parameter configuration 119B total parameters, 6.5B active के रूप में दिखाया गया है
  • context length 256k है
  • pricing item $0 दिखाया गया है
  • release category Labs v1.5 है

Conversation, agent और structured output APIs

Document processing, code completion और embeddings

Safety, audio और batch processing

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 3 시간 전
Hacker News की राय

  • जिज्ञासा में साइन अप किया, अकाउंट में पैसे डाले, इस्तेमाल करने की कोशिश की तो चला ही नहीं। Labs मॉडल बताया गया था, इसलिए Labs ऑन करने की कोशिश की, तो इस बार unknown error आ गया। निर्देशों के मुताबिक customer support से संपर्क करना चाहा, तो customer support था ही नहीं, बस जल्दबाज़ी में बनाया हुआ FAQ था
    FAQ ऐसा लग रहा था जैसे vibe coding से बनाया गया हो और search भी बेहद खराब था; कोई भी query डालो, बिल्कुल असंबंधित जवाब ही मिलता था। फिर समझ आया: अगर AI customer support में अच्छा है, तो AI कंपनियां अपने AI से customer support क्यों नहीं देतीं?

    • असल में इस्तेमाल करती हैं। उदाहरण के लिए Cursor है। पुरानी चर्चा “Cursor IDE support hallucinates lockout policy, causes user cancellations” देख सकते हैं[1]
      [1]: https://news.ycombinator.com/item?id=43683012
    • किसी ने यह नहीं सोचा था कि AI customer support में अच्छा है। वह बस सस्ता customer support बनाता है, और पहले से ही कई कंपनियों को support quality की परवाह नहीं है, इसलिए वे खराब support देती आई हैं; उन्हें यह अच्छा लगता है कि लागत और घट सकती है
      उन कंपनियों के नजरिए से यह “अच्छा” customer support है जिन्हें असली समस्या ठीक करने पर पैसा खर्च करना खलता है
    • यह comment पढ़कर हंसी भी आई और थोड़ा भावुक भी हो गया। बहुत EU-जैसा लगा। एक EU enterprise contract जीतने में 18 महीने लगे, और आज sign करके वापस भेजा तो auto-reply आया: “माफ़ कीजिए, लेकिन हम जुलाई के अंत तक छुट्टी पर हैं...”
      पिछले एक साल में इस व्यक्ति से संपर्क के दौरान मिला यह चौथा vacation auto-reply है
    • अजीब और निराशाजनक है, लेकिन मैंने कभी कोई payment method लिंक नहीं किया, फिर भी मैं यह मॉडल मुफ्त में इस्तेमाल कर सकता हूं
    • ये लोग email का जवाब नहीं देते। qwant के साथ भी यही था
      sample size सिर्फ दो है, लेकिन इससे यह मानने का मन होता है कि फ्रांसीसी कंपनियां अंग्रेज़ी में संपर्क किए जाने को खास पसंद नहीं करतीं

  • थोड़ा अलग मुद्दा है, लेकिन यह काफी दुखद है कि EU के पास वास्तविक frontier LLM market में कुछ भी नहीं है। खासकर हाल में अमेरिका ने सचमुच frontier models तक पहुंच पूरी तरह सीमित कर दी, इसे देखते हुए और भी
    क्या यह सिर्फ funding और infrastructure की कमी की वजह से था?

    • Mistral जिन क्षेत्रों में लड़ने का फैसला करता है, उनमें आम तौर पर जीत रहा है, और फिलहाल उसी की जरूरत है
      यह देखने के बजाय कि पूरी EU economy frontier models में कितना योगदान दे सकती है, French economy कितना योगदान दे सकती है, इसे देखना और अमेरिका या चीन से तुलना करना ज्यादा सटीक है। scale नहीं बनता। इसके बजाय यह देखना बेहतर है कि उस कम scale में वे क्या कर पाते हैं, और Leanstral, Voxtral जैसे niche products उसी के नतीजे हैं
    • मोटे तौर पर सही है
      France और Germany EU की सबसे बड़ी economies हैं; France में Mistral है, और Germany में government-backed venture-capital जैसी एक संस्था है। वह संस्था बहुत गर्व से बता रही है कि वह European researchers को sovereign models में नया frontier हासिल करने में मदद करने के लिए पूरे 125 million euros (<150 million dollars) दे रही है[1]
      वह पैसा भी किसी एक winner को नहीं, बल्कि कई recipients में बंटेगा। first step के तौर पर अच्छा है, लेकिन सच कहें तो यह 3–4 साल पहले होता तो first step कहलाता। वाकई अफसोसजनक
      [1] (German) https://www.sprind.org/worte/magazin/verkuendung-next-fronti...
    • Software कुल मिलाकर, और AI भी, rich-get-richer market है। American big tech कंपनियों के पास European talent और उभरती European companies को समेट लेने की क्षमता है, और वे सच में ऐसा करती हैं। अगर खरीदना न चाहें, तो pricing से दबाकर bankrupt भी कर सकती हैं
      हम ऐसी colonial economy में रह रहे हैं जहां human capital raw material है, और वह सब अमेरिका की ओर बहता है। इससे बचना है तो मौजूदा game छोड़ना होगा और China की तरह proper industrial policy से competitive industries बनानी होंगी। पिछले कई दशकों में ऐसी इच्छाशक्ति नहीं दिखी, लेकिन Trump ने state की वापसी बहुत साफ दिखा दी है और Europe भी धीरे-धीरे इसे मान रहा है
    • Mistral ने $4 billion से ज्यादा raise किया है, इसलिए यह काफी बड़ा पैसा है, लेकिन OpenAI/Anthropic/xAI के स्तर का नहीं
      मुश्किल हिस्सा pure LLM development को financially justify करना है। Models एक-दूसरे से बहुत मिलते-जुलते हैं। OpenAI ने शुरुआत में खुद को pure research के लिए “charity” बताकर justify किया, और Anthropic यह कहते हुए अलग हुआ कि OpenAI safety पर पर्याप्त ध्यान नहीं दे रहा। Elon ने कहा कि अगर वह Grok नहीं बनाएगा तो AI woke होने का नाटक करेगा और truthful नहीं होगा, और Google ने Gemini इसलिए बनाया क्योंकि शुरुआत मूल रूप से उन्हीं से हुई थी और AI research Larry और Sergey द्वारा founding के समय दी गई core mission थी। हालांकि financial reasons से उन्होंने इसे कुछ समय तक ठंडे बस्ते में रखा था
      Chinese models की motivation सच कहूं तो स्पष्ट नहीं है। कोई अच्छा explanation नहीं देखा, सिर्फ hypotheses देखी हैं। लेकिन वे free में release करते हैं या बहुत ज्यादा cheap देते हैं, इसे देखते हुए उनकी motivation भी financial नहीं लगती
      दूसरी तरफ Mistral एक सामान्य company है। उसके पास कोई अमीर patron नहीं है जो cosmic destiny जैसी narrative में विश्वास करके पैसा उड़ाए, इसलिए उसे अपने काम को return on investment से justify करना पड़ता है। तब बड़े पैमाने पर LLM training लगभग बाहर हो जाती है
      EU regulations को भी consider करना होगा। पहले जब मैंने देखा था, तो European tech industry की संभावना खत्म करने वाले कई अजीब rules थे। UK में तो यह rule भी था कि internet को केवल research purposes के लिए crawl किया जा सकता है
      https://knowledgerights21.org/news-story/the-uks-copyright-l...
      और First Amendment न हो तो model ने जो कहा उसके कारण prosecution का risk कहीं ज्यादा है। Germany ने search results page में model द्वारा डाली गई सामग्री के लिए Google को court में घसीटा था, वह case देख लें
      इसलिए profits अस्पष्ट हैं और legal risk बहुत बड़ा है
    • EU में ठीक से काम करने वाला single market नहीं है, खासकर capital markets में। आबादी अमेरिका से ज्यादा और total economy बड़ी होने पर भी, अगर resources को efficiently pool नहीं कर सकते तो उसका ज्यादा मतलब नहीं
      क्या Europe में किसी नए lab के लिए $100 billion raise करना संभव है? अगर नहीं, तो खेल खत्म है और छोड़ देना चाहिए

  • क्या संयोग है। आज सुबह ही OpenATP रिलीज़ किया है। OpenATP agentic automated theorem proving के लिए एक open source Python package और CLI है
    इसमें Mistral के Vibe harness के ज़रिए Leanstral support भी शामिल है। पिछला production Leanstral model 22 मई को deprecate हो गया था, और package को Leanstral 1.5 की ओर point कराने के लिए जल्द से जल्द update करूँगा
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com

  • 404 है क्या?
    https://web.archive.org/web/20260630223430/https://docs.mist...

  • weights policy ठीक से समझ नहीं आ रही। इस site पर weights Apache license के तहत बताए गए हैं, इसलिए ये public weights जैसे लगते हैं, लेकिन download link नहीं मिल रहा
    Hugging Face profile पर लगता है सिर्फ पुराना snapshot उपलब्ध है[0]। क्या किसी को पता है कि weights download किए जा सकते हैं या नहीं, और अगर हाँ तो कहाँ से?
    [0] https://huggingface.co/mistralai/Leanstral-2603

  • मुझे भी “Page not found” दिख रहा है। क्या आप access कर पाए? इसमें क्या लिखा है?

    • Web Archive के मुताबिक: Leanstral 1.5 - 30 जून 2026
      automated theorem proving और auto-formalization के लिए optimized updated Lean 4 formal proof engineering model है। कुल 119B parameters, active 6.5B
      https://web.archive.org/web/20260630223430/https://docs.mist...

  • Leanstral 1 पर चर्चा: https://news.ycombinator.com/item?id=47404796

  • Lean 4 और Idris 2 underrated हैं, और extra guarantees देते हैं, इसलिए LLMs के लिए coding में बहुत अच्छे साबित हो सकते हैं

  • अभी 404 दिख रहा है

  • इसी खबर की वजह से sign up किया, लेकिन “Code” इस्तेमाल करने के लिए GitHub connection करना पड़ता है? बहुत restrictive लग रहा है