“Verimlilik” için yaptığı baskıda DOGE, mantıklı olup olmadığına bakmaksızın giderek daha fazla yapay zekaya yaslanıyor. Ve onu yıkıcı amaçlara ulaşmak için kusurlu bir araç olarak kullanıyor.
DeepSeek AI, Lean 4 ortamında resmi teorem kanıtlama için özel olarak tasarlanmış çığır açan açık kaynaklı büyük dil modeli DeepSeek-Prover-V2’nin piyasaya sürüldüğünü duyurdu. Bu son yineleme, DeepSeek-V3’ün gücünden yararlanarak kendi yüksek kaliteli başlatma verilerini üreten yenilikçi bir yinelemeli teorem kanıtlama hattı sunarak önceki çalışmalara dayanıyor. Ortaya çıkan model, sinirsel teorem kanıtlamada en son teknoloji performansına ulaşıyor ve matematiksel akıl yürütme yeteneklerini değerlendirmek için yeni bir ölçüt olan ProverBench’in tanıtımıyla birlikte geliyor.
Öncü Soğuk Başlatma Mantığı Veri Üretimi
DeepSeek-Prover-V2’nin temel bir yeniliği, benzersiz soğuk başlatma eğitim prosedüründe yatmaktadır. Bu süreç, güçlü DeepSeek-V3 modelinin karmaşık matematiksel teoremleri bir dizi daha yönetilebilir alt hedefe ayırmasını sağlayarak başlar. Aynı zamanda, DeepSeek-V3 bu üst düzey kanıt adımlarını Lean 4’te resmileştirerek, etkili bir şekilde yapılandırılmış bir alt problem dizisi oluşturur.
Her alt hedef için hesaplama açısından yoğun kanıt aramasını ele almak için araştırmacılar daha küçük bir 7B parametre modeli kullandılar. Zorlu bir problemin tüm ayrıştırılmış adımları başarıyla kanıtlandığında, tam adım adım resmi kanıt DeepSeek-V3’ün karşılık gelen düşünce zinciri akıl yürütmesiyle eşleştirilir. Bu yaratıcı yaklaşım, modelin hem gayriresmî, yüksek seviyeli matematiksel akıl yürütmeyi hem de titiz resmi kanıtları birleştiren sentezlenmiş bir veri kümesinden öğrenmesini sağlayarak sonraki takviyeli öğrenme için güçlü bir soğuk başlangıç sağlar.
Gelişmiş Muhakeme için Takviyeli Öğrenme
Sentetik soğuk başlangıç verilerine dayanarak, DeepSeek ekibi 7B kanıtlayıcı modelinin uçtan uca çözemediği ancak tüm alt hedeflerin başarıyla ele alındığı zorlu problemlerden oluşan bir seçki hazırladı. Bu alt hedeflerin resmi kanıtlarını birleştirerek, orijinal problem için eksiksiz bir kanıt oluşturulur. Bu resmi kanıt daha sonra DeepSeek-V3’ün lemma ayrıştırmasını ana hatlarıyla belirten düşünce zinciriyle ilişkilendirilir ve resmi olmayan akıl yürütmenin ardından resmileştirmenin birleşik bir eğitim örneği oluşturulur.
Kanıtlayıcı model daha sonra bu sentetik veriler üzerinde ince ayar yapılır, ardından bir takviye öğrenme aşaması gelir. Bu aşama, ödül sinyali olarak ikili doğru veya yanlış geri bildirimini kullanır ve modelin resmi olmayan matematiksel sezgi ile resmi kanıtların kesin inşası arasındaki boşluğu kapatma yeteneğini daha da geliştirir.
Son teknoloji performans
Bu yenilikçi eğitim sürecinin doruk noktası, 671 milyar parametreye sahip bir model olan DeepSeek-Prover-V2–671B’dir. Bu model, sinirsel teorem kanıtlamada en son teknoloji performansını göstererek dikkat çekici sonuçlar elde etti. MiniF2F testinde etkileyici bir %88,9’luk geçme oranına ulaştı ve PutnamBench’ten 658 problemden 49’unu başarıyla çözdü . DeepSeek-Prover-V2 tarafından miniF2F veri kümesi için üretilen kanıtlar, daha fazla inceleme ve analize olanak tanıyarak indirilmek üzere herkese açık olarak mevcuttur.
ProverBench’i Tanıtıyoruz: Değerlendirme İçin Yeni Bir Standart
Model sürümüne ek olarak, DeepSeek AI, 325 problemden oluşan yeni bir kıyaslama veri kümesi olan ProverBench’i tanıttı . Bu kıyaslama, farklı zorluk seviyelerinde matematiksel akıl yürütme yeteneklerinin daha kapsamlı bir değerlendirmesini sunmak için tasarlanmıştır.
ProverBench, son AIME (Amerikan Davetli Matematik Sınavı) yarışmalarından (AIME 24 ve 25) resmileştirilmiş 15 problem içerir ve lise yarışma seviyesinde gerçek zorluklar sunar. Geriye kalan 310 problem, çeşitli alanları kapsayan çeşitli ve pedagojik olarak sağlam bir resmileştirilmiş matematik problemleri koleksiyonu sunan, düzenlenmiş ders kitabı örneklerinden ve eğitim öğreticilerinden alınmıştır
ProverBench, hem zorlu rekabet problemlerinde hem de temel lisans seviyesi matematikte sinirsel teorem ispatlayıcılarının daha kapsamlı bir şekilde değerlendirilmesini kolaylaştırmayı amaçlamaktadır.
Kullanılabilirlik
DeepSeek AI, farklı hesaplama kaynaklarına hitap etmek için DeepSeek-Prover-V2’yi iki model boyutunda yayınlıyor: 7B parametreli model ve daha büyük 671B parametreli model. DeepSeek-Prover-V2–671B, DeepSeek-V3-Base’in sağlam temeli üzerine inşa edilmiştir. Daha küçük DeepSeek-Prover-V2–7B, DeepSeek-Prover-V1.5-Base üzerine inşa edilmiştir ve 32K token’a kadar genişletilmiş bir bağlam uzunluğuna sahiptir, bu da daha uzun ve daha karmaşık akıl yürütme dizilerini işlemesine olanak tanır.
DeepSeek-Prover-V2’nin piyasaya sürülmesi ve ProverBench’in tanıtılması, sinirsel teorem kanıtlama alanında önemli bir adım ileri anlamına geliyor. Yinelemeli bir kanıt arama hattından yararlanarak ve zorlu yeni bir ölçüt sunarak DeepSeek AI, topluluğun resmi matematik için daha sofistike ve yetenekli AI sistemleri geliştirmesini ve değerlendirmesini sağlıyor.
