Kimina-Prover Model Ailesi Test Zamanı Pekiştirmeli Öğrenme Araması ile Tanıtıldı
Kaynak: huggingface.co ·
Numina ve Kimi Ekibi, Qwen2.5-72B temel alınarak geliştirilen ve Test Zamanı Pekiştirmeli Öğrenme Arama çerçevesiyle eğitilen Kimina-Prover-72B modelini duyurdu. Bu model ailesi, Qwen3 tabanlı 8B ve 1.7B'lik damıtılmış sürümleri de içeriyor. Sistem; aracı tabanlı lemma keşfi, hata düzeltme yetenekleri ve özyinelemeli ayrıştırma ile matematiksel teoremleri kanıtlama yeteneğini artırıyor. Bu yenilikler sayesinde model, karmaşık matematik problemlerini çözmekte ve miniF2F kıyaslama testinde başarı sağlamaktadır.
Neden önemli?
Bu geliştirme, otomatik teorem kanıtlama süreçlerinde tek adımlı akıl yürütmenin ötesine geçerek uzun vadeli ve çok aşamalı stratejilerin uygulanmasını sağlar. Matematikçiler, araştırmacılar ve yazılım geliştiriciler için resmi mantıksal kanıtların oluşturulmasında örnek verimliliğini ve başarı oranını önemli ölçüde artırır.
Bununla neler yapılabilir?
- Olası kullanım: Lean 4 dilinde yazılmış karmaşık matematiksel teoremlerin otomatik olarak biçimsel kanıtlarının oluşturulması ve doğrulanması
- Olası kullanım: Derleyici hata mesajlarının okunarak hedefli düzeltmelerin önerilmesiyle kanıt denemelerinin optimize edilmesi
- Olası kullanım: Doğrudan kanıt gerektirmeyen kombinatorik matematik problemlerinde iki aşamalı çıkarımla hem doğru yanıtın türetilmesi hem de kanıtlanması
Somut sonuçlar ve kanıtlar
- miniF2F kıyaslama testinde Kimina-Prover, tam Test Zamanı Pekiştirmeli Öğrenme arama çerçevesi uygulandığında %92.2 oranında teorem kanıtlama başarısı elde etmiştir. (Üreticinin açıklaması)
- 16 deneme ve ardından hata düzeltme adımı içeren 16+16 stratejisi, 32 bağımsız denemeden oluşan 32×1 kaba kuvvet karşılaştırma düzeyine kıyasla %35.6 başarı oranı sağlamıştır. (Üreticinin açıklaması)
Sınırlar ve açık kalan sorular
Mevcut örnekleme bütçesinin önemli bir kısmı yararlı olmayan veya gereksiz lemmaların kanıtlanmasına harcanmaktadır; bu durum gelecekteki sürümlerde optimizasyon gerektirir. Örnekleme bütçesi pass@1024 sınırını aştığında azalan verim gözlemlenmiştir.