Mistral'ın matematiksel ispat modeli miniF2F testini tamamen çözdü

Bir dil modelinin matematik sorusunu "doğru" cevaplaması ile ispatını biçimsel olarak üretmesi çok farklı iki iş. İkincisinde tahmin yürütmenin yeri yok: ispat ya doğrulayıcıdan geçer ya geçmez. Mistral'ın yayımladığı Leanstral 1.5 bu ikinci işe odaklanıyor.

Model Lean 4 dilinde teorem kanıtlıyor ve yazılım doğrulamasında kullanılıyor. Toplam 119 milyar parametreye sahip, ancak her çağrıda bunun yalnızca 6 milyarı etkin — bu mimari, bu boyutta bir modelin makul maliyetle çalışmasını sağlıyor.

Paylaşılan sonuçlar iddialı. Temel matematikten uluslararası olimpiyat düzeyine uzanan miniF2F kıyaslamasında model hem doğrulama hem test kümesinde yüzde 100'e ulaşıyor, yani testi tamamen doyuruyor. Putnam Matematik Yarışması sorularından oluşan PutnamBench'te 672 problemden 587'si çözülüyor. Lisansüstü düzeyde soyut cebir soruları içeren FATE-H'de yüzde 87, doktora düzeyindeki FATE-X'te yüzde 34 ile yeni bir üst seviye belirleniyor.

Eğitim üç aşamalı: ara eğitim, denetimli ince ayar ve CISPO adı verilen pekiştirmeli öğrenme. Modelin iki farklı ortamda eğitilmesi dikkat çekici. Çok turlu ortamda modele bir teorem ifadesi veriliyor ve ispatlaması ya da çürütmesi isteniyor; model ispatı gönderiyor, Lean derleyicisinden geri bildirim alıyor ve her denemede yaklaşımını düzeltiyor. İspat derlenirse başarılı sayılıyor, aksi hâlde döngü bütçe bitene kadar sürüyor.

İkinci ortam daha ilginç: kod ajanı ortamında Leanstral bir geliştirici gibi çalışıyor. Dosyaları düzenliyor, bash komutları çalıştırıyor ve Lean dil sunucusunu kullanarak hedefleri, hataları ve tip bilgilerini gerçek zamanlı inceliyor. Bu, bir depodaki yarım kalmış ispatları tamamlamak, yardımcı lemmalar kurmak ve birden fazla bağlam sıkıştırma turunda ısrar etmek gibi uzun soluklu görevleri mümkün kılıyor. Sonuçlar şirketin SafeVerify çatallamasıyla doğruluk açısından sınanıyor.

Kâğıt üzerindeki sayılardan daha ilgi çekici olan pratik deneme. Fermat'ın Son Teoremi deposundaki gerçek katkı taleplerine dayanan FLTEval testinde modelin, Opus 4.6'dan yedi kat daha ucuza daha iyi sonuç verdiği belirtiliyor. Ayrıca model 57 açık kaynak deposunda çalıştırılmış ve daha önce bilinmeyen beş hata ortaya çıkarmış.

Leanstral 1.5, Apache 2.0 lisansıyla Hugging Face üzerinde yayımlandı. Ayrıca leanstral-1-5 adıyla ücretsiz bir API uç noktası ve Mistral Vibe üzerinden erişim sunuluyor.