DeepSeek-Prover-V2-671B 테스트: 간단 사용 후기

AI의 발전은 전례 없는 정확성으로 복잡한 작업을 해결하도록 설계된 새로운 전문 모델의 물결을 가져왔습니다. 그중에서도 DeepSeek Prover V2는 특히 형식 수학 및 정리 증명 분야에서 뛰어난 성능을 보여주고 있습니다. 이 글에서는 DeepSeek Prover V2가 무엇인지, 온라인에서 무료로 액세스하고 사용하는 방법, 그리고 성능 평가를 위해 신중하게 작성된 프롬프트로 그 기능을 테스트한 결과를 자세히 살펴봅니다.

DeepSeek-Prover-V2-671B는 무엇인가요?

DeepSeek-Prover-V2-671B는 DeepSeek이 개발한 6,710억 개의 매개변수를 가진 MoE(Mixture-of-Experts) 언어 모델로, 형식 수학 정리 증명에 최적화되어 있습니다. X에 올라온 게시물에 따르면, 이는 DeepSeek V3 아키텍처를 기반으로 구축되었지만 논리 중심 작업에 특화되어 AI 기반 수학적 추론에 있어 상당한 도약을 나타냅니다.

이 모델은 수학 연구에서 널리 사용되는 증명 도우미인 Lean 4를 사용하여 형식 증명 생성을 자동화하도록 설계되었습니다. 방대한 합성 데이터셋에 대한 훈련을 통해 복잡한 수학 문제를 효율적으로 처리할 수 있어 연구원과 수학자에게 귀중한 도구가 됩니다.

AI 커뮤니티 회원들은 주요 기능을 다음과 같이 강조했습니다.

• 추론 패스당 370억 개의 활성 매개변수를 가진 6,710억 개의 매개변수 규모로, 토큰당 256개 전문가 중 8개가 동적으로 활성화되며, 최적화된 성능을 위해 FP8 및 BF16 정밀도를 지원합니다.
• DeepSeek V3에서 상속받은 최대 163,840개의 토큰 컨텍스트 창을 지원할 가능성이 높으며, 고급 YaRN RoPE 인코딩을 통해 안정적인 장문 모델링으로 광범위한 수학적 컨텍스트를 처리할 수 있습니다.
• 코드에 대해서는 MIT 라이선스로, 가중치에 대해서는 상업적 사용을 허용하는 관대한 모델 라이선스로 출시되었습니다.

이 모델은 X에서 "수학 증명 괴물"로 묘사되며, 이전 모델들이 miniF2F 벤치마크에서 63.5%, ProofNet에서 25.3%를 달성한 성공을 기반으로 형식 정리 자동화에 탁월한 성능을 보여줍니다. DeepSeek-Prover-V2-671B는 일반적인 추론보다는 수학적 논리에 초점을 맞추고 있어, 범용 언어 모델이 아닌 전문 도구로 자리매김하고 있습니다.

Hugging Face에 출시되면서 AI 커뮤니티 회원들 사이에서 "형식 수학 증명을 위한 강력한 도구"라 불리며 흥분을 불러일으켰고, 형식 수학 애플리케이션에서 다른 오픈 소스 모델을 능가할 잠재력이 있다고 언급되었습니다. 곧 출시될 예정인 보다 범용적인 모델인 DeepSeek R2와는 구별되며, 틈새 분야에서 한계를 뛰어넘는 도메인별 모델을 개발하려는 DeepSeek의 전략을 강조합니다. Prover-V2-671B는 형식 수학 분야 AI의 새로운 기준을 제시합니다.

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

DeepSeek Prover V2를 온라인에서 무료로 사용하는 방법

OpenRouter와 같은 플랫폼 덕분에 DeepSeek Prover V2에 액세스하는 것은 간단합니다. OpenRouter는 OpenAI 호환 API를 통해 모델을 테스트할 수 있는 무료 등급을 제공합니다. 다음은 사용 가능한 리소스와 모범 사례를 기반으로 https://openrouter.ai/models/deepseek/deepseek-prover-v2:free에서 DeepSeek Prover V2를 무료로 사용하는 단계별 가이드입니다.

1단계: OpenRouter 가입

1. OpenRouter.ai를 방문하여 오른쪽 상단 모서리에 있는 "Sign Up" 버튼을 클릭합니다.
2. 이메일, Google 또는 GitHub 계정을 사용하여 등록합니다. 개발자에게는 더 빠른 설정을 위해 GitHub 계정을 추천합니다.
3. 로그인 후 대시보드로 이동합니다.

2단계: DeepSeek Prover V2 찾기

1. "Trending Models" 섹션으로 스크롤하거나 검색창에 "DeepSeek"을 입력합니다.
2. 목록에서 "DeepSeek: DeepSeek Prover V2 (free)"를 선택합니다. 이렇게 하면 무료 등급 모델에 액세스할 수 있습니다.

3단계: API 키 생성

1. 모델 페이지에서 "Create API Key" 버튼을 찾습니다 (모델 설명 아래 또는 계정 설정에 있습니다).
2. 키 이름을 지정하고 (예: "ProverV2-Test") 확인합니다. API 요청에 필요하므로 키를 복사하여 안전하게 보관합니다.
3. OpenRouter의 API는 OpenAI 호환이므로 기존 도구와의 통합이 간단합니다.

4단계: 환경 설정

API와 상호 작용하려면 프로그래밍 환경이 필요합니다. 단순성을 위해 Python을 추천합니다. 아직 설치하지 않았다면 openai 라이브러리를 설치합니다.

pip install openai

5단계: API 요청

다음 Python 스크립트를 사용하여 DeepSeek Prover V2를 테스트합니다. YOUR_API_KEY_HERE를 OpenRouter API 키로 바꿉니다.

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": "You are a mathematical proof assistant specializing in formal theorem proving with Lean 4."},
        {"role": "user", "content": "Prove that the sum of two even numbers is even."}
    ]
)

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

이 스크립트는 Prover V2에 프롬프트를 보내고 응답을 출력합니다. 필요에 따라 temperature (응답의 창의성) 또는 max_tokens (응답 길이)와 같은 매개변수를 조정할 수 있습니다.

6단계: 사용량 모니터링

무료 등급에는 사용량 제한이 있으므로 토큰 소비량을 모니터링하십시오. OpenRouter는 짧은 지연 시간을 위해 "Together"와 같은 제공업체로 요청을 라우팅하여 안정성을 보장합니다. 더 많은 용량이 필요한 경우 유료 등급 또는 OpenRouter의 다른 DeepSeek 모델을 살펴보십시오.

성공을 위한 팁

• 상세한 프롬프트: Prover V2는 테스트에 최적화된 기본 모델이므로 최적의 결과를 얻으려면 정확하고 상세한 프롬프트가 필요합니다.
• 오류 처리: 모델이 때때로 빈 응답을 반환할 수 있으므로 재시도 메커니즘을 구현합니다.
• 보안: 무단 액세스를 방지하기 위해 API 키를 공개적으로 공유하지 마십시오.

프롬프트로 DeepSeek Prover V2 테스트

DeepSeek Prover V2의 기능을 평가하기 위해 형식 수학적 추론 및 정리 증명에서의 강점을 목표로 하는 세 가지 테스트 프롬프트를 설계했습니다. 이 프롬프트는 기본부터 고급까지 다양하며, 수학 연구의 일반적인 사용 사례를 반영합니다. 각 프롬프트는 모델의 전문성을 고려하여 정확하고 형식적인 증명을 생성하는 능력, 이상적으로는 Lean 4와 호환되는 형식으로 생성하는 능력을 평가하도록 세심하게 작성되었습니다.

쉬운 프롬프트부터 시작해 보겠습니다.

프롬프트: "두 집합 A와 B에 대해 그들의 교집합이 A의 부분집합임을 증명하시오. 즉, A ∩ B ⊆ A 임을 증명하시오. 완전한 Lean 4 증명과 핵심 단계에 대한 한 문장 설명을 제공하시오."

Deepseek-Prover-V2 모델 응답:

### Lean 4 Proof

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

### Explanation of the Key Step

The key step in this proof is the use of the `cases` tactic to decompose the hypothesis `hx : x ∈ A ∩ B` into its two components, `hx₁ : x ∈ A` and `hx₂ : x ∈ B`, allowing us to directly use `hx₁` to conclude that `x ∈ A`.

### One-Sentence Explanation

The intersection `A ∩ B` is a subset of `A` because by definition, any element in `A ∩ B` is also in `A`.

궁금해서 OpenAI o3 모델에게 이 응답에 대한 의견을 물어보니 매우 흥미로웠습니다.

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.

저는 OpenAI o3의 응답을 Deepseek-Prover-V3에 입력했고, Deepseek-Prover-V3는 다음과 같이 말했습니다.

### Revised Lean 4 Proof

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

### One-Sentence Explanation

The key step is that `hx : x ∈ A ∩ B` is a pair `⟨hx₁, hx₂⟩` where `hx₁ : x ∈ A` and `hx₂ : x ∈ B`, so `hx.1` directly gives `x ∈ A`, proving `A ∩ B ⊆ A`.

### Additional Notes

1. The proof correctly uses `Set α` instead of `Type` to represent sets.
2. The `{α : Type*}` syntax allows the theorem to be generic over any type `α`.
3. The unnecessary parameter `a : A` and trailing tactics have been removed.
4. The `open Set` command is omitted because we use the full name `Set α`.
5. The proof leverages the fact that `hx.1` directly extracts the first component of `hx`, which is `x ∈ A`.

그리고 이 프롬프트에 대한 o3의 응답은 다음과 같습니다.

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.

두 모델이 서로 의견을 주고받으며 수정하는 것을 보는 것은 정말 흥미로웠습니다.

결론

DeepSeek Prover V2는 형식 수학 정리 증명을 위한 획기적인 도구로, 6,710억 개의 매개변수를 가진 MoE 아키텍처를 활용하여 Lean 4에서 복잡한 증명을 자동화합니다. OpenRouter의 API를 통해 무료로 액세스할 수 있어 연구원과 애호가들에게 AI 기반 수학을 탐구할 강력한 플랫폼을 제공합니다. 제공된 테스트 프롬프트(기본, 중급, 고급 정리 포함)는 다양한 수학적 문제를 처리할 수 있는 잠재력을 보여줍니다. AI가 학술 연구를 계속 재편함에 따라 Prover V2는 형식 수학 분야에서 혁신을 이끄는 전문화된 오픈 소스 솔루션으로 두각을 나타냅니다.