DeepSeek, Lean 4 çerçevesinde biçimsel teorem kanıtlama alanında devrim yaratan açık kaynaklı bir büyük dil modeli (LLM) olan DeepSeek-Prover-V2’yi tanıttı. Bu model, DeepSeek’in son teknoloji ürünü DeepSeek-V3 temel modelinin gücünü kullanan yinelemeli bir teorem kanıtlama hattından yararlanıyor. Lean 4, Microsoft Research tarafından geliştirilen etkileşimli bir kanıt yardımcısı olan Lean teorem kanıtlayıcının en son sürümüdür. Bu gelişmiş fonksiyonel programlama dili ve etkileşimli teorem kanıtlama sistemi, matematikçilere ve bilgisayar bilimcilerine benzersiz makine tarafından kontrol edilen doğrulama ile biçimsel kanıtlar oluşturma olanağı tanır.
Proje, biçimsel ve gayri resmi matematiksel akıl yürütme arasındaki boşluğu kapatmaya yönelik anıtsal bir adımı temsil ediyor. Genel amaçlı LLM’lerin doğal yeteneklerinden yararlanarak, biçimsel teorem kanıtlamanın son derece yapılandırılmış alanını etkili bir şekilde ele almayı amaçlamaktadır. DeepSeek araştırma ekibi, yenilikçi yaklaşımlarının, karmaşık teoremleri daha yönetilebilir ve anlaşılır bileşenlere ayırırken, insan matematikçilerin kanıtlar oluştururken kullandıkları bilişsel süreçleri yansıttığını iddia ediyor.
Değerlendirme Çerçevesini Genişletme: ProverBench’in Tanıtımı
DeepSeek ekibi, araştırmalarının titizliğini artırmak amacıyla, biçimsel teorem kanıtlama yeteneklerinin kapsamlı bir şekilde değerlendirilmesi için özel olarak tasarlanmış yepyeni bir kıstas koleksiyonu olan ProverBench’i tanıtarak değerlendirme çerçevelerini önemli ölçüde genişletti. Bu kapsamlı koleksiyon, LLM’lerin biçimsel matematik bağlamındaki performansını değerlendirmek için değerli bir kaynak görevi görüyor.
Araştırmacılar, "Geleneksel kıstasların ötesinde, değerlendirme sürecimizi zenginleştirmek için titizlikle hazırlanmış 325 resmileştirilmiş problemden oluşan bir koleksiyon olan ProverBench’i gururla sunuyoruz. Bu koleksiyon, özellikle 24-25 yıllarından olmak üzere, son Amerikan Davetli Matematik Sınavı (AIME) yarışmalarından doğrudan alınan özenle seçilmiş 15 problemi içeriyor" şeklinde açıklama yaptı.
AIME problemlerinin ProverBench veri kümesine dahil edilmesi özellikle dikkat çekicidir, çünkü matematik camiasında yaygın olarak tanınan bir dizi zorlu ve köklü matematiksel problemi sunmaktadır. Bu, DeepSeek-Prover-V2’nin performansını değerlendirmek ve diğer yaklaşımlarla karşılaştırmak için standartlaştırılmış ve titiz bir temel sağlar.
Umut Veren İlk Sonuçlar: AIME Problemlerini Ele Alma
Bu zorlu AIME problemleri üzerinde yapılan titiz testlerden elde edilen ilk sonuçlar, özenle tasarlanmış özel teorem kanıtlama modellerinden olağanüstü umut verici bir performans ortaya koydu. DeepSeek ekibi, DeepSeek-Prover-V2’nin kendisine sunulan 15 AIME probleminden etkileyici bir şekilde 6’sını başarıyla çözerek hünerini sergilediğini gururla bildiriyor. Karşılaştırma yapıldığında, genel amaçlı DeepSeek-V3 modeli, çoğunluk oylama tekniklerini kullanırken 8 problemi başarıyla çözmeyi başardı.
Bu bulgular, hem özel hem de genel amaçlı LLM’lerin karmaşık matematiksel problemlerle başa çıkma potansiyelini vurgulamaktadır. Genel amaçlı model bu özel kıstasta biraz daha yüksek bir başarı oranı sergilerken, özel teorem kanıtlama modeli biçimsel matematiksel akıl yürütmedeki yeterliliğini gösterdi.
İnsan Kanıt Yapımını Taklit Etme: Bir Düşünce Zinciri Yaklaşımı
DeepSeek ekibi, "Genel amaçlı modellerin eksiksiz Lean kanıtları üretmeye çalışırken genellikle karşılaştığı iyi belgelenmiş zorluklar göz önüne alındığında, DeepSeek-V3’e kasıtlı olarak karmaşık ayrıntıları atlayarak yalnızca üst düzey bir kanıt taslağı oluşturması talimatını verdik. Ortaya çıkan düşünce zinciri, her biri çözülmesi gereken bir alt hedefi etkili bir şekilde gösteren bir üzgün yer tutucu ile titizlikle sonuçlandırılan bir dizi sahip durumundan oluşan bir Lean teoremiyle sonuçlanır. Bu yenilikçi yaklaşım, karmaşık bir teoremin aşamalı olarak daha yönetilebilir bir dizi lemaya indirgendiği insan tarzı kanıt yapımını zarif bir şekilde yansıtır" şeklinde açıklama yaptı.
Üst düzey kanıt taslakları oluşturmaya yönelik bu yenilikçi yaklaşım, matematikçilerin genellikle karmaşık kanıtlara nasıl yaklaştığıyla örtüşüyor. Model, genel yapıya ve temel adımlara odaklanarak, kanıtın sonraki iyileştirilmesine ve tamamlanmasına etkili bir şekilde rehberlik edebilir.
Yöntemsel Bir Strateji: Her Kanıt Bileşenini Ayrı Ayrı Ele Alma
Sistem daha sonra, kanıtın her bir bileşenini ele almak için yöntemli ve yapılandırılmış bir strateji kullanır. Bu sistematik yaklaşım, kanıtın her yönünün dikkatlice değerlendirilmesini ve mantıksal ve tutarlı bir şekilde ele alınmasını sağlar. Sistem, her bir sonraki adım için sağlam bir temel sağlamak amacıyla, önceden oluşturulmuş sonuçlara dayalı olarak teorem kanıtlamaya son derece yapılandırılmış bir yaklaşım oluşturur.
Araştırmacılar, "DeepSeek-V3 tarafından oluşturulan alt hedeflerden yararlanarak, her bir ara kanıt adımını sistematik olarak çözmek için yinelemeli bir çözme stratejisi benimsiyoruz. Ortaya çıkan sorunlarda orijinal hedeflerin yerine koymak için sahip durumlarından alt hedef ifadelerini çıkarıyoruz ve ardından önceki alt hedefleri önermeler olarak dahil ediyoruz. Bu yapı, sonraki alt hedeflerin önceki adımların ara sonuçları kullanılarak çözülmesini sağlayarak daha yerel bir bağımlılık yapısını teşvik eder ve daha basit lemmaların geliştirilmesini kolaylaştırır," diye detaylandırdı.
Yinelemeli çözme stratejisi, sistemin karmaşık kanıtlarla başa çıkma yeteneğinin temel bir yönüdür. Sistem, sorunu daha küçük, daha yönetilebilir alt hedeflere bölerek, her bir bileşene akıl yürütme yeteneklerini etkili bir şekilde uygulayabilir.
Hesaplama Kaynaklarını Optimize Etme: Özel Bir 7B Parametre Modeli
Sistemin ayrıştırılmış lemmaları işlemesi için etkili bir şekilde hesaplama kaynaklarını optimize etmek ve verimli işlemeyi sağlamak için stratejik olarak daha küçük, son derece özel bir 7B parametre modeli kullanır. Bu yaklaşım, sistemi arama uzayının karmaşıklığı tarafından bunaltılmadan verimli bir şekilde çalışmasını sağlayarak, kapsamlı kanıt aramalarıyla ilişkili hesaplama taleplerini etkili bir şekilde yönetmek için çok önemlidir. Yaklaşım, ayrıştırılmış tüm adımlar başarıyla çözüldüğünde otomatik olarak türetilmiş eksiksiz bir kanıtla sonuçlanır.
Araştırmacılar, "Algoritmik çerçeve, iki tamamlayıcı modelden yararlanarak iki ayrı aşamada çalışır: lemma ayrıştırması için DeepSeek-V3 ve karşılık gelen biçimsel kanıt ayrıntılarını tamamlamak için bir 7B kanıtlayıcı modeli" şeklinde tanımladı.
Bu iki aşamalı yaklaşım, sistemin hem büyük genel amaçlı bir modelin hem de daha küçük özel bir modelin güçlü yönlerinden yararlanmasını sağlar. Büyük model, üst düzey kanıt taslakları oluşturmak için kullanılırken, daha küçük model ayrıntıları doldurmak ve biçimsel kanıtı tamamlamak için kullanılır.
Biçimsel Akıl Yürütme Verilerini Sentezleme: Doğal Bir Yol
Bu titizlikle tasarlanmış mimari, yüksek düzeyde matematiksel akıl yürütmeyi biçimsel doğrulamanın sıkı ve katı gereksinimleriyle sorunsuz bir şekilde birleştirerek biçimsel akıl yürütme verilerini sentezlemek için doğal ve sezgisel bir yol oluşturur. Bu entegrasyon, sistemin sonuçlarının güvenilirliğini ve güvenilirliğini sağlamak için gereklidir.
Araştırmacılar, "Uçtan uca şekilde 7B kanıtlayıcı modeli tarafından çözülemeyen ancak ayrıştırılmış tüm alt hedeflerin başarıyla çözüldüğü zorlu problemlerin bir alt kümesini derliyoruz. Tüm alt hedeflerin kanıtlarını birleştirerek, orijinal problem için eksiksiz bir biçimsel kanıt oluşturuyoruz," diye açıkladı.
Bu yaklaşım, sistemin hatalarından ders almasını ve karmaşık problemleri çözme yeteneğini geliştirmesini sağlar. Sistem, zorluklara neden olan belirli alt hedefleri belirleyerek, çabalarını bu alanlardaki performansını iyileştirmeye odaklayabilir.
Endişeler ve Zorluklar: Uygulama Ayrıntıları İnceleme Altında
DeepSeek-Prover-V2 tarafından gösterilen inkar edilemez teknik başarılara rağmen, alandaki bazı uzmanlar belirli uygulama ayrıntılarıyla ilgili ilgili endişeleri dile getirdiler. Epoch AI’da saygın bir Baş Matematikçi olan Elliot Glazer, daha fazla araştırma gerektiren potansiyel sorunlara işaret etti.
DeepSeek-Prover-V2 bildirisiyle ilgili bazı endişeler. Potansiyel olarak yanlış resmileştirilmiş örnekler ve Lean zulip üzerindeki tartışma, PutnamBench kanıtlarının saçma olduğunu ve okuma-değerlendirme-yazdırma döngüsünde bildirilmeyen örtük bir üzgün (muhtemelen uygula? taktiğine gizlenmiş) kullandığını gösteriyor.
Bu endişeler, biçimsel doğrulama alanında var olan devam eden zorlukları canlı bir şekilde vurgulamaktadır; burada en küçük ve görünüşte önemsiz uygulama ayrıntıları bile sonuçların genel geçerliliği ve güvenilirliği üzerinde orantısız derecede büyük bir etki yaratabilir. Biçimsel doğrulama süreci, ayrıntılara sarsılmaz dikkat ve yerleşik standartlara titiz bağlılık gerektirir.
Yanlış resmileştirilmiş örnekler olasılığı ve PutnamBench kanıtlarında gizli "üzgün" taktiklerin olasılığı, doğrulama sürecinin titizliği ve eksiksizliği hakkında önemli soruları gündeme getiriyor. Bu endişeler, sonuçların sürekli inceleme ve bağımsız doğrulanması ihtiyacını vurgulamaktadır.
Erişilebilirlik ve Kaynaklar: Biçimsel Teorem Kanıtlamaya Erişimi Demokratikleştirme
DeepSeek, çeşitli hesaplama kaynaklarına ve araştırma hedeflerine hitap eden Prover-V2’yi iki farklı model boyutunda kullanıma sundu. İlk sürüm, önceki Prover-V1.5-Base’leri üzerine inşa edilmiş ve 32K tokene kadar genişletilmiş bir içerik uzunluğuna sahip 7B parametre modelidir. İkinci sürüm, DeepSeek-V3-Base üzerinde eğitilmiş önemli ölçüde daha büyük bir 671B parametre modelidir. Her iki modele de artık makine öğrenimi modellerini paylaşmak ve işbirliği yapmak için önde gelen bir platform olan HuggingFace’te kolayca erişilebilir.
DeepSeek, modellere ek olarak, değerlendirme amaçlı 325 titizlikle resmileştirilmiş problemi içeren tam ProverBench veri kümesini de HuggingFace’te kullanıma sundu. Bu kapsamlı veri kümesi, araştırmacılara ve geliştiricilere modellerinin performansını değerlendirmek ve DeepSeek-Prover-V2 ile karşılaştırmak için değerli bir kaynak sağlar.
DeepSeek, bu kaynakları ücretsiz olarak sunarak biçimsel teorem kanıtlama teknolojisine erişimi demokratikleştiriyor ve araştırma topluluğu içinde işbirliğini teşvik ediyor. Bu açık kaynak yaklaşımının alandaki ilerlemeyi hızlandırması ve otomatik akıl yürütme ve doğrulama konusunda yeni atılımlara yol açması muhtemeldir.
Bu sürüm, araştırmacıları ve geliştiricileri bu teknolojinin yeteneklerini ve sınırlamalarını derinlemesine incelemek için gereken kaynaklarla güçlendiriyor. DeepSeek, modellere ve ProverBench veri kümesine açık erişim sağlayarak, alandaki uzmanlar tarafından dile getirilen endişeleri ele almak için daha fazla araştırma ve işbirlikçi çabaları teşvik ediyor. Bu işbirlikçi yaklaşım, biçimsel teorem kanıtlamanın karmaşıklıklarını çözmenin ve bu çığır açan gelişmelerin güvenilirliğini sağlamanın anahtarını elinde tutuyor.