Leanstral: Güvenilir kod ve biçimsel ispat mühendisliği için açık kaynak bir ajan

• Lean 4 için tasarlanan ilk açık kaynak kod ajanı; biçimsel ispat (formal proof) süreçlerini otomatikleştirerek insan doğrulama yükünü azaltmayı hedefliyor
• Model ağırlıkları Apache 2.0 lisansı ile yayımlandı ve Mistral Vibe ortamı ile ücretsiz API endpoint üzerinden hemen kullanılabiliyor
• 6B aktif parametreli seyrek bir mimari kullanarak verimlilik ve maliyet tasarrufu sağlıyor; lean-lsp-mcp gibi MCP entegrasyonlarını destekliyor
• FLTEval benchmark'ında Qwen3.5, GLM5, Kimi-K2.5 gibi büyük açık kaynak modellerden daha yüksek puan alırken, Claude Sonnet'e benzer performansı 15 kattan düşük maliyetle sunuyor
• Biçimsel ispat otomasyonu ile kod güvenilirliğinin artırılmasını birleştiren yeni bir yaklaşımla, hem araştırma matematiği hem de görev kritik yazılım geliştirme için kullanım potansiyeli gösteriyor

---

Leanstral genel bakış

• Leanstral, Lean 4 için geliştirilen ilk açık kaynak kod ajanı ve biçimsel ispat yardımcısı (proof assistant) ortamında çalışıyor
  • Lean 4, karmaşık matematiksel nesneleri (ör. perfectoid uzaylar) ve yazılım belirtimlerini ifade edebiliyor
  • Mevcut ispat sistemleri genel model wrapper'larına ya da tekil problemlere odaklanırken, Leanstral gerçekçi biçimsel depolarda (formal repositories) verimli çalışacak şekilde eğitildi
• 6B aktif parametreye sahip seyrek (sparse) bir mimari benimseyerek paralel çıkarımı (parallel inference) Lean'in doğrulama yetenekleriyle birleştiriyor
• MCP entegrasyon desteği sayesinde lean-lsp-mcp gibi yaygın kullanılan protokollerle uyumlu

Yayınlanma ve erişilebilirlik

• Model ağırlıkları Apache 2.0 lisansı ile yayımlandı ve Mistral Vibe içinde ajan modu olarak sunuluyor
• Ücretsiz API endpoint'i (labs-leanstral-2603) üzerinden herkes erişebiliyor; kullanıcı geri bildirimleri toplanarak sonraki model iyileştirmelerinde kullanılacak
• Teknik rapor ve değerlendirme aracı FLTEval birlikte yayımlandı; böylece mevcut matematik odaklı değerlendirmelerin ötesine geçilip gerçek ispat mühendisliği performansı ölçülüyor

Performans değerlendirmesi (Evaluation)

• Değerlendirme, FLT projesindeki Pull Request düzeyinde tüm biçimsel ispatları ve yeni matematiksel kavram tanımlarını tamamlama yeteneğine göre yapıldı
• Karşılaştırılan modeller: Claude Opus 4.6, Sonnet 4.6, Haiku 4.5, Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B

Leanstral ve açık kaynak modeller

• Leanstral-120B-A6B, GLM5'in (16.6 puan) ve Kimi-K2.5'in (20.1 puan) üstünde 26.3 puan (pass@2) aldı
• Qwen3.5, 4 çalıştırmada (pass@4) 25.4 puan alırken Leanstral bunun yarısı kadar çalıştırmayla daha yüksek puana ulaştı
• Aynı maliyet seviyesinde doğrusal biçimde 29.3 puana (pass@4) kadar ölçeklenebiliyor

Leanstral ve Claude ürün ailesi

• Sonnet'e karşı 2.6 puan üstünlük (26.3 puan vs 23.7 puan) gösterirken, çalıştırma maliyeti $36 vs $549 ile 15 kattan fazla daha ucuz
• pass@16 ölçümünde 31.9 puan alarak Sonnet'ten 8 puan daha yüksek sonuç verdi
• En yüksek performanslı model olan Claude Opus 4.6 39.6 puan aldı, ancak maliyeti $1,650 ile Leanstral'ın 92 katı oldu
• Tüm benchmark'lar Mistral Vibe ortamında herhangi bir değişiklik yapılmadan yürütüldü

Model	Maliyet($)	Puan
Haiku	184	23.0
Sonnet	549	23.7
Opus	1,650	39.6
Leanstral	18	21.9
Leanstral pass@2	36	26.3
Leanstral pass@4	72	29.3
Leanstral pass@8	145	31.0
Leanstral pass@16	290	31.9

Vaka incelemeleri (Case Studies)

Lean sürüm değişikliğine uyum

• Lean 4.29.0-rc6'da ortaya çıkan tür takma adıyla ilgili bir StackExchange sorusu girdi olarak verildi
• Leanstral, problem ortamını yeniden üretti ve tanımsal eşitlik (definitional equality) sorununu doğru şekilde teşhis etti
• def yerine abbrev kullanılmasını önererek rw taktiğinin (tactic) yeniden düzgün çalışmasını sağladı
• Sorunun nedenini ve çözümün niçin işe yaradığını kullanıcıya açık biçimde anlattı

Program akıl yürütme ve dönüşüm

• Rocq içindeki program tanımını Lean'e dönüştürdü ve kullanıcı tanımlı gösterimi de uyguladı
• Örnek olarak plus2 komutunun X değişkenine 2 ekleme işlemini yaptığını ispatladı
• Yalnızca verilen Rocq belirtiminden yola çıkarak Lean içinde teoremi (theorem) tamamlayıp ispatı gerçekleştirdi

Kullanım şekli

• Mistral Vibe entegrasyonu: /leanstall komutuyla hemen kullanılabiliyor
• Labs API: ücretsiz ya da düşük maliyetle erişim sağlanabiliyor
• Model indirme: Apache 2.0 lisansı ile doğrudan çalıştırılabiliyor

Önemi

• Leanstral, kod üretimi ile biçimsel ispat otomasyonunu birleştiren ilk açık kaynak girişim
• Araştırma matematiği, doğrulanabilir yazılım geliştirme, yüksek güvenilirlikli sistem tasarımı gibi alanlarda kullanım potansiyeli gösteriyor
• Maliyet verimliliği ve açıklığı aynı anda sunan yeni bir kod doğrulama altyapısı olarak değerlendiriliyor

[GN⁺]

Hacker News görüşleri

• İnsanların artık ajanın istenen davranışını belirtip, buna uygun kod yazdırabildiği örüntüyü fark etmeye başlaması ilginç
  TDD ya da doğrulama araçları gibi hangi yöntem kullanılırsa kullanılsın, zamanla bu tür doğrulama paketleri “nasıl çalışması gerektiğini” gösteren çalıştırılabilir bir dokümantasyon deposu olarak birikiyor
  Bu yaklaşım, basit bir Markdown spesifikasyonundan çok daha güçlü. Çünkü niyeti değil, ayrıntılı davranışı kodla ifade ediyor
  Yazılım karmaşıklaştıkça “onu Jim'e sor” tarzı sözlü aktarımın sınırları ortaya çıkıyor

  • Aradaki farkın çok büyük olmadığını düşünüyorum. Kod da sonuçta .md dosyasına yazılacak bilginin başka bir ifadesi sadece
    Ayrıntı ve bağlam, çözünürlük değişimi sırasında kayboluyor
    TDD ya da doğrulama odaklı geliştirmeye katılıyorum, ama bunu kodla yazmak nihai amaç değil
    Zaten milyonlarca satır test mevcut; gerçekçi olan, bunları temel alarak geliştirmek
  • Yapay zekanın ortaya çıkmasıyla birlikte nihayet TDD'nin hayal ettiği gerçekliğin mümkün hale geldiğini düşünüyorum
  • Bu yaklaşım ilgi çekici ama blog yazısı kafa karıştırıcıydı
    Lean'ın pratikte tam olarak ne sağladığını merak ediyorum.
    Örneğin Lean ile bir durum makinesi kanıtlanıp sonra bunun Dart'a aktarılması gibi mi?
    Lean'ı iyi bilmediğim için bunun ne kadar gerçekçi bir yaklaşım olduğunu kestiremiyorum

• Yakın zamanda Jack Clark'ın (Anthropic kurucu ortağı) ve Ezra Klein'ın podcast'inde de değinildiği gibi, model hizalaması (alignment) göreceli ve çeşitlilik önemli yönünde çok tartışma var
  Mistral'ın modelinin diğer frontier modellere kıyasla geride kaldığını söyleyenler olsa da, farklı hizalama teknikleri ve şirketlerin denenmesi ekosistem için önemli

  • Sonuçta bunu zamanın çözeceğini düşünüyorum

• Gerçek başarı örneği Simon Willison'ın Red Green TDD yaklaşımını hatırlattı
  Leanstral'ın hata ortamını yeniden üreten test kodu üretmesi ve tanımsal eşitlik (definitional equality) sorununu bulması etkileyiciydi

  • Eğer ajan kendi testlerini yazıyorsa, kod ve testleri ayrı ayrı yazmaya kıyasla doğruluk güvencesi daha mı yüksek olur diye merak ediyorum
  • Bence TDD sonuçta prompt engineering ile aynı şey. Çünkü ajana net bir hedef verme süreci bu

• Bu model belirli görevlere uygun şekilde eğitilmiş olsa da Opus'tan daha düşük performans gösteriyor
  Opus 6 kat daha pahalı ama buna değiyor gibi görünüyor

  • Fikir iyi ama sonuçta kalite güvenden önce gelir
    Sermayesi kısıtlı bir Avrupa girişiminin böyle bir nişi hedeflemesini anlıyorum ama bunun büyük gelire dönüşmesi zor görünüyor
  • Benchmark'ların güvenilirliği belirsiz ama pass@2 ya da pass@3 sonuçlarına bakınca izlenim değişiyor
    Bunu Codex gibi modellerle karşılaştırmak daha ilginç olabilir
  • Model açık kaynak ve yerelde çalıştırılabiliyor. Bu oldukça önemli bir nokta değil mi?

• “Güvenilir kod” konseptini sevdim
  Ama karşılaştırma ölçütü kafa karıştırıcı. Haiku'dan daha ucuz olduğu vurgulanıyor ama Haiku zaten bu işte zayıf, Leanstral ise ondan da zayıf
  Hedef doğruluksa, “ucuz ama kötü”nün neden önemli olduğunu anlamıyorum
  Yine de Opus da kusursuz değil; ölçek büyütülürse daha iyi sonuçlar çıkabilir gibi

  • Grafiğe bakınca pass sayısı arttıkça performansın yükseldiği görülüyor
    2 denemede Haiku ve Sonnet'ten daha iyi, 16 denemede ise Opus'a yaklaşırken maliyet verimliliği de yüksek
  • Aslında basit — prompt'a sadece “yalnızca güvenilir çıktı” istemek yeterli

• Lean'ı bilmeyen biri olarak, bunun doğrudan bir değeri olup olmadığını merak ediyorum
  Go gibi dillerdeki koda otomatik olarak ispat mı ekliyor, yoksa sadece açık modellerde çeşitliliği desteklemek mi gerekiyor?

  • Muhtemelen yapı, ajanın Lean4 spesifikasyonları üretip yazılımı bu spesifikasyonlara göre değerlendirmesi şeklinde
    Ama sonuçta Lean4 spesifikasyonunun kendisi de bir yazılım artefaktı haline geliyor
    O zaman tekrar bu spesifikasyonun doğru olup olmadığını doğrulama sorununa dönüyoruz — yani yine insan incelemesi gerekiyor

• Birkaç haftadır bu yönelimi bekliyordum; gerçekten gerçekleştiğini görmek sevindirici
  LLM çağında kodun insan dostu olmasındansa ispatlanabilirlik ve token verimliliği daha önemli hale gelebilir gibi görünüyor
  Lean ile Rust birleştirilerek, “yalnızca ispatlanmış kodun derlendiği” bir dünya gelebilir
  İlgili tartışmayı önceki yorumda özetlemiştim

  • Ancak hiçbir ispat sistemi “doğru ispatı” garanti etmez
    Sadece mantıksal olarak geçerli (valid) olduğunu garanti eder
    Bir ispatın neyi ispat ettiğini tam olarak anlamak, bir programı anlamak kadar zordur; ama bu süreçte düşüncenin derinleşmesi gibi bir fayda da vardır

• “Açık kaynak” ifadesinin sadece lafta kalmayıp gerçekten Apache-2.0 lisanslı ağırlıklar olarak yayımlanmış olması sevindirici

  • Ancak topluluk ölçütlerine göre, model yeniden üretilemiyorsa bu “open weights”tir, “open source” değil

• Mistral resmi haberi'ne göre
  Claude Opus 1.650 dolar maliyetle 39.6 puan alırken,
  Leanstral pass@8 145 dolara 31.0, pass@16 ise 290 dolara 31.9 alıyor;
  maliyet başına performans verimliliği oldukça yüksek