DeepSeek, 671 Milyar Parametreli Otomatik Teorem İspat Modeli DeepSeek-Prover-V2-671B'yi Açık Kaynak Olarak Yayınladı

Yapay zekâ alanında önemli bir adım atan DeepSeek, yeni matematiksel ispat otomasyon modeli DeepSeek-Prover-V2-671B'yi açık kaynak olarak duyurdu. Hugging Face platformundaki yayınla beraber, model araştırmacılar ve geliştiriciler için erişime açıldı. DeepSeek-Prover-V2-671B, devasa 671 milyar parametrelik Mixture-of-Experts (MoE) mimarisiyle DeepSeek-V3 üzerine inşa edildi ve matematiksel ispatlama konusunda yeni bir çığır açmayı hedefliyor.

Özellikle matematiksel problem çözme ve resmi teorem ispatında özelleşen model, Lean 4 ispat asistanı diliyle sorulara %88,9 başarı oranı (MiniF2F testinde) sağlayarak mevcut yapay zekâ temelli ispatlayıcılara kıyasla yeni bir standart belirledi. Ayrıca DeepSeek-Prover-V2-671B, PutnamBench'te 49/658 problemi çözerek ileri düzey matematiksel zorlukları da aşabildiğini gösterdi.

Model, eğitim materyali olarak kendi oluşturduğu zorlu matematik problemlerinin alt adımlara ayrıldığı ve adım adım çözüldüğü sentetik veri kümeleriyle güçlendirildi. Reinforcement learning (pekiştirmeli öğrenme) ile desteklenen bu yaklaşım, modelin hem teorik hem pratik ispat performansını artırıyor. DeepSeek-Prover-V2-671B, eğitsel ve bilimsel alanlarda; matematik öğretimi, akademik araştırmalar, mühendislik tasarımı ve finansal analiz gibi çeşitli sektörlerde kullanılabiliyor. Yazılım geliştiriciler içinse, algoritma tasarımı ve kod doğrulama işlerinde değerli bir araç sunuyor.

Modelin 7B ve 671B parametreli iki versiyonu, Hugging Face üzerinden indirilebilir ve akademik ya da ticari projelerde açık ve serbest lisansla kullanılabiliyor. Geliştiriciler, Hugging Face'in popüler Transformers kütüphanesiyle hızlıca modelden faydalanabiliyor. DeepSeek, topluluk desteği ve yeni benchmark setleriyle (ProverBench dahil) modelin devamlı güncelleneceğini duyurdu.