Leanstral 1.5

 (docs.mistral.ai)
1 puan yazan GN⁺ 3 시간 전 | 1 yorum | WhatsApp'ta paylaş
  • Leanstral 1.5, Lean 4 biçimsel ispat mühendisliğine odaklanan güncellenmiş bir model olup otomatik teorem ispatı ve otomatik biçimselleştirmeyi hedefler
  • Model ölçeği, toplam 119B parametre ve 6.5B aktif parametre yapısından oluşur; uzun ispat ve belge bağlamlarını işlemeyi temel alır
  • Sunulan tanımlayıcı labs-leanstral-1-5 olup, belgelerde Labs v1.5 modeli olarak gösterilir
  • Bağlam uzunluğu 256k olup fiyat kalemi $0 olarak listelenmiştir; bu da deney ve değerlendirme amaçlı erişilebilirliği vurgular
  • Chat Completions, function calling, agents, structured outputs, OCR, Document QnA, FIM, embeddings, moderations, audio ve batch processing API'leriyle birlikte kullanılabilir

Lean 4 biçimsel ispatına uyarlanmış model

  • Leanstral 1.5, Lean 4 biçimsel ispat mühendisliği modelinin güncellenmiş sürümüdür
  • Temel optimizasyon hedefleri otomatik teorem ispatı ve otomatik biçimselleştirmedir
  • Model tanımlayıcısı labs-leanstral-1-5 olarak sunulur

Model ölçeği ve temel özellikler

  • Parametre yapısı 119B total parameters, 6.5B active olarak belirtilir
  • Bağlam uzunluğu 256k'dir
  • Fiyat kalemi $0 olarak gösterilir
  • Sürüm sınıflandırması Labs v1.5'tir

Diyalog, agent ve structured output API'leri

Belge işleme, kod tamamlama ve embeddings

Güvenlik, ses ve batch processing

İlgili okumalar

1 yorum

 
GN⁺ 3 시간 전
Hacker News görüşleri

  • Merakımdan kaydoldum, hesaba para yükledim ve kullanmayı denedim ama çalışmadı. Labs modeli olduğu söylendiği için Labs’ı açmaya çalıştım, bu kez de bilinmeyen hata verdi. Yönergede söylendiği gibi müşteri desteğine ulaşmaya çalıştım ama müşteri desteği yoktu, sadece alelacele hazırlanmış bir FAQ vardı
    FAQ sanki vibe coding ile yapılmış gibiydi ve arama da berbattı; ne sorgu girsem tamamen alakasız yanıtlar veriyordu. Sonra şunu fark ettim: Yapay zeka müşteri desteğinde bu kadar iyiyse, neden yapay zeka şirketleri kendi yapay zekalarıyla müşteri desteği sunmuyor?

    • Aslında kullanıyorlar. Mesela Cursor var. Eski tartışma olan “Cursor IDE support hallucinates lockout policy, causes user cancellations” başlığına bakabilirsiniz[1]
      [1]: https://news.ycombinator.com/item?id=43683012
    • Kimse yapay zekanın müşteri desteğinde iyi olduğunu düşünmüyordu. Sadece ucuz müşteri desteği sağlıyor ve zaten pek çok şirket müşteri desteğinin kalitesiyle ilgilenmediği, uzun süredir berbat destek sunduğu için maliyeti daha da düşürebilme fikrini seviyor
      Gerçek sorunu çözmek için para harcamak zorunda kalmaktan hoşlanmayan şirket açısından bakınca bu “iyi” müşteri desteği sayılıyor
    • Bu yorumu görünce hem güldüm hem içim burkuldu. Fazlasıyla AB işi hissettiriyor. Bir AB şirketi sözleşmesi almak 18 ay sürdü; bugün imzalayıp geri gönderdim, ardından “Üzgünüz, temmuz sonuna kadar tatildeyim...” otomatik yanıtı geldi
      Son 1 yılda bu kişiyle yazışırken aldığım tatil otomatik yanıtlarının dördüncüsü bu oldu
    • Garip ve sinir bozucu ama ben ödeme yöntemi hiç bağlamamış olmama rağmen bu modeli ücretsiz kullanabiliyorum
    • Bunlar e-postalara yanıt vermiyor. qwant da aynıydı
      Örneklem sadece iki şirket ama Fransız şirketlerinin İngilizce iletişim kurulmasından pek hoşlanmadığını düşünmeye başlıyor insan

  • Biraz farklı bir konu ama AB’nin gerçek en ileri LLM pazarında hiçbir şeye sahip olmaması epey üzücü. Özellikle de son dönemde ABD’nin gerçekten en ileri modellere erişimi tamamen kısıtladığını düşününce daha da öyle
    Bu tamamen finansman ve altyapı eksikliğinden mi kaynaklanıyordu?

    • Mistral, mücadele etmeyi seçtiği alanlarda çoğunlukla kazanıyor ve şu an ihtiyaç duyulan da bu
      Burada ABD ya da Çin’le karşılaştırırken AB ekonomisinin tamamının en ileri modellere ne kadar katkı sunabileceğine değil, Fransız ekonomisinin ne kadar katkı sunabildiğine bakmak daha doğru olur. Ölçek yetmiyor. Bunun yerine bu daha küçük ölçekle neler başarabildiklerine bakmak gerekir; Leanstral ve Voxtral gibi niş ürünler bunun sonucu
    • Genel olarak doğru
      Fransa ve Almanya AB’nin en büyük iki ekonomisi; Fransa’da Mistral var, Almanya’da ise devlet destekli bir girişim sermayesi kurumu bulunuyor. Bu kurum, Avrupalı araştırmacıların egemen modellerde yeni bir son teknoloji seviyesine ulaşmasına yardımcı olmak için tam 125 milyon avrodan (<150 milyon dolar) söz etmekle çok gurur duyuyor[1]
      Üstelik bu para tek bir kazanana gitmeyecek, birden fazla alıcı arasında bölünecek. İlk adım olarak güzel ama aslında bu ancak 3-4 yıl önce bir ilk adım sayılabilirdi. Gerçekten yazık
      [1] (Almanca) https://www.sprind.org/worte/magazin/verkuendung-next-fronti...
    • Genel yazılım pazarı da, yapay zeka da kazanan her şeyi alır türü pazarlar. ABD’li büyük şirketlerin Avrupa’daki yetenekleri ve yükselen Avrupa şirketlerini süpürüp alma gücü var ve gerçekten de bunu yapıyorlar. Satın almak istemezlerse fiyat kırarak batırabilirler de
      İnsan sermayesini hammadde olarak kullanan bir sömürge ekonomisinde yaşıyoruz ve bütün bunlar ABD’ye akıyor. Bundan kaçınmak için bugünkü oyunu bırakıp, Çin’in yaptığı gibi ciddi bir sanayi politikasıyla rekabetçi sektörler inşa etmek gerekir. Son birkaç on yıldır buna yönelik bir irade yoktu ama Trump devletin geri dönüşünü çok net gösteriyor ve Avrupa da bunu yavaş yavaş kabul ediyor
    • Mistral 4 milyar doların üzerinde yatırım topladı, yani oldukça büyük bir para ama OpenAI/Anthropic/xAI düzeyinde değil
      Zor olan kısım, saf LLM geliştirmeyi finansal açıdan gerekçelendirmek. Modeller birbirine çok benziyor. OpenAI bunu başlangıçta saf araştırma için kurulmuş bir “hayır kurumu” anlatısıyla gerekçelendirdi; Anthropic ise OpenAI’nin güvenliği yeterince önemsemediğini söyleyerek ayrıldı. Elon, Grok’u yapmazsa yapay zekanın uyanıkmış gibi yapıp dürüst olmayacağını söyledi; Google’ın Gemini’yi yapmasının nedeni de baştan beri çıkış noktalarının bu olması ve yapay zeka araştırmasının Larry ile Sergey’nin kurarken verdikleri temel görevlerden biri olmasıydı. Sadece finansal nedenlerle bir süre beklettiler
      Çin modellerinin motivasyonuysa açıkçası belirsiz. İyi bir açıklama görmedim, sadece varsayımlar gördüm. Ama ücretsiz sunmaları ya da aşırı ucuza vermeleri, motivasyonlarının finansal olmadığını düşündürüyor
      Buna karşılık Mistral sıradan bir şirket. Kozmik kader gibi bir anlatıya inanıp para saçan zengin destekçileri olmadığı için yaptığını yatırım getirisi ile gerekçelendirmek zorunda. Bu da büyük ölçekli LLM eğitimini neredeyse devre dışı bırakıyor
      AB düzenlemelerini de hesaba katmak gerek. Daha önce baktığımda Avrupa teknoloji sektörünün potansiyelini öldüren tuhaf kurallar vardı. Birleşik Krallık’ta interneti sadece araştırma amacıyla taramaya izin veren bir düzenleme bile vardı
      https://knowledgerights21.org/news-story/the-uks-copyright-l...
      Ayrıca Birinci Değişiklik benzeri bir koruma olmayınca, modelin söylediği şeyler yüzünden yargılanma riski çok daha büyük. Almanya’nın, arama sonuçları sayfasında modelin eklediği içerik yüzünden Google’ı mahkemeye vermesi buna örnek
      Bu yüzden getirisi belirsiz, hukuki riski ise çok büyük
    • AB’de gerçek anlamda bir ortak pazar yok, özellikle de sermaye piyasalarında. Nüfus ABD’den fazla, toplam ekonomi daha büyük olsa da kaynakları verimli biçimde bir araya getiremiyorsanız bunun pek anlamı kalmıyor
      Avrupa’da yeni bir laboratuvar için 100 milyar dolar toplamak mümkün mü? Değilse iş bitmiştir, vazgeçebilirsiniz

  • Ne tesadüf. Bu sabah OpenATP’yi yeni duyurdum. OpenATP, ajan tabanlı otomatik teorem ispatlayıcılar için açık kaynaklı bir Python paketi ve CLI
    Ayrıca Mistral’ın Vibe harness’i üzerinden Leanstral desteği de içeriyor. Önceki prodüksiyon Leanstral modeli 22 Mayıs’ta kullanımdan kaldırıldı ve paketi mümkün olduğunca hızlı şekilde Leanstral 1.5’i işaret edecek biçimde güncellemeyi planlıyorum
    GitHub: https://github.com/henryrobbins/open-atp
    Belgeler: https://open-atp.henryrobbins.com

  • 404 mü?
    https://web.archive.org/web/20260630223430/https://docs.mist...

  • Ağırlık politikasını pek anlayamadım. Bu site, ağırlıkların Apache lisanslı olduğunu söylediği için açık ağırlıkmış gibi görünüyor, ama bir indirme bağlantısı bulamıyorum
    Hugging Face profilinde yalnızca önceki anlık görüntüler sunuluyor gibi görünüyor[0]. Ağırlıkları indirmenin mümkün olup olmadığını, mümkünse nereden alınacağını bilen var mı?
    [0] https://huggingface.co/mistralai/Leanstral-2603

  • Bende de “Page not found” çıkıyor. Erişmeyi başaran oldu mu? Bu ne anlatıyor?

  • Leanstral 1 hakkındaki tartışma: https://news.ycombinator.com/item?id=47404796

  • Lean 4 ve Idris 2 yeterince değer görmüyor; sundukları ek güvenceler nedeniyle LLM’lerin kod yazması için muhtemelen çok uygunlar

  • Şu anda 404 veriyor

  • Bu haber yüzünden kaydoldum; “Code”u kullanmak için GitHub bağlantısı yapmak mı gerekiyor? Fazlasıyla kısıtlayıcı görünüyor