DeepSeek Prover V2 공개, AI가 수학을 증명하는 시대

안녕하세요.

오늘은 인공지능 분야에서 주목받고 있는 DeepSeek Prover V2에 대해 소개드립니다. 최근 AI는 자연어 처리에서 뛰어난 성과를 보였지만, 이제 그 영역을 넘어 수학 증명 같은 복잡한 문제 해결로 확장되고 있습니다. 특히 DeepSeek Prover V2는 기존의 방식과 달리 강화학습과 공식적인 논리 구조를 결합해 복잡한 수학 문제를 놀랍도록 정교하게 풀어내는 능력을 보여주고 있습니다. 예를 들어, 고등학교나 대학 수준의 수학 문제를 사람이 해결하듯 단계별로 쪼개어 분석하고 증명하는 것이죠. 오늘 포스팅에서는 이 모델이 왜 혁신적인지, 어떻게 작동하는지, 그리고 우리 일상과 연구에 어떤 영향을 줄 수 있는지 하나하나 살펴보겠습니다.

 

 

---

DeepSeek Prover V2란 무엇인가?

DeepSeek Prover V2는 딥러닝 기반의 대형 언어 모델로, Lean 4라는 공식 증명 언어를 활용해 복잡한 수학적 문제를 자동으로 증명할 수 있도록 설계된 시스템입니다. 기존에는 AI가 자연어 이해나 기계 번역 같은 작업에 주로 활용되었지만, 이 모델은 수학처럼 엄격한 논리 체계 안에서도 강력한 성능을 보여주고 있습니다.

 

DeepSeek Prover V2는 두 가지 모델 버전으로 제공됩니다:

• ⚙️ 7B 모델: 가벼운 환경에서 테스트 가능
• ⚙️ 671B 모델: 대규모 연산용으로 높은 정확도 제공

📊  개발 배경과 목표

기존의 수학 증명 자동화 시스템은 제한적 문제에만 적용할 수 있었고, 대규모 문제 해결에는 한계가 있었습니다. DeepSeek Prover V2는 이러한 문제점을 해결하기 위해 개발됐습니다. 목표는 "비공식적 추론"과 "공식적 증명"을 하나의 통합된 프레임워크에서 결합하는 것입니다. 개발팀은 기존 DeepSeek V3 모델을 활용해 복잡한 문제를 여러 단계로 쪼개어(subgoal decomposition) 해결하는 방식을 도입했으며, 이렇게 분해된 문제들을 다시 통합해 최종 증명을 완성합니다. 이 과정은 마치 어려운 수학 문제를 단계별로 나눠서 풀어가는 인간의 사고 방식과 유사합니다.

---

반응형

핵심 기능과 기술적 특징

🚀 강화 학습과 Subgoal 분해 기법

DeepSeek Prover V2의 가장 큰 강점은 강화 학습(Reinforcement Learning)을 활용한 점입니다. 이 방식은 AI가 문제 해결 과정에서 스스로 학습하고 점점 더 나은 결과를 도출할 수 있게 만듭니다.

• ✔️ 어려운 문제를 작은 단계로 나누어(subgoal) 해결
• ✔️ 각 단계에서 증명 과정을 학습하고 보강
• ✔️ 최종적으로 전체 증명을 완성

📄 Lean 4를 활용한 공식 증명

Lean 4는 수학 공식 증명을 위해 개발된 강력한 언어입니다. DeepSeek Prover V2는 이 언어를 통해 형식적으로 검증 가능한 증명을 생성합니다. 이는 단순히 답만 구하는 것이 아니라, 실제 수학 논문처럼 단계별 증명 과정을 제공합니다.

 

Lean은 Microsoft에서 개발한 증명 지원 시스템으로, 복
잡한 수학 문제뿐만 아니라 소프트웨어 검증에도 널리 사용됩니다.

🔄 Recursive Proof Search 혁신

기존 증명 모델은 복잡한 문제를 한 번에 해결하려다 실패하는 경우가 많았습니다. DeepSeek Prover V2는 이 점을 극복하기 위해 Recursive Proof Search(재귀적 증명 탐색) 기법을 사용합니다. 이 방식은 복잡한 문제를 반복적으로 쪼개고 탐색하여 단계적으로 완성도 높은 증명을 만들어냅니다.

예시 코드:

from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
torch.manual_seed(30)

model_id = "DeepSeek-Prover-V2-7B"  # or DeepSeek-Prover-V2-671B
tokenizer = AutoTokenizer.from_pretrained(model_id)

formal_statement = """
import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- What is the positive difference between $120\%$ of 30 and $130\%$ of 20? Show that it is 10.-/
theorem mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := by
  sorry
""".strip()

prompt = """
Complete the following Lean 4 code:

```lean4
{}
```

Before producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.
The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.
""".strip()

chat = [
  {"role": "user", "content": prompt.format(formal_statement)},
]

model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True)
inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device)

import time
start = time.time()
outputs = model.generate(inputs, max_new_tokens=8192)
print(tokenizer.batch_decode(outputs))
print(time.time() - start)

---

성능 평가와 벤치마크

📊 MiniF2F 테스트 결과

MiniF2F는 유명한 수학 문제 벤치마크로, DeepSeek Prover V2는 이 테스트에서 88.9%의 높은 통과율을 기록했습니다. 이는 현재까지 발표된 수학 증명 AI 중에서도 상위권 성적입니다.

🏆 PutnamBench 성능 리뷰

PutnamBench는 미국 대학 수학 경시대회 문제들로 구성된 벤치마크입니다. DeepSeek Prover V2는 총 658개 문제 중 49개를 정확히 증명했으며, 이는 인간 수준의 사고 방식을 모방해낸 결과로 평가됩니다.

📚 ProverBench 성능 리뷰 

ProverBench는 총 325개의 문제로 구성된 벤치마크 데이터셋입니다. 이 중 15문제는 AIME 24·25 대회의 수론 및 대수 문제를 정형화한 것으로, 실제 고등학교 경시대회 수준의 문제들입니다. 나머지 310문제는 교재 예제와 교육용 튜토리얼에서 엄선된 문제들로 구성돼 있어 다양한 수학적 주제를 다룹니다. 이 벤치마크는 고등학교 경시 수준부터 대학 수준의 수학 문제까지 폭넓은 평가를 할 수 있도록 설계되었습니다. DeepSeek Prover V2는 AIME 24·25 의 15문제중 6문제를 증명하였습니다. 

---

활용 사례와 적용 분야

DeepSeek Prover V2는 단순한 수학 증명용 AI를 넘어 다음과 같은 분야에서 활용 가능합니다:

• 🏫 교육: 수학 증명 학습 보조
• 🔬 연구: 이론 검증 및 수학적 모델링
• 🖥️ 소프트웨어: 코드 검증 및 정형 분석

---

결론: Deepseek Prover V2의 미래 

DeepSeek Prover V2의 주요 강점은 다음과 같습니다:

• ✅ 비공식적 추론과 공식적 증명의 결합
• ✅ 높은 증명 정확도
• ✅ 사용 편의성

그러나 다음과 같은 한계도 존재합니다:

• ⚠️ 매우 큰 모델은 고성능 GPU가 필요
• ⚠️ 일부 고난도 문제는 여전히 미해결

DeepSeek Prover V2는 수학뿐 아니라 법률, 과학, 소프트웨어 검증 등 다양한 분야로 확장될 가능성이 큽니다. AI가 인간의 고차원적 사고를 얼마나 빠르게 따라잡을 수 있는지 지켜보는 것도 흥미로울 것입니다.

---

출처

https://github.com/deepseek-ai/DeepSeek-Prover-V2

GitHub - deepseek-ai/DeepSeek-Prover-V2