Menguji DeepSeek-Prover-V2-671B: Tinjauan Singkat

Pengembangan AI telah melahirkan gelombang baru model-model khusus yang dirancang untuk menangani tugas-tugas kompleks dengan presisi yang belum pernah terjadi sebelumnya. Di antara model-model ini, DeepSeek Prover V2 telah muncul sebagai model yang menonjol, terutama dalam bidang matematika formal dan pembuktian teorema. Artikel ini menggali lebih dalam tentang apa itu DeepSeek Prover V2, cara mengakses dan menggunakannya secara gratis daring, serta menguji kemampuannya dengan prompt yang dibuat dengan cermat untuk mengevaluasi kinerjanya.

Apa Itu DeepSeek-Prover-V2-671B?

DeepSeek-Prover-V2-671B adalah model bahasa Mixture-of-Experts (MoE) berparameter 671 miliar yang dikembangkan oleh DeepSeek, dioptimalkan untuk pembuktian teorema matematika formal. Menurut postingan di X, model ini mewakili lompatan signifikan dalam penalaran matematika berbasis AI, dibangun di atas arsitektur DeepSeek V3 tetapi disesuaikan secara khusus untuk tugas-tugas yang berat logika.

Model ini dirancang untuk mengotomatiskan pembuatan bukti formal menggunakan Lean 4, asisten pembuktian yang banyak digunakan dalam penelitian matematika. Pelatihannya pada kumpulan data sintetis yang masif memungkinkannya menangani masalah matematika yang kompleks secara efisien, menjadikannya alat yang berharga bagi para peneliti dan matematikawan.

Anggota komunitas AI telah menyoroti fitur utamanya:

• Skala parameter 671B dengan 37B parameter aktif per lintasan inferensi, memanfaatkan 8 ahli yang diaktifkan secara dinamis dari 256 per token, dengan dukungan untuk presisi FP8 dan BF16 untuk kinerja yang dioptimalkan.
• Kemungkinan mendukung jendela konteks hingga 163.840 token, sebagaimana diwarisi dari DeepSeek V3, memungkinkannya memproses konteks matematika yang luas dengan pemodelan teks panjang yang stabil melalui pengkodean YaRN RoPE tingkat lanjut.
• Dirilis di bawah Lisensi MIT untuk kodenya dan Lisensi Model yang permisif untuk bobotnya, keduanya mengizinkan penggunaan komersial.

Model ini digambarkan sebagai "monster pembuktian matematika" di X, unggul dalam mengotomatiskan teorema formal dan membangun kesuksesan pendahulunya, yang mencapai 63,5% pada benchmark miniF2F dan 25,3% pada ProofNet. DeepSeek-Prover-V2-671B berfokus pada logika matematika daripada penalaran umum, memposisikannya sebagai alat khusus daripada model bahasa tujuan umum.

Perilisannya di Hugging Face telah memicu kegembiraan, dengan beberapa anggota komunitas AI di X menyebutnya sebagai "kekuatan besar untuk bukti matematika formal" dan mencatat potensinya untuk mengungguli model sumber terbuka lainnya dalam aplikasi matematika formal. Model ini berbeda dari DeepSeek R2, model tujuan umum yang lebih luas yang diharapkan segera dirilis, menggarisbawahi strategi DeepSeek untuk mengembangkan model khusus domain yang mendorong batas-batas di area khusus. Prover-V2-671B menetapkan standar baru untuk AI dalam matematika formal.

Tautan Huggingface: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B/tree/main

Cara Menggunakan DeepSeek Prover V2 Secara Gratis Daring

Mengakses DeepSeek Prover V2 sangat mudah, berkat platform seperti OpenRouter, yang menyediakan tingkatan gratis untuk menguji model melalui API yang kompatibel dengan OpenAI. Berikut adalah panduan langkah demi langkah untuk menggunakan DeepSeek Prover V2 secara gratis di https://openrouter.ai/models/deepseek/deepseek-prover-v2:free, berdasarkan sumber daya yang tersedia dan praktik terbaik.

Langkah 1: Daftar di OpenRouter

1. Kunjungi OpenRouter.ai dan klik tombol "Sign Up" di sudut kanan atas.
2. Daftar menggunakan email, akun Google, atau GitHub. Akun GitHub direkomendasikan untuk pengembang karena pengaturan yang lebih cepat.
3. Setelah masuk, navigasikan ke dasbor.

Langkah 2: Temukan DeepSeek Prover V2

1. Gulir ke bagian "Trending Models" atau gunakan bilah pencarian untuk mengetik "DeepSeek."
2. Pilih "DeepSeek: DeepSeek Prover V2 (free)" dari daftar. Ini memastikan Anda mengakses model tingkatan gratis.

Langkah 3: Hasilkan Kunci API

1. Di halaman model, temukan tombol "Create API Key" (di bawah deskripsi model atau di pengaturan akun).
2. Beri nama kunci Anda (misalnya, "ProverV2-Test") dan konfirmasi. Salin kunci dan simpan dengan aman, karena diperlukan untuk permintaan API.
3. API OpenRouter kompatibel dengan OpenAI, menyederhanakan integrasi dengan alat yang ada.

Langkah 4: Siapkan Lingkungan Anda

Untuk berinteraksi dengan API, Anda memerlukan lingkungan pemrograman. Python direkomendasikan karena kesederhanaannya. Instal pustaka openai jika Anda belum melakukannya:

pip install openai

Langkah 5: Lakukan Permintaan API

Gunakan skrip Python berikut untuk menguji DeepSeek Prover V2. Ganti YOUR_API_KEY_HERE dengan kunci API OpenRouter Anda:

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": "Anda adalah asisten pembuktian matematika yang berspesialisasi dalam pembuktian teorema formal dengan Lean 4."},
        {"role": "user", "content": "Buktikan bahwa jumlah dua bilangan genap adalah genap."}
    ]
)

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

Skrip ini mengirimkan prompt ke Prover V2 dan mencetak responsnya. Anda dapat menyesuaikan parameter seperti temperature (untuk kreativitas respons) atau max_tokens (untuk panjang respons) sesuai kebutuhan.

Langkah 6: Pantau Penggunaan

Tingkatan gratis memiliki batas penggunaan, jadi pantau konsumsi token Anda. OpenRouter memastikan keandalan dengan merutekan permintaan ke penyedia seperti "Together" untuk latensi rendah. Jika Anda membutuhkan kapasitas lebih, jelajahi tingkatan berbayar atau model DeepSeek lainnya di OpenRouter.

Tips untuk Sukses

• Prompt Rinci: Prover V2 adalah model dasar yang dioptimalkan untuk pengujian, membutuhkan prompt yang tepat dan rinci untuk hasil optimal.
• Penanganan Kesalahan: Terapkan mekanisme coba lagi, karena model kadang-kadang dapat mengembalikan respons kosong.
• Keamanan: Jangan pernah membagikan kunci API Anda secara publik untuk mencegah akses tidak sah.

Menguji DeepSeek Prover V2 dengan Prompt

Untuk mengevaluasi kemampuan DeepSeek Prover V2, saya telah merancang tiga prompt pengujian yang menargetkan kekuatannya dalam penalaran matematika formal dan pembuktian teorema. Prompt ini berkisar dari dasar hingga lanjutan, mencerminkan kasus penggunaan umum dalam penelitian matematika. Setiap prompt dibuat untuk menilai kemampuan model dalam menghasilkan bukti yang akurat, formal, idealnya dalam format yang kompatibel dengan Lean 4, mengingat spesialisasi model ini.

Mari Kita Mulai dengan Prompt Mudah

Prompt: "buktikan bahwa untuk setiap dua himpunan A dan B, irisan keduanya adalah himpunan bagian dari A; yaitu. A ∩ B ⊆ A. Berikan bukti Lean 4 yang lengkap dan penjelasan satu kalimat tentang langkah kuncinya."

Respons Model Deepseek-Prover-V2:

### Bukti Lean 4

```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
```

### Penjelasan Langkah Kunci

Langkah kunci dalam bukti ini adalah penggunaan taktik `cases` untuk menguraikan hipotesis `hx : x ∈ A ∩ B` menjadi dua komponennya, `hx₁ : x ∈ A` dan `hx₂ : x ∈ B`, memungkinkan kita untuk langsung menggunakan `hx₁` untuk menyimpulkan bahwa `x ∈ A`.

### Penjelasan Satu Kalimat

Irisan `A ∩ B` adalah himpunan bagian dari `A` karena berdasarkan definisi, setiap elemen dalam `A ∩ B` juga berada dalam `A`.

Karena penasaran, saya meminta model OpenAI o3 untuk memberikan komentar tentang respons tersebut, dan itu sangat menarik:

Your idea is right—​“from `x ∈ A ∩ B` extract the first conjunct”—but the statement and proof need a few fixes.

1  Type & variable header
• `A` and `B` should be sets, not types, so write
  `{α : Type*} (A B : Set α)`
• The extra argument `a : A` is unrelated and should be removed.

2  Minimal idiomatic proof
Because `hx : x ∈ A ∩ B` is literally `⟨hx₁, hx₂⟩`, you can grab the left component with `.1` (or `.left`) instead of destructuring with `cases`.
```lean
open Set

theorem inter_subset_left {α} (A B : Set α) : A ∩ B ⊆ A := by
  intro x hx
  exact hx.1          -- or `exact hx.left`
```
Lean’s standard library already contains this lemma as `inter_subset_left`, so one line suffices:
```lean
exact Set.inter_subset_left
```

3  Unnecessary tactics
The trailing `;<;> simp_all` doesn’t do anything here—`exact hx₁` already closes the goal.

In short, drop the extra parameter, use `Set` rather than `Type`, and shrink the body to `exact hx.1` (or just reuse the builtin lemma) for a clean, conventional proof.

Saya memasukkan respons OpenAI o3 ke Deepseek-Prover-V3, dan responsnya adalah:

### Bukti Lean 4 yang Direvisi

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

### Penjelasan Satu Kalimat

Langkah kunci adalah bahwa `hx : x ∈ A ∩ B` adalah pasangan `⟨hx₁, hx₂⟩` di mana `hx₁ : x ∈ A` dan `hx₂ : x ∈ B`, jadi `hx.1` secara langsung memberikan `x ∈ A`, membuktikan `A ∩ B ⊆ A`.

### Catatan Tambahan

1. Bukti ini dengan benar menggunakan `Set α` alih-alih `Type` untuk merepresentasikan himpunan.
2. Sintaks `{α : Type*}` memungkinkan teorema ini bersifat generik di atas tipe apa pun `α`.
3. Parameter `a : A` yang tidak perlu dan taktik tambahan telah dihapus.
4. Perintah `open Set` dihilangkan karena kita menggunakan nama lengkap `Set α`.
5. Bukti ini memanfaatkan fakta bahwa `hx.1` secara langsung mengekstrak komponen pertama dari `hx`, yaitu `x ∈ A`.

Dan respons o3 terhadap prompt ini mengatakan:

Your revision is spot-on.

• Correctness and conciseness `hx.1` (alias `hx.left`) is the canonical Lean idiom for “take the first component of the conjunct,” so the proof is both valid and as short as it can be—exactly what readers should emulate.

• Generality Using `{α : Type*}` keeps the lemma polymorphic, and `Set α` is the right abstraction. Good call on deleting the stray parameter and tactics.

• Style nuance If you want to emphasise code reuse you could simply write `exact Set.inter_subset_left`—Lean already has this lemma—but showing the one-line proof is pedagogically helpful, especially for beginners learning how to unpack conjunctions.

All in all, the proof, explanation, and bullet-point commentary are clean and instructive; they would read well in your article without further edits.

Sangat menarik melihat kedua model ini saling berbalas dan mengoreksi satu sama lain.

Kesimpulan

DeepSeek Prover V2 adalah alat terobosan untuk pembuktian teorema matematika formal, memanfaatkan arsitektur MoE 671B-parameter untuk mengotomatiskan bukti kompleks di Lean 4. Dapat diakses secara gratis melalui API OpenRouter, model ini menawarkan platform yang kuat bagi peneliti dan penggemar untuk menjelajahi matematika berbasis AI. Prompt pengujian yang disediakan—meliputi teorema dasar, menengah, dan lanjutan—menunjukkan potensinya untuk menangani berbagai tantangan matematika. Seiring AI terus membentuk kembali penelitian akademis, Prover V2 menonjol sebagai solusi khusus dan sumber terbuka yang mendorong inovasi dalam matematika formal.