DeepSeek-Prover-V2 formal ispat AI ile açık kaynak matematiksel ispat otomasyonunda çığır açılıyor. DeepSeek-AI ekibi, formel mantıkta hata payı olmayan, adım adım doğrulanabilen ispatlar üretmek için subgoal decomposition ve takviyeli öğrenme (reinforcement learning) kombinasyonunu kullandı.

DeepSeek-Prover-V2 formal ispat AI nasıl çalışıyor?

Model, karmaşık teoremleri önce DeepSeek-V3 ile doğal dilde ispat taslağına dönüştürüyor. Ardından bunları Lean 4 formatında, tamamlanmamış \”have\” ifadeleriyle küçük alt-hedeflere (subgoal) parçalayarak her kısmı 7B boyutlu prover modeliyle formal olarak çözüyor. Tüm bu adımlar birleştirilip Lean ortamında gerçek zamanlı doğrulanabilir bir kanıta dönüştürülüyor. Eğitim süreci tamamen sentetik verilerle, insan etiketine gerek kalmadan ilerliyor.

• Müfredat tabanlı curriculum learning ile her aşamada daha zor görevler ekleniyor.
• İki tip subgoal (bağımlı ve bağımsız) ile model, hem parça hem bütün bazında ispat üretmeyi öğreniyor.

Benchmark	Sonuç
MiniF2F-test	%88.9 başarı (Pass@8192)
PutnamBench	49/658 problem çözüldü
AIME 2024-2025	6/15 formel ispat

Yeni ProverBench datasetiyle modelin çoklu formel ispat görevlerinde genelleme kapasitesi gösterildi. Takviyeli öğrenmede tutarlılık tabanlı ödül, modelin eskiz ve formal çözümü arasında tam uyumu destekledi.

‘DeepSeek-Prover-V2 ile hem insanlar hem klasik modeller aşılıyor; formel kanıt üreten AI için yeni çıta.’

İleri matematik, mühendislik, otomatik program doğrulama ve formal mantık gerektiren diğer disiplinlerde; insan benzeri açıklama ile gerçek zamanlı formel doğrulamanın aynı anda sunulduğu yeni bir seviye sunuyor.