DeepSeek, Matematiksel İspat ve Teorem Çözümünde Çığır Açabilecek Yapay Zekâ Modeli Prover V2’yi Yayımladı

Yapay zekâ teknolojileri her geçen gün gelişirken, genel yeteneklerin yanı sıra belirli uzmanlık alanlarına odaklanan modeller de dikkat çekiyor. Yapay zekâ geliştiricisi DeepSeek, yapay zekânın en zorlu alanlarından biri olarak kabul edilen matematiksel ispat ve teorem çözümüne odaklanan iddialı yapay zekâ modeli Prover‘ın yeni ve geliştirilmiş sürümünü duyurdu: Prover V2.

Prover V2, büyük bir lansman veya etkinlikle değil, yapay zekâ modelleri ve veri kümeleri için popüler bir platform olan Hugging Face üzerinden ‘sessizce’ erişime açıldı. Bu hamle, modelin doğrudan araştırmacılar ve geliştiriciler tarafından keşfedilmesine ve test edilmesine olanak tanıyor.

Prover V2 Neler Sunuyor? Gelişmiş Matematiksel Yetenekler ve Mimari

DeepSeek tarafından geliştirilen Prover V2, adından da anlaşılacağı üzere, karmaşık matematiksel ispatlar yapma ve soyut teoremleri çözme gibi ileri düzey matematiksel akıl yürütme görevlerinde yapay zekânın yeteneklerini zorluyor.

Yeni sürüm Prover V2, önceki versiyonlara kıyasla matematiksel işlemleri gerçekleştirme ve ispat adımlarını takip etme konusunda daha yetenekli ve gelişmiş bir performans sergilemek üzere tasarlandı. DeepSeek, Prover V2’nin yanı sıra, aynı yeteneklere sahip, ancak daha az kaynak gerektiren, daha küçük ve yoğunlaştırılmış bir versiyonunu da Hugging Face platformunda paylaştı. Bu, farklı donanım seviyelerine sahip kullanıcıların da modeli deneyimlemesine imkan tanıyor.

Prover V2 modelinin temelinde, DeepSeek’in daha önce duyurduğu ve genel amaçlı görevlerde yüksek performans sergileyen 671 milyar parametreli güçlü V3 modeli yer alıyor. Ancak Prover V2, matematiksel ispat gibi spesifik ve yapısal görevleri daha etkin çözmek için mimarisinde bir farklılık sunuyor: Görevleri tek bir büyük yapı yerine daha küçük alt modellere bölerek işliyor. Her bir alt model, ispat sürecinin veya teorem çözümünün belirli bir aşamasında veya alanında uzmanlaşarak, genel çözüm yeteneğini ve verimliliğini artırıyor. Bu modüler yapı, modelin matematiksel görevlere daha odaklı ve derinlemesine yaklaşmasını sağlıyor olabilir.

DeepSeek’in Yapay Zeka Yol Haritası: Prover’ın Yeri

DeepSeek, yapay zekâ alanında farklı alanlara yönelik modeller geliştirmeye devam ediyor. Prover model ailesi, en son Ağustos (2024) ayında güncellenmiş ve o dönemde teorem ispatı ve matematiksel akıl yürütme için açık kaynaklı bir araç olarak duyurulmuştu. Bu, DeepSeek’in bu alana verdiği önemi gösteriyor.

Şirket, yakın zamanda genel amaçlı büyük dil modeli V3’ün de yenilenmiş bir versiyonunu paylaşarak genel yapay zekâ yeteneklerini geliştirdiğini göstermişti. DeepSeek’in yol haritasında, özellikle “akıl yürütme” yeteneklerine odaklanan R1 isimli başka bir modelini de yakında güncellemesi bekleniyor. Prover V2’nin yayımlanması ve diğer modellerdeki bu güncellemeler, DeepSeek’in hem genel hem de spesifik alanlarda yapay zekânın sınırlarını zorlama çabasını ortaya koyuyor.

DeepSeek’in matematiksel ispat ve teorem çözümüne odaklanan Prover V2 modelini yayımlaması, yapay zekânın giderek daha spesifik, soyut ve zorlu bilimsel alanlarda yetenek kazandığını gösteren önemli bir gelişmedir. 671 milyar parametreli V3 modelini temel alan ancak alt modellere bölünen özelleşmiş mimarisiyle dikkat çeken Prover V2, matematiksel akıl yürütme gerektiren problemlerin çözümünde araştırmacılar ve geliştiriciler için güçlü bir araç olma potansiyeli taşıyor. Hugging Face üzerinden erişime açılan bu modelin, yapay zekâ destekli bilimsel keşiflere ve matematik alanındaki araştırmalara önemli katkılar sağlaması bekleniyor.

1. Temel Özellikler ve Geliştirme Süreci

• Soğuk Başlangıç (Cold-Start) Veri Üretimi:
  • Model, DeepSeek-V3‘ün matematiksel problemleri alt hedeflere ayırmasıyla oluşturulan bir veri kümesiyle eğitilmiştir.
  • Her alt hedef, 7B parametreli bir model tarafından çözülmüş ve bu çözümler birleştirilerek tam bir ispat zinciri oluşturulmuştur 1.
• Pekiştirmeli Öğrenme ile İyileştirme:
  • Model, başlangıç verileriyle ince ayar yapıldıktan sonra, doğru/yanlış geri bildirimleri ile RL aşamasına geçmiştir.
  • Bu süreç, modelin informel matematiksel akıl yürütme ile formel ispatları birleştirme becerisini güçlendirmiştir 1.

2. Performans ve Başarılar

• MiniF2F-test üzerinde %88.9 başarı oranı elde etmiştir.
• PutnamBench‘ten 658 problemden 49’unu çözmüştür.
• ProverBench adında yeni bir veri kümesi sunmuştur:
  • 325 problem içerir (AIME yarışmalarından 15, sayı teorisi, lineer cebir, analiz vb.) 1.

3. Model ve Veri Seti İndirme Seçenekleri

DeepSeek-Prover-V2 iki boyutta mevcuttur:

• 7B parametreli (32K token bağlam uzunluğu)
• 671B parametreli (DeepSeek-V3 tabanlı)

Kullanıcılar, Hugging Face üzerinden modeli yükleyip Lean 4 teoremlerini ispatlamak için kullanabilirler. Örnek bir kod snippet’i:

from transformers import AutoModelForCausalLM, AutoTokenizer
model = AutoModelForCausalLM.from_pretrained("DeepSeek-Prover-V2-7B")
tokenizer = AutoTokenizer.from_pretrained(model_id)

4. Farklılaştırıcı Özellikler

• Alt hedef analizi ile karmaşık teoremlerin parçalara ayrılması.
• Hem insan dostu akıl yürütme hem de makine dostu formel ispat üretebilme yeteneği.
• Geniş matematiksel alanlarda (cebir, analiz, olasılık) yüksek performans.

DeepSeek-Prover-V2, yapay zeka destekli matematiksel ispatlama alanında önemli bir adımdır. Özellikle eğitim ve araştırma alanlarında kullanılabilecek güçlü bir araç sunmaktadır.