딥시크 프루버-V2: AI 수학 증명의 새로운 지평을 열다
딥시크(DeepSeek)에서 수학 분야에 특화된 강력한 인공지능(AI) 모델, 딥시크 프루버-V2(DeepSeek-Prover-V2)를 오픈 소스로 공개했습니다. 이 모델은 특히 린 4(Lean 4)라는 정형 증명 도우미(formal proof assistant) 언어를 사용하여 수학 정리를 엄격하게 증명하는 정형 정리 증명(formal theorem proving) 분야를 위해 설계되었습니다.
공식적인 큰 발표 없이 조용하게 공개되었는데, 이는 차세대 모델 출시에 앞서 기술적 완성도를 점검하고 개발 커뮤니티로부터 피드백을 얻으려는 의도로 보입니다.
딥시크 프루버-V2는 어떻게 수학을 증명할까요?
딥시크 프루버-V2의 핵심에는 재귀적 정리 증명 파이프라인(recursive theorem proving pipeline)이라는 독특한 방식이 있습니다. 복잡한 수학 문제를 증명하는 과정은 마치 큰 산을 작은 언덕으로 나누어 오르는 것과 같습니다.
- 문제 분해 및 정형화: 먼저, 딥시크-V3(DeepSeek-V3) 모델이 복잡한 정리나 문제를 여러 개의 더 작은 하위 목표(subgoals)로 분해하는 것을 돕습니다. 동시에, 이 하위 목표들을 린 4 언어로 정형화(formalization)하여 컴퓨터가 이해하고 처리할 수 있는 형태로 만듭니다. 마치 문제의 개요(proof sketches)를 잡으면서 동시에 각 단계를 정확한 수학 언어로 번역하는 것과 같습니다.
- 하위 목표 증명: 각 하위 목표는 더 작은 7B 매개변수(parameter) 모델이 증명을 시도합니다. 이는 계산 부담을 줄이기 위한 효율적인 방법입니다.
- 학습 데이터 생성: 하위 목표들이 성공적으로 증명되면, 이 증명 과정들이 모여 완전한 정형 증명(formal proof)을 만듭니다. 이 정형 증명은 딥시크-V3가 문제를 분해할 때 사용했던 사고의 사슬(chain-of-thought), 즉 단계별 추론 과정과 결합됩니다. 이렇게 비정형적인 추론과 정형적인 증명이 결합된 데이터는 모델 학습을 위한 콜드 스타트 데이터(cold-start data)로 활용됩니다.
모델 학습 과정과 성능
딥시크 프루버-V2는 이렇게 생성된 합성 콜드 스타트 데이터(synthetic cold-start data)를 사용하여 초기 학습을 진행합니다. 특히, 7B 모델로 한 번에 풀기 어려운 문제 중에서도, 모든 하위 목표가 해결된 문제들을 활용하여 완전한 증명을 구성하고 이를 딥시크-V3의 추론 과정과 연결합니다.
이후에는 강화 학습(reinforcement learning) 단계를 거쳐 모델의 성능을 더욱 향상시킵니다. 강화 학습에서는 증명 결과가 '맞다' 또는 '틀리다'는 이진 피드백(binary feedback)을 보상 신호로 사용하여 모델이 비정형적인 추론과 정형적인 증명 구성을 더 잘 연결하도록 학습시킵니다.
이러한 과정을 거쳐 탄생한 딥시크 프루버-V2-671B 모델은 신경망 기반 정리 증명 분야에서 최첨단 성능(state-of-the-art performance)을 달성했습니다. 미니F2F 테스트(MiniF2F-test)에서 88.9%의 합격률(pass ratio)을 기록했으며, 푸트넘벤치(PutnamBench)의 658개 문제 중 49개를 해결했습니다. 미니F2F 데이터셋에 대한 증명 결과는 다운로드 가능합니다. (참고로, 공개 초기에는 다른 회사 모델과의 직접적인 비교 벤치마크 결과는 포함되지 않았다는 기사 내용도 있습니다.)
새로운 평가 데이터셋: 프루버벤치
딥시크는 모델 성능을 평가하기 위한 새로운 벤치마크 데이터셋(benchmark dataset)인 프루버벤치(ProverBench)도 함께 공개했습니다. 이 데이터셋은 총 325개의 문제로 구성되어 있습니다.
- AIME 24 & 25: 15개 문제. 최근 고등학교 수준의 수학 경시대회(AIME) 문제에서 정형화되었습니다.
- 기타: 310개 문제. 다양한 교과서 예제(textbook examples)와 교육 자료에서 가져왔으며, 대학 수준 수학 문제 평가에 기여합니다.
프루버벤치 데이터셋의 세부 구성은 다음과 같습니다:
- AIME 24&25: 15개
- 정수론(Number Theory): 40개
- 초등 대수학(Elementary Algebra): 30개
- 선형 대수학(Linear Algebra): 50개
- 추상 대수학(Abstract Algebra): 40개
- 미적분학(Calculus): 90개
- 실해석학(Real Analysis): 30개
- 복소 해석학(Complex Analysis): 10개
- 함수 해석학(Functional Analysis): 10개
- 확률론(Probability): 10개
- 총계: 325개
이 데이터셋은 고등학교 수준부터 대학 수준까지의 수학 문제를 아우르며, 모델의 포괄적인 평가를 가능하게 합니다.
모델 종류 및 활용
딥시크 프루버-V2는 두 가지 크기로 공개되었습니다: 7B 매개변수 모델과 671B 매개변수 모델입니다.
- 딥시크 프루버-V2-671B: 딥시크-V3-Base 모델을 기반으로 훈련되었습니다. 전문가 혼합(MoE: Mixture-of-Experts) 아키텍처를 채택했으며, 딥시크-V3와 동일한 아키텍처를 공유합니다. (https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B)
- 딥시크 프루버-V2-7B: 딥시크 프루버-V1.5-Base 모델을 기반으로 하며, 최대 32K 토큰(tokens)의 확장된 컨텍스트 길이(context length) 를 특징으로 합니다. (https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B)
두 모델 모두 허깅페이스(Hugging Face) 플랫폼을 통해 공개되었으며 다운로드하여 사용할 수 있습니다. 허깅페이스의 트랜스포머(Transformers) 라이브러리를 사용하여 모델 추론(inference)을 쉽게 수행할 수 있도록 파이썬 코드 예제도 제공됩니다.
딥시크 프루버-V2 모델 사용은 별도의 모델 라이선스(Model License) 정책을 따릅니다.
딥시크 프루버-V2는 수학 문제 해결, 특히 엄격한 정형 증명 분야에서 AI의 가능성을 보여주는 중요한 발전입니다. 재귀적인 문제 분해와 정형화, 합성 데이터 활용, 강화 학습 등 혁신적인 학습 방식을 통해 최첨단 성능을 달성했습니다. 함께 공개된 프루버벤치 데이터셋은 모델 평가를 위한 표준을 제공합니다.
비록 조용하게 공개되었지만, 이는 딥시크가 차세대 AI 모델(예: 딥시크-R2) 출시에 앞서 기반 기술을 다지고 있음을 시사하며, AI 경쟁 속에서 딥시크의 행보에 주목하게 만듭니다. 수학 분야에서 AI의 발전이 앞으로 어떤 새로운 가능성을 열어줄지 기대됩니다.
참고자료
- Hugging Face: deepseek-ai/DeepSeek-Prover-V2-7B (https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B)
- AI타임스: 딥시크, 수학 특화 AI 모델 ‘프루버-V2’ 조용히 공개 (박찬 기자, 2025.05.01) (https://www.aitimes.com/news/articleView.html?idxno=170101)