DeepSeek-Prover-V2 분석: 6710억 개 매개변수 모델이 AI 수학적 추론의 미래를 이끌 수 있는 이유
2025년 4월 30일, 중국 휴일 직전에 조용히 DeepSeek는 인공지능의 중요한 분야인 형식적 수학 추론에서 큰 반향을 일으키고 있는 모델을 공개했습니다. 광범위한 AI 경쟁이 챗봇 기능과 화려한 멀티모달 데모에 집중하는 동안, DeepSeek는 헤드라인을 장식하지 않지만 전략적으로 중요한 영역인 자동 정리 증명에 집중하고 있습니다.
DeepSeek-Prover-V2는 소셜 미디어에서 큰 관심을 받지 못할 수도 있지만, 그 영향은 학계, 엔지니어링 및 미래 AGI 시스템에 걸쳐 나타납니다. 6710억 개의 매개변수와 Lean 4 형식 증명과의 긴밀한 통합을 통해 수학 문제를 해결하는 것 이상으로 수학적 진실을 코드로 공식화합니다. 장기 투자자, 연구 기관 및 AI 인프라 이해 관계자에게 이 모델은 단순한 호기심이 아닌 벤치마크이자 잠재적으로 청사진입니다.
수학 엔진 콜드 스타트—DeepSeek가 정리 증명 LLM을 훈련하는 방법
DeepSeek-Prover-V2는 기존 모델을 미세 조정하는 데 그치지 않습니다. 핵심 혁신은 데이터가 매우 부족한 영역에서 모델 훈련을 위한 합성 "콜드 스타트" 데이터를 생성하는 방식에 있습니다.
이것이 왜 중요한지 이해하려면 형식 증명은 자연어와 달리 엄격한 논리, 엄격한 구문 및 검증 가능한 결과를 요구한다는 점을 고려하십시오. 용납하지 않습니다. 모호성이나 스타일 변화의 여지가 없습니다.
DeepSeek의 해답은 자체 기본 모델인 DeepSeek-V3를 교사로 사용하는 것입니다. 파이프라인은 복잡한 수학 정리를 일련의 구조화된 하위 목표로 분해하고, 각 하위 목표는 Lean 4를 통해 형식 논리로 변환됩니다. 이러한 증명 단계는 효율성을 위해 먼저 작은 70억 개 모델로 처리되며, 해결되면 일관된 사고 사슬 추론 추적으로 엮어 합성 콜드 스타트 데이터 세트를 형성합니다.
이 재귀적 생성 프레임워크는 영리할 뿐만 아니라 확장 가능합니다. DeepSeek는 기본적으로 수학자가 문제를 해결하는 방식을 모방하는 자체 학습 루프를 구축했습니다. 생각하고, 단순화하고, 증명하고, 종합합니다.
데이터에서 강화 학습으로—검증된 추론을 통한 훈련
콜드 스타트 데이터가 합성되면 DeepSeek는 강화 학습으로 이동합니다. 그러나 사람이 라벨링한 데이터가 아닌 검증 가능한 결과가 있는 문제를 사용합니다. 모델은 이진 피드백을 받습니다. 올바른 증명을 생성했습니까?
이 피드백 루프는 비공식 추론(LLM의 자연스러운 영역)과 형식 논리(Lean 4의 엄격한 영역)를 연결합니다. 최종 결과인 DeepSeek-Prover-V2-671B는 단어로 추론하는 것이 아니라 기계와 수학자가 모두 한 줄씩 검증할 수 있는 증명을 생성합니다.
성능 수치는 약속을 강화합니다.
- MiniF2F 테스트(수학적 추론 벤치마크)에서 88.9% 통과율
- 엘리트 수준의 수학 문제 세트인 PutnamBench에서 658개 문제 중 49개 해결
맥락상 이러한 수치는 신경 정리 증명에서 최첨단을 보여줍니다. 이미지 생성이나 대화 에이전트만큼 매력적으로 들리지 않을 수도 있지만 기본 기능은 강력하고 안정적인 AI 추론 시스템으로 훨씬 더 쉽게 이전할 수 있습니다.
ProverBench—형식화된 수학 평가를 위한 새로운 표준
모델과 함께 DeepSeek는 325개의 엄격하게 형식화된 문제 데이터 세트인 ProverBench를 출시했습니다. 여기에는 다음이 포함됩니다.
- 최근 AIME 대회에서 15개의 문제
- 대수학, 미적분학, 실수 및 복소수 분석, 확률과 같은 핵심 수학 영역에서 더 많은 문제
이는 형식 정리 증명의 이전 데이터 세트가 너무 합성적이거나 너무 좁았기 때문에 중요합니다. ProverBench는 균형을 제공합니다. 실제 교육 관련성, 경쟁적인 문제 난이도 및 다양한 수학적 구조입니다.
데이터 세트 분석:
| 영역 | 문제 수 |
|---|---|
| 미적분학 | 90 |
| 선형 대수학 | 50 |
| 추상 대수학 | 40 |
| 정수론 | 40 |
| AIME | 15 |
| 기타 | 90 |
DeepSeek는 모델과 이 벤치마크를 모두 출시함으로써 단순히 기능을 과시하는 것이 아니라 엄격한 비교와 공개 실험을 유도합니다.
투자자 영향—이 틈새 시장이 중요한 이유
평범한 관찰자에게 형식 정리 증명은 연구 허영심 프로젝트처럼 보일 수 있습니다. 그러나 AGI 경쟁을 추적하는 사람에게는 패턴이 점점 더 명확해지고 있습니다. DeepSeek의 로드맵은 다음을 우선시합니다.
- 수학 및 코딩 모델
- 멀티모달 통합
- 자연어 추론
그리고 그 순서대로.
Prover-V2와 같은 수학 모델이 투자 및 전략적 관점에서 특히 매력적인 이유는 검증 가능성입니다. 환각이 LLM의 아킬레스건인 세상에서 정리 증명기는 드문 이점을 제공합니다. 결정적 정확성입니다. 증명이 유지되거나 그렇지 않습니다.
여러 전문가들은 DeepSeek-Prover-V2가 최종 목표가 아니라 전략적 발판이라고 암시했습니다. 한 내부자는 이를 DeepSeek의 곧 출시될 일반 모델(잠재적으로 V4 또는 R2라는 코드명)을 위한 "데이터 합성기"라고 불렀습니다. 이러한 미래 시스템은 Prover-V2의 엄격한 추론을 보다 광범위하고 일반적인 모델에 통합하여 인간 수준의 정확도로 여러 영역에서 코딩, 쓰기 및 문제를 해결할 수 있습니다.
다시 말해 DeepSeek는 단어 예측을 넘어 논리적 추론과 신뢰할 수 있는 출력으로 나아가는 검증 가능하고 책임 있는 AGI 시스템의 토대를 조용히 구축하고 있을 수 있습니다.
기술 액세스 및 오픈 웨이트 출시
폐쇄형 모델이 점점 더 보편화되는 업계에서 DeepSeek가 70억 및 6710억 구성 모두에서 Prover-V2를 오픈 웨이트하기로 한 결정은 주목할 만합니다. 특히 교육, 연구 및 Lean 4용 툴체인 개발에서 글로벌 협업과 실험을 장려합니다.
두 모델 모두 Hugging Face에서 사용할 수 있으며 Transformers를 통해 쉽게 통합할 수 있습니다. 더 큰 6710억 개 모델은 DeepSeek-V3 아키텍처를 미러링하여 최대 32K 컨텍스트 길이와 추론 준비 성능을 제공합니다.
샘플 추론에는 다음을 포함한 완전한 Lean 4 코드 생성이 포함됩니다.
- 정리 공식화
- 증명 계획 생성
- Lean 구문을 사용한 공식 증명 실행
AI의 미래가 형식이 될 수 있는 이유
요약하면 DeepSeek-Prover-V2는 재미로 교과서 문제를 해결하는 것이 아닙니다. 한 번에 하나의 공식 증명으로 AI의 검증 문제를 해결하는 것입니다.
주요 내용:
- 재귀적 증명 합성은 확장 가능한 콜드 스타트 학습을 가능하게 합니다.
- 이 모델은 비공식 LLM 추론과 공식 증명 구조를 혼합합니다.
- 주요 수학 벤치마크에서 이전 모델보다 성능이 뛰어납니다.
- 미래 평가를 위한 새로운 공개 벤치마크(ProverBench)를 도입합니다.
- 검증 가능한 지능에 초점을 맞춘 광범위한 AGI 전략을 나타냅니다.
AI 투자자, 연구소 및 고급 엔지니어링 팀에게 DeepSeek의 형식 정리 증명 작업은 심각한 차세대 AI 기능이 더 넓은 대화가 아닌 더 깊고 입증 가능한 사고로 향하고 있음을 보여주는 가장 명확한 신호일 수 있습니다.
곧 출시될 DeepSeek R2: AI 분야의 강력한 새로운 경쟁자
중국 기술 회사 DeepSeek의 곧 출시될 AI 모델인 DeepSeek R2는 인상적인 사양과 비용 이점으로 서구 AI 지배력에 도전할 준비가 되어 있습니다. 2025년 5월 초에 출시될 예정인 R2는 이전 모델의 두 배인 1조 2천억 개의 매개변수를 가진 하이브리드 MoE(Mixture-of-Experts) 아키텍처를 특징으로 합니다. 이 모델은 Huawei의 Ascend 910B 칩 클러스터를 사용하여 5.2 페타바이트의 데이터로 훈련되어 82%의 하드웨어 활용도로 512 페타플롭의 놀라운 계산 효율성을 달성하는 것으로 알려져 있습니다.
R2의 예상 기능에는 향상된 추론, 이미지 및 비디오 지원을 위한 멀티모달 지원, 고급 코딩 기능, R1의 중국어 및 영어 기능 외에 확장된 다국어 지원이 포함됩니다. 아마도 가장 파괴적인 것은 DeepSeek의 보고된 비용 이점일 것입니다. R2는 OpenAI의 GPT-4o보다 97.3% 저렴하게 구축할 수 있으며 엔터프라이즈 가격은 백만 입력 토큰당 0.07달러에 불과할 것으로 예상됩니다. 이러한 비용 효율성은 서구 주요 모델과 비슷하거나 잠재적으로 우수한 성능과 결합되어 DeepSeek R2를 글로벌 AI 환경에서 중요한 경쟁자로 자리매김합니다. 이러한 사양은 공식 출시될 때까지 크게 확인되지 않았지만 AI 커뮤니티는 DeepSeek가 차세대 모델을 공개할 준비를 하면서 면밀히 주시하고 있습니다.