Leanstral 1.5: Herkes için kanıt bolluğu

 (mistral.ai)
1 puan yazan GN⁺ 4 시간 전 | 1 yorum | WhatsApp'ta paylaş
  • Biçimsel doğrulamayı gerçek geliştirme işlerine daha yakın kullanma eğilimi içinde, Mistral AI, Lean 4 için Apache-2.0 lisanslı Leanstral 1.5 modelini duyurdu
  • Model, toplam 119B parametrenin yalnızca 6B’sini etkinleştiriyor; ara eğitim, gözetimli ince ayar ve CISPO pekiştirmeli öğrenme süreçlerinden geçerek kanıt yazımı ile kod deposu görevlerini birlikte öğreniyor
  • miniF2F %100, PutnamBench 587/672, FATE-H %87, FATE-X %34 sonuçlarıyla matematiksel kanıt kıyaslamalarında ve gerçek kanıt mühendisliği değerlendirmelerinde güçlü performans gösteriyor
  • Gerçek kod doğrulamasında AVL ağacının O(log n) zaman karmaşıklığı kanıtı ve Rust-to-Lean hattı üzerinden 57 depoda 11 gerçek hata buldu
  • Ağırlıklar ve ücretsiz leanstral-1-5 API’si yayımlandı; böylece teorem ispatı, kanıt hata ayıklama ve depo katkısı gibi pratik kanıt mühendisliği işlerine doğrudan uygulanabiliyor

Leanstral 1.5’in duyurusu ve model özellikleri

  • Leanstral 1.5, Lean 4 üzerinde kanıt mühendisliği yapmak için oluşturulmuş bir modeldir
  • Lisansı Apache-2.0’dır ve model ölçeği toplam 119B parametre ile 6B etkin parametreden oluşur
  • Biçimsel doğrulama performansını yükselterek yalnızca matematik kıyaslamalarında değil, gerçek kod özelliklerinin doğrulanmasında da kullanılabilir
  • miniF2F’yi doyuma ulaştırdı, PutnamBench’teki 672 sorunun 587’sini çözdü ve FATE-H’te %87, FATE-X’te %34 elde etti

Kanıt geri bildirimini öğrenen 3 aşamalı eğitim

  • Eğitim, ara eğitim, gözetimli ince ayar ve CISPO tabanlı pekiştirmeli öğrenmeden oluşan 3 aşamadan meydana geliyor
  • Pekiştirmeli öğrenmede iki ortam kullanılıyor
    • Çok turlu ortam: Model bir teorem önermesi alıp bunu ispatlıyor ya da çürütüyor ve Lean derleyicisinin geri bildirimine göre kanıtı tekrar tekrar düzeltiyor
    • Kanıt derlenirse başarılı sayılıyor; aksi halde problem çözülene veya bütçe tükenene kadar döngü sürüyor
    • Kod ajanı ortamı: Ham dosya sistemi üzerinde bir geliştirici gibi dosyaları düzenliyor, bash komutları çalıştırıyor ve Lean language server ile hedef, hata ve tür bilgilerini gerçek zamanlı görüyor
  • Kod ajanı ortamı, depo içindeki kısmi kanıt tamamlama, yardımcı lemma yazma ve birden çok bağlam sıkıştırmasından sonra bile sürdürülen uzun görevleri ele alıyor
  • Nihai doğruluk, hedef teorem listesine göre Mistral’in SafeVerify fork’u üzerinde doğrulanıyor

Matematik ve kanıt mühendisliği kıyaslamaları

  • Değerlendirmede miniF2F, PutnamBench, FATE-H/FATE-X ve FLTEval kullanılıyor
    • miniF2F, temel düzey sorulardan IMO seviyesindeki sorulara kadar uzanan biçimsel matematik kıyaslamasıdır
    • PutnamBench, Putnam Mathematical Competition’dan 672 sorudan oluşur
    • FATE-H ve FATE-X, sırasıyla yüksek lisans ve doktora düzeyinde soyut cebir kıyaslamalarıdır
    • FLTEval, Fermat’s Last Theorem deposundaki gerçek pull request’lere dayanarak kanıt mühendisliği zorluğunu değerlendirir
  • miniF2F’de hem doğrulama setinde hem test setinde %100 elde edildi
  • PutnamBench ve FATE-H/X’te, doğal dil kanıt kılavuzları olmadan Goedel-Architect, Seed-Prover 1.5 high ve AxProverBase ile karşılaştırıldı
  • FATE-H/X performansı: {b:87,34}
  • FATE-H’te %87, FATE-X’te %34 ile yeni en yüksek performans elde edildi
  • PutnamBench’te Seed-Prover 1.5 high’dan 7 soru daha fazla çözdü ve soru başına maliyet yaklaşık 4 dolar seviyesindeydi
    • Seed-Prover’ın high ayarı soru başına 10 H20-days bütçe kullanıyor ve maliyetin 300 doların üzerinde olduğu tahmin ediliyor
    • Daha üst sıralardaki bazı kanıtlayıcılar doğal dil kanıt kılavuzları alıyor ya da Aleph Prover örneğinde olduğu gibi soru başına 54–68 dolar maliyetli farklı koşullarda çalışıyor

Uzun akıl yürütme bütçesinde ölçeklenebilirlik ve FLTEval

  • Leanstral 1.5, PutnamBench’te token bütçesi arttıkça Pass@8 performansının yumuşak ve tekdüze biçimde yükseldiğini gösteriyor
  • Deneme başına token bütçesinin 25k’den 4M’e çıkarıldığı deneyde çözülen soru sayısı şöyle artıyor
    • 50k token: 44 soru
    • 200k token: 244 soru
    • 1M token: 493 soru
    • 4M token: 587 soru
  • Uzun kanıtlarda durmadan milyonlarca token boyunca akıl yürütmeye, dosya düzenlemeye ve düzeltmeye devam etmesi performans artışına katkı sağlıyor
  • FLTEval de tamamen açık kaynak olarak yayımlandı
  • FLTEval’de Leanstral 1.5, pass@1’i 21.9’dan 28.9’a, pass@8’i 31.9’dan 43.2’ye yükseltti
  • pass@8’deki 43.2 skoru, Opus 4.6’nın 39.6 sonucunu aşıyor ve maliyet yaklaşık yedide bir düzeyinde kalıyor
  • Açık kaynak modeller arasında kendisinden 3 ila 10 kat büyük modellere karşı da daha iyi performans gösteriyor

Gerçek kod doğrulama örnekleri

  • AVL ağacı zaman karmaşıklığı kanıtı

    • AVL ağacı, ekleme ve silme sırasında yeniden dengeleme sayesinde O(log n) yüksekliğini koruyan, kendi kendini dengeleyen bir ikili arama ağacıdır
    • Leanstral 1.5, gerçek bir uygulama üzerinde ekleme ve silmenin O(log n) olduğunu doğruluyor
    • Bu çalışma, ağacın özyinelemeli yapısını yansıtan yapısal tümevarım, monad tabanlı zaman izleme işleme ve yeniden dengeleme yolları için kapsamlı durum analizleri gerektirdi
    • Kanıt, 2,7 milyondan fazla token ve 22 bağlam sıkıştırması boyunca ilerledi
    • Leanstral, TimeM monadının her katmanını sistematik biçimde açarak denetim akışıyla iç içe geçmiş hesaplamayı görünür kılıyor
    • Ekleme için yükseklik birimi başına 48 adımlık ve sabit terime yakın bir sınır kuruyor; ardından yükseklik ile ağaç boyutunu logaritmik ilişkiyle bağlıyor

  • Rust kodunda hata bulma

    • Hata tespiti deneyi, Aeneas’ın Rust kodunu Lean’a dönüştürdüğü ve Leanstral’ın koddan kullanıcı niyetini çıkararak tutarlılık özellikleri ürettiği bir hat üzerinden oluşuyor
    • Leanstral her özelliği 4 kez deneyerek ispatlamaya çalışıyor; hepsi başarısız olursa bu kez olumsuzlamasını yine 4 kez ispatlamayı deniyor
    • 57 depoda 47 ihlal eden özellik işaretlendi ve bunların 11’i gerçek hatalara işaret etti
    • Gerçek hatalardan 5’i daha önce GitHub’da raporlanmamıştı
    • Bir örnek, datrs/varinteger kütüphanesindeki zigzag decoding sign işlevinde bulundu
    • Girdi Std.U64.MAX olduğunda (value + 1) ifadesi taşmaya neden oluyor
    • Debug modunda çökme yaşanıyor, release modunda ise sessiz veri bozulması ortaya çıkıyor
    • Bu uç durum, sıradan testlerin ve fuzzing’in kolayca kaçırabileceği bir örnek

Dağıtım ve kullanım

  • Ağırlıklar Hugging Face üzerinde yayımlandı
  • Ücretsiz API uç noktası, model kartında leanstral-1-5 adıyla sunuluyor
  • Kullanım ortamı olarak Mistral Vibe öneriliyor
  • Başlangıç adımları; Mistral Vibe kurulumu, Leanstral 1.5 kurulumu, ajanı çalıştırma, isteğe bağlı Lean LSP MCP kurulumu ve kanıt görevine başlama sırasından oluşuyor
  • Lean LSP MCP, ~/.vibe/config.toml dosyasına eklenerek kurulması önerilen bir yapıdadır
  • Mevcut bir MCP sunucusu yoksa mcp_servers = [] satırını kaldırmak gerekebilir
  • Leanstral; teorem çözme, kanıt hata ayıklama ve depo katkısı işlerinde kullanılabilir

İlgili okumalar

1 yorum

 
GN⁺ 4 시간 전
Hacker News yorumları

  • Mistral’in büyük modellerle rekabet etmesinin zor olduğuna dair eleştiri haklı, ama bence gerçekte küçük modellerde belirli işlevleri yüksek kalitede sunmaya odaklanıyor
    OCR veya dosya analizi gibi işler için Mistral kullanıyorum; hesaba 100 dolar koyunca istek hacmi derdi olmadan 1 yıl idare ediyor
    Maliyeti son derece düşük olduğu için, Opus 4.8 ile rekabet edemese bile yeterince değerli

    • OCR’de gerçekte ne kadar rekabetçi olduğunu merak ediyorum
      Düşük fiyata makul kalite, daha sonra hataları azaltmak için 10 katını ödeyip en yüksek kaliteyi kullanmaktan daha niş bir pazar gibi görünüyor
    • Avrupalı aptallar, parayı azami düzeyde kazanmak için değil iyi ürün yapmak için optimizasyon yapıyor /s
    • “Yılda 100 doların altında 1 yıllık belge işleme”nin düşünüldüğü kadar harika olduğundan pek emin değilim. En azından Avrupa rekabet gücü açısından Mistral’in gelir tavanını çok düşük belirlediği anlamına geliyor
      OCR zaten neredeyse metalaşmış durumda; açık kaynak modellerde veya AWS gibi yerlerde de temel olarak sunuluyor
      Üstelik yıllık 100 dolarlık fiyat etiketiyle sadakat yaratmak zor; geçiş maliyeti de yok, daha düşük fiyat çıkarsa müşteri hemen ayrılabilir
      Kolayca kopyalanabilen düşük maliyetli bir araçta müşteri kilidi yoksa bu, işten çok bir özellik gibidir
      Alıcı açısından iyi olabilir, ama bir Avrupa şirketinin uzun vadede küresel rakiplerle ürün yetkinliği üzerinden rekabet etmesini istiyorsak kötü bir strateji gibi görünüyor

  • Çalışmanın kendisi iyi, ama hata bulma örneği tuhaf geldi
    zigzag kod çözmedeki sign fonksiyonunda Std.U64.MAX girdisinde (value + 1) taşma yapıyor; debug modunda çökme, release modunda ise sessiz bozulma olduğu söylenmiş. Buna testlerin “genellikle kaçırdığı” bir sınır koşulu denebilir mi bilmiyorum
    Kötü testlerse kaçırır, ama dikkatli bir insan ya da makine öğrenmesi tabanlı bir kodlama sistemi “uç değerleri test etmeliyim” konusunda epey iyidir. Özellikle kullanıcı girdisini ayrıştıran kodlarda daha da öyle
    Daha ilginç hatalar da bulmuşlar ama hızlı anlatması zor olduğu için bu örneği mi verdiler, merak ediyorum

    • Özellikle “fuzzing de kaçırır” kısmı tuhaf. Benim gördüğüm fuzzing genelde sınır değerleri bilinçli olarak araştırır
      Böyle bir kodlama kütüphanesinde iyi koddan temel beklenti fuzzing olur; neredeyse kesinlikle birkaç saniye içinde yakalanırdı diye düşünüyorum
      Gerçekten de proptest ile çok basit bir gidiş-dönüş testi yazınca 1 saniye bile geçmeden onlarca hata ve aşağıdaki sonuç çıktı:
      thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:
      Test failed: attempt to multiply with overflow.
      minimal failing input: value = 4611686018427387904
      successes: 2
      local rejects: 0
      global rejects: 0
    • “Genelde kaçırılır” demek zor olabilir, ama gerçekten var olduğuna göre bazen kaçırılan bir hata olduğu doğru
      Lean kullanınca hangi örnekleri test etmek gerektiğini zekice seçme ihtiyacının azalması avantajı ortaya çıkıyor
    • Bu temel kalite güvencesi. Testler böyle bir şeyi kaçırıyorsa, normalde beklediğimizden çok daha sınırlı faydaya sahiptir
      Yazarların geçmişini merak ettim
    • Bu düpedüz kötü tanıtım
      1980 civarında icat edilen tüm özellik tabanlı test sistemleri sınır değerleri araştırır
      C ve C++ semantiği, ya da semantiğin yokluğu, gerçek testleri zorlaştırabilir. Çünkü derleyicinin tanımsız davranışa yol açan tüm girdiler için “test geçti” demesine izin verilebilir

  • Yazının ortasında çeşitli en ileri düzey LLM’lerle karşılaştırmalar var, ama hepsi yarım yıl önceki modeller
    “Yeni modelimiz 3 nesil önceki Çin modellerinden daha iyi” der gibi, epey komikti

    • Bu 6 milyar parametreli bir model, yani tamamen farklı bir sınıf. Asıl “en ileri düzey küçük dil modeli” beklentisi daha yerinde
    • Katılıyorum, ama açık ağırlıklı ve nispeten küçük olması bile başlık değeri taşıyor. Bu model epey iyi çalışıyor

  • Söz konusu kütüphane https://github.com/datrs/varinteger
    Makale yayımlanmadan bir hafta önce aynı sorun bu depoya zaten açılmış, muhtemelen doğru olan bu: https://github.com/datrs/varinteger/issues/8
    Bu kişinin Leanstral çalışanı mı olduğunu, yoksa Leanstral’in bu issue’yu öylece mi aldığını bilmiyorum
    Bu kütüphane küçük, testleri şaşırtıcı derecede zayıf ve 8 yıldır neredeyse hiç ellenmemiş: https://github.com/datrs/varinteger/blob/master/tests/test.r...
    İndirmeleri günde yaklaşık 1 bin civarında, düşük gibi görünüyor: https://crates.io/crates/varinteger
    Bu yüzden tek örnek olarak öne çıkarılacak kadar büyük bir başarı olduğunu söylemek zor. Otomatik tespitin faydalı olduğu doğru, ama bu alt alanda kayda değer bir başarı mı emin değilim
    Kanıt yazan LLM hiç kullanmadım, ama eğitim verisi görece az olduğundan genel kodlama modellerinden daha kaba olmasına şaşırmam
    Bu arada https://crates.io/crates/varinteger üzerinde https://github.com/mafintosh/varinteger-rs olarak görünüyor, ama bu adres https://github.com/datrs/varinteger adresine yönlendiği için, göründüğünün aksine aynı kütüphane gibi duruyor

    • Kanıtın sorunu, değerini aktarmanın bazen zor olması
      Esas nokta hata bulmak değil, belirli türde hataların belirli varsayımlar altında olmadığını kanıtlamak
      Ama bu hikâyeyi satmak zor olduğundan pazarlama sık sık “bu hatayı buldu” tarafına kayıyor

  • Lean’ı hiç bilmeyen biri için de yararlı olabilir mi? Üzerinde çalıştığım yazılımı doğrulamak istiyorum ama biçimsel doğrulama deneyimim yok
    Yalnızca spesifikasyon, kod ve sınırlı öğrenme süresiyle işe yarar sonuçlar alıp alamayacağımı merak ediyorum

    • Kanıtlamak istediğiniz kısmın kendisini anlamanız gerekir, ama tüm kanıt sürecini anlamanız şart değil
      Matematikten çok Haskell tipleri okumaya daha yakın; sadece kelime dağarcığı büyük ölçüde matematikten ödünç alınmış gibi
    • Yazıdaki “Bug Discovery: Finding Hidden Flaws” bölümünü okursanız, yalnızca Rust koduyla başlayıp açık kaynak Rust’ta sorun bulmak için modeli kullandıkları görülüyor
      Uygulama doğrulaması için Lean kodu yazma konusunda sohbet ederek yardım alınabilir belki, ama bundan emin değilim
    • En azından kod hakkında hangi teoremi kanıtlamak istediğinizi ve bunu Lean’de nasıl ifade edeceğinizi anlamanız gerekir
      Aksi halde çıktıyı doğrulayamazsınız
      Mekanik olarak doğru olduğu kontrol edilmiş bir önermeyi kanıtlamış olabilirsiniz; ama o önermenin ne anlama geldiğini ve gerçekte doğrulamak istediğiniz şeyi kapsayıp kapsamadığını bilmiyorsanız bunun bir anlamı yok
    • Lean4’ü hiç bilmezken yaklaşık 6 ay içinde kodlamamın çoğunu Lean4 ile yapacak düzeye geldim ve bu süreç yapay zeka desteği sayesinde ciddi şekilde hızlandı
      Modellerin Lean4’te ne kadar tutarlı biçimde akıcı olduğuna şaşırıyorum. Sadece en ileri seviye modeller değil, küçük yerel modeller de öyleydi; LLM’ler Lean4’ü doğrudan iyi anlıyor gibi
      Kendime Lean4 uzmanı demek için hâlâ yolum var, ama artık yararlı programlar yapmak için desteğe mutlaka ihtiyaç duymuyorum
      Neredeyse hiç bilgi yokken bile tamamen anlamadığınız kısımlara güvenebilmek öğrenme hızını ciddi ölçüde artırıyor. Eksik bilgiyle de güvenilebilir programlar elde etmek pratik ve motive edici
      Sınırı, ara kanıt adımlarının tamamından ziyade, kendi aksiyomlarınızı ve önermelerinizin yüzeyini açıklayan dil kısmı belirliyor gibi. Zamanla daha fazlasını yapmak için daha fazlasını anlamak gerekiyor, ama bir anlamda N+1 seviyesinde güvenle çalışabiliyorsunuz
      Lean4, teorem kanıtlama rolünden bağımsız olarak da keyifli bir programlama dili ve hızı da şaşırtıcı derecede yüksek
      io_uring ile birlikte kullanıyorum; birçok durumda C++/libuv veya Rust/Tokio’dan çok daha hızlı
      Bazen p99.99 gecikme süresi gibi yerlerde uzun kuyruklar görünürse sayıları sabit genişliğe çevirmek gibi ayarlar yapmak gerekiyor, ama C++ ve Rust’ta da ayar yapmak gerekiyor

  • Lean 4’ün biçimsel doğrulama için öne çıkarılması ilginç
    Bu alanın Isabelle/HOL ve TLA+ tarafında olduğunu sanıyordum
    En azından üçünü de kullanacak şekilde eğitilmiş bir model beklerdim. Doğrusal cebirin ileri yönlü çıkarımları için Isabelle/Isar da daha iyi görünüyor; biri açıklayabilir mi?

    • Lean’in, Isabelle’e veya eski Coq olan Rocq’a kıyasla yazılım doğrulamada daha az benimsendiği doğru
      Bu alanda Agda bile daha fazla kullanılmış sayılır
      Ancak Lean şu anda alternatif olarak kayda değer bir ivme kazanıyor; özellikle de genel amaçlı fonksiyonel programlama dili olma becerisi büyük etken
      Kişisel olarak gereksinimler ile spesifikasyonları eşleştirmesi daha kolay olan Hoare mantığı veya ayırma mantığı tabanlı yaklaşımları daha pratik buluyorum. Dafny ve F* hoşuma gidiyor

  • Twitter duyurusunda geliştiricilerin Le Chaton Fat’e hafifçe değinmesi eğlenceliydi
    Gerçekten Le Chaton Fat’te yer alıp almadıklarından bağımsız olarak, gerçek anlamda “yeni büyük genel amaçlı” bir model yakında gelecek gibi görünüyor
    Medya karmaşasından sonra da doğrudan bahsettiklerine göre beklenti yüksek. Umarım adı “Large 4”ten daha yaratıcı olur

  • En güncel OpenATP’de Leanstral 1.5’i deneyebilirsiniz
    OpenATP, ajan tabanlı otomatik teorem kanıtlayıcılar için açık kaynaklı bir Python paketi ve CLI’dır; Docker’da yerel çalıştırmayı veya Modal sandbox’ında uzaktan çalıştırmayı varsayılan olarak destekler
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com