DeepSeek-Prover-V2-671B'yi Test Etme: Hızlı Bir Bakış

Yapay zekanın gelişimi, benzeri görülmemiş bir hassasiyetle karmaşık görevlerin üstesinden gelmek için tasarlanmış yeni bir uzmanlaşmış model dalgası ortaya çıkardı. Bunlar arasında DeepSeek Prover V2, özellikle formel matematik ve teorem ispatı alanında öne çıkıyor. Bu makale, DeepSeek Prover V2'nin ne olduğunu, ona nasıl ücretsiz çevrimiçi erişilebileceğini ve performansını değerlendirmek için özenle hazırlanmış istemlerle yeteneklerini test etmeyi inceliyor.

💡

Harika bir API Dokümantasyonu oluşturan harika bir API Test aracı mı istiyorsunuz?

Geliştirici Ekibinizin maksimum verimlilikle birlikte çalışması için entegre, Hepsi Bir Arada bir platform mu istiyorsunuz?

Apidog tüm taleplerinizi karşılıyor ve Postman'in yerini çok daha uygun bir fiyata alıyor!

DeepSeek-Prover-V2-671B Nedir?

DeepSeek-Prover-V2-671B, formel matematiksel teorem ispatı için optimize edilmiş, DeepSeek tarafından geliştirilen, 671 milyar parametreli, Uzman Karışımı (MoE) bir dil modelidir. X'teki gönderilere göre, DeepSeek V3 mimarisi üzerine inşa edilmiş, ancak özellikle mantık ağırlıklı görevler için uyarlanmış, yapay zeka destekli matematiksel akıl yürütmede önemli bir sıçramayı temsil ediyor.

Model, matematiksel araştırmalarda yaygın olarak kullanılan bir ispat asistanı olan Lean 4'ü kullanarak formel ispatların oluşturulmasını otomatikleştirmek için tasarlanmıştır. Büyük sentetik veri kümeleri üzerinde eğitimi, karmaşık matematiksel problemleri verimli bir şekilde ele almasını sağlayarak, onu araştırmacılar ve matematikçiler için değerli bir araç haline getiriyor.

Yapay zeka topluluğu üyeleri, temel özelliklerini vurguladı:

Optimum performans için FP8 ve BF16 hassasiyetini destekleyen, belirteç başına 256'dan 8 dinamik olarak etkinleştirilmiş uzmanı kullanan, çıkarım başına 37B aktif parametreye sahip 671B parametre ölçeği.
Gelişmiş YaRN RoPE kodlaması aracılığıyla kararlı uzun metin modellemesi ile kapsamlı matematiksel bağlamları işleyebilmesini sağlayan, DeepSeek V3'ten miras alındığı gibi, 163.840 belirtece kadar bir bağlam penceresini desteklemesi muhtemeldir.
Hem ticari kullanıma izin veren kodu için bir MIT Lisansı hem de ağırlıkları için izin verici bir Model Lisansı altında yayınlandı.

Model, X'te bir "matematik ispat canavarı" olarak tanımlanıyor ve miniF2F kıyaslamasında %63,5 ve ProofNet'te %25,3'e ulaşan seleflerinin başarısı üzerine inşa edilerek, formel teoremleri otomatikleştirme konusunda mükemmel. DeepSeek-Prover-V2-671B, genel akıl yürütmeden ziyade matematiksel mantığa odaklanarak, onu genel amaçlı bir dil modelinden ziyade özel bir araç olarak konumlandırıyor.

Hugging Face'deki yayınlanması heyecan yarattı; X'teki bazı yapay zeka topluluğu üyeleri onu "formel matematik ispatları için bir güç merkezi" olarak adlandırıyor ve formel matematik uygulamalarında diğer açık kaynaklı modellerden daha iyi performans gösterme potansiyeline dikkat çekiyor. Yakında beklenen daha genel amaçlı bir model olan DeepSeek R2'den farklıdır ve DeepSeek'in niş alanlarda sınırları zorlayan etki alanı odaklı modeller geliştirme stratejisinin altını çiziyor. Prover-V2-671B, formel matematikte yapay zeka için yeni bir standart belirliyor.

Huggingface bağlantısı: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B/tree/main

DeepSeek Prover V2'yi Çevrimiçi Olarak Ücretsiz Nasıl Kullanılır

OpenRouter gibi platformlar sayesinde DeepSeek Prover V2'ye erişmek kolaydır; bu platformlar, modeli bir OpenAI uyumlu API aracılığıyla test etmek için ücretsiz bir katman sağlar. Aşağıda, mevcut kaynaklara ve en iyi uygulamalara dayanarak, https://openrouter.ai/models/deepseek/deepseek-prover-v2:free adresinde DeepSeek Prover V2'yi ücretsiz kullanmaya yönelik adım adım bir kılavuz bulunmaktadır.

Adım 1: OpenRouter'a Kaydolun

OpenRouter.ai adresini ziyaret edin ve sağ üst köşedeki "Kaydol" düğmesini tıklayın.
Bir e-posta, Google veya GitHub hesabı kullanarak kaydolun. Daha hızlı kurulum nedeniyle geliştiriciler için bir GitHub hesabı önerilir.
Oturum açtıktan sonra, panoya gidin.

Adım 2: DeepSeek Prover V2'yi Bulun

"Trend Olan Modeller" bölümüne gidin veya "DeepSeek" yazmak için arama çubuğunu kullanın.
Listeden "DeepSeek: DeepSeek Prover V2 (ücretsiz)" seçeneğini seçin. Bu, ücretsiz katman modeline eriştiğinizden emin olmanızı sağlar.

Adım 3: Bir API Anahtarı Oluşturun

Model sayfasında, "API Anahtarı Oluştur" düğmesini bulun (model açıklamasının altında veya hesap ayarlarında).
Anahtarınıza bir ad verin (örneğin, "ProverV2-Test") ve onaylayın. Anahtarı kopyalayın ve güvenli bir şekilde saklayın, çünkü API istekleri için gereklidir.
OpenRouter'ın API'si, mevcut araçlarla entegrasyonu basitleştiren OpenAI uyumludur.

Adım 4: Ortamınızı Kurun

API ile etkileşim kurmak için bir programlama ortamına ihtiyacınız olacak. Basitliği nedeniyle Python önerilir. Henüz yapmadıysanız, openai kitaplığını yükleyin:

pip install openai

Adım 5: API İstekleri Yapın

DeepSeek Prover V2'yi test etmek için aşağıdaki Python betiğini kullanın. YOUR_API_KEY_HERE'ı OpenRouter API anahtarınızla değiştirin:

import openai

client = openai.OpenAI(
    base_url="<https://openrouter.ai/api/v1>",
    api_key="YOUR_API_KEY_HERE"
)

response = client.chat.completions.create(
    model="deepseek/deepseek-prover-v2:free",
    messages=[
        {"role": "system", "content": "Lean 4 ile formel teorem ispatı konusunda uzmanlaşmış bir matematiksel ispat asistanısınız."},
        {"role": "user", "content": "İki çift sayının toplamının çift olduğunu kanıtlayın."}
    ]
)

print(response.choices[0].message.content)

Bu betik, Prover V2'ye bir istem gönderir ve yanıtı yazdırır. Yanıt yaratıcılığı için sıcaklık veya yanıt uzunluğu için max_tokens gibi parametreleri gerektiği gibi ayarlayabilirsiniz.

Adım 6: Kullanımı İzleyin

Ücretsiz katmanın kullanım sınırları vardır, bu nedenle belirteç tüketiminizi izleyin. OpenRouter, istekleri düşük gecikme süresi için "Together" gibi sağlayıcılara yönlendirerek güvenilirliği sağlar. Daha fazla kapasiteye ihtiyacınız varsa, ücretli katmanları veya OpenRouter'daki diğer DeepSeek modellerini keşfedin.

Başarı İçin İpuçları

Ayrıntılı İstemler: Prover V2, test için optimize edilmiş bir temel modeldir ve optimum sonuçlar için hassas ve ayrıntılı istemler gerektirir.
Hata İşleme: Modelin bazen boş yanıtlar döndürebileceğinden, yeniden deneme mekanizmalarını uygulayın.
Güvenlik: Yetkisiz erişimi önlemek için API anahtarınızı asla kamuya açık olarak paylaşmayın.

DeepSeek Prover V2'yi İstemlerle Test Etme

DeepSeek Prover V2'nin yeteneklerini değerlendirmek için, formel matematiksel akıl yürütme ve teorem ispatındaki güçlü yönlerini hedefleyen üç test istemi tasarladım. Bu istemler, matematiksel araştırmalarda yaygın kullanım durumlarını yansıtan temelden gelişmişe kadar uzanmaktadır. Her istem, ideal olarak uzmanlığı göz önüne alındığında, Lean 4 ile uyumlu bir biçimde doğru, formel ispatlar üretme yeteneğini değerlendirmek için hazırlanmıştır.

Kolay Bir İstemle Başlayalım

İstem: "A ve B gibi herhangi iki küme için, kesişimlerinin A'nın bir alt kümesi olduğunu kanıtlayın; yani. A ∩ B ⊆ A. Lean 4 ispatını ve ana adımın tek cümlelik bir açıklamasını sağlayın."

Deepseek-Prover-V2 Model Yanıtları:

### Lean 4 İspatı

```lean
theorem intersection_subset_left (A B : Type) (a : A) : A ∩ B ⊆ A := by
  intro x hx
  cases hx with
  | intro hx₁ hx₂ =>
    exact hx₁
  <;> simp_all
```

### Ana Adımın Açıklaması

Bu ispattaki ana adım, hipotezi `hx : x ∈ A ∩ B` iki bileşenine, `hx₁ : x ∈ A` ve `hx₂ : x ∈ B` ayrıştırmak için `cases` taktiğinin kullanılmasıdır ve `x ∈ A` sonucuna varmak için doğrudan `hx₁`'yi kullanmamızı sağlar.

### Tek Cümlelik Açıklama

`A ∩ B` kesişimi, tanım gereği, `A ∩ B`'deki herhangi bir eleman aynı zamanda `A`'da olduğundan, `A`'nın bir alt kümesidir.

Merakımdan, OpenAI o3 modelinden yanıta yorum yapmasını istedim ve bu çok ilginç:

Fikriniz doğru—“`x ∈ A ∩ B`'den ilk bağlacı çıkarın”—ancak ifade ve ispatın birkaç düzeltmeye ihtiyacı var.

1  Tip ve değişken başlığı  
• `A` ve `B` türler değil, kümeler olmalıdır, bu nedenle şunu yazın  
  `{α : Type*} (A B : Set α)`  
• Ek argüman `a : A` ilgisizdir ve kaldırılmalıdır.

2  Minimal deyimsel ispat  
Çünkü `hx : x ∈ A ∩ B` kelimenin tam anlamıyla `⟨hx₁, hx₂⟩`'dir, `cases` ile parçalamak yerine `.1` (veya `.left`) ile sol bileşeni alabilirsiniz.  
```lean
open Set

theorem inter_subset_left {α} (A B : Set α) : A ∩ B ⊆ A := by
  intro x hx
  exact hx.1          -- veya `exact hx.left`
```
Lean'in standart kitaplığı zaten bu lemmayı `inter_subset_left` olarak içerir, bu nedenle bir satır yeterlidir:
```lean
exact Set.inter_subset_left
```

3  Gereksiz taktikler  
İzleyen `;<;> simp_all` burada hiçbir şey yapmıyor—`exact hx₁` zaten hedefi kapatıyor.

Kısacası, ek parametreyi bırakın, `Type` yerine `Set` kullanın ve temiz, geleneksel bir ispat için gövdeyi `exact hx.1`'e (veya sadece yerleşik lemmayı yeniden kullanın) küçültün.

OpenAI o3'ün yanıtını Deepseek-Prover-V3'e besledim ve şöyle diyor:

### Revize Edilmiş Lean 4 İspatı

```lean
theorem intersection_subset_left {α : Type*} (A B : Set α) : A ∩ B ⊆ A := by
  intro x hx
  exact hx.1
```

### Tek Cümlelik Açıklama

Ana adım, `hx : x ∈ A ∩ B`'nin `hx₁ : x ∈ A` ve `hx₂ : x ∈ B` olduğu bir çift `⟨hx₁, hx₂⟩` olmasıdır, bu nedenle `hx.1` doğrudan `x ∈ A` verir ve `A ∩ B ⊆ A`'yı kanıtlar.

### Ek Notlar

1. İspat, kümeleri temsil etmek için `Type` yerine doğru bir şekilde `Set α` kullanır.
2. `{α : Type*}` sözdizimi, teoremin herhangi bir `α` türü üzerinde genel olmasına izin verir.
3. Gereksiz parametre `a : A` ve izleyen taktikler kaldırılmıştır.
4. Tam adı `Set α` kullandığımız için `open Set` komutu atlanmıştır.
5. İspat, `hx.1`'in doğrudan `x ∈ A` olan `hx`'nin ilk bileşenini çıkardığı gerçeğinden yararlanır.

Ve o3'ün bu isteme verdiği yanıt şöyle:

Revizyonunuz nokta atışı.

• Doğruluk ve özlülük `hx.1` (diğer adıyla `hx.left`), “bağlacın ilk bileşenini al” için kanonik Lean deyimidir, bu nedenle ispat hem geçerlidir hem de olabildiğince kısadır—okuyucuların taklit etmesi gereken tam olarak budur.

• Genellik `{α : Type*}`'i kullanmak lemmanın polimorfik kalmasını sağlar ve `Set α` doğru soyutlamadır. Yersiz parametreyi ve taktikleri silme çağrısı iyi.

• Stil nüansı Kod yeniden kullanımını vurgulamak istiyorsanız, basitçe `exact Set.inter_subset_left` yazabilirsiniz—Lean zaten bu lemaya sahip—ancak tek satırlık ispatı göstermek, özellikle birleşimleri nasıl açacaklarını öğrenen yeni başlayanlar için pedagojik olarak faydalıdır.

Sonuç olarak, ispat, açıklama ve madde işaretli yorum temiz ve öğreticidir; daha fazla düzenleme yapmadan makalenizde iyi okunacaktır.

2 modelin karşılıklı etkileşimini ve birbirlerini düzeltmelerini izlemek gerçekten ilginç.

Sonuç

DeepSeek Prover V2, Lean 4'te karmaşık ispatları otomatikleştirmek için 671B parametreli bir MoE mimarisinden yararlanan, formel matematiksel teorem ispatı için çığır açan bir araçtır. OpenRouter'ın API'si aracılığıyla ücretsiz olarak erişilebilen, araştırmacılara ve meraklılara yapay zeka destekli matematiği keşfetmek için güçlü bir platform sunar. Temel, orta ve gelişmiş teoremleri kapsayan sağlanan test istemleri, çeşitli matematiksel zorlukların üstesinden gelme potansiyelini göstermektedir. Yapay zeka akademik araştırmayı yeniden şekillendirmeye devam ettikçe, Prover V2, formel matematikte yeniliği yönlendiren özel, açık kaynaklı bir çözüm olarak öne çıkıyor.

💡

button