딥시크, 수학 추론 특화 모델 출시했다

중국 AI 기업 딥시크가 수학적 추론에 특화된 AI Prover 2세대 모델인 DeepSeek-Prover-V2를 허깅페이스와 깃허브에 공개했다. 이 모델은 동사의 대규모 언어 모델인 DeepSeek-V3 아키텍처를 기반으로 한 MoE(Mixture-of-Experts) 모델로 정리 증명 지원 언어인 Lean 4를 사용해 형식화한 정리 증명 생성을 자동화하도록 설계됐다.

DeepSeek-Prover-V2는 수학적 추론에 특화된 AI DeepSeek-Prover-V1.5 후속 모델로 DeepSeek-Prover-V1.5-Base를 기반으로 한 7B(70억 파라미터) 모델과 DeepSeek-V3-Base를 기반으로 한 671B(6710억 파라미터) 모델 두 종류가 제공된다.

7B 모델은 671B 모델보다 성능면에서는 열등하지만 배포와 추론에 필요한 리소스가 적게 들고 계산 비용이 낮아 실용적이다. 이전 세대 모델이 기반이 됐지만 최대 32K 토큰 컨텍스트 길이를 지원해 긴 증명이나 복잡한 추론이 필요한 문제도 다룰 수 있다. 671B 모델 특징은 DeepSeek-V3를 기반으로 한 재귀적 정리 증명 파이프라인에서 수집된 데이터로 학습된 점이다. 이 재귀적 정리 증명 파이프라인에서는 DeepSeek-V3로 복잡한 정리를 분해하면서 Lean 4로 형식화하고 7B 모델로 분해한 논리를 개별적으로 해결한다. 모두 해결한 뒤에는 DeepSeek-V3 비형식적 사고 연쇄를 통해 개별 증명을 조합해 복잡한 정리 증명을 구축한다. 671B 모델은 이 과정에서 생성된 데이터를 사용해 파인튜닝이 이뤄졌으며 인간과 같은 추론 능력과 엄격한 형식적 증명 능력을 겸비했다고 한다.

딥시크는 671B 모델이 수학 올림피아드 수준 문제를 수록한 MiniF2F-test 벤치마크에서 88.9% 합격률을 달성했고 정리 증명 알고리즘의 벤치마크(PutnamBench)에서 658문제 중 49문제를 해결할 수 있었다고 보고했으며 671B 모델이 정리 증명에서 현 시점 최첨단 성능을 갖고 있다는 걸 보여준다고 주장했다.

또 딥시크는 미국 수학 올림피아드 출전 자격 인증에 사용되는 AIME 시험 문제를 포함한 325문제로 구성된 새로운 정리 증명 벤치마크(ProverBench)도 동시에 발표했다. 그 중 2024년과 2025년 AIME에서 출제된 문제 15개를 이용한 성능 비교에서 671B 모델은 6문제를 해결했다고 한다. DeepSeek-V3가 같은 AIME 문제에서 8문제를 해결한 걸 고려하면 형식적 증명과 비형식적 추론의 성능 차이가 크게 줄어들다는 걸 보여준다는 주장이다.

DeepSeek-Prover-V2 671B 모델과 7B 모델은 깃허브와 허깅페이스에서 공개됐다. 또 허깅페이스 트랜스포머 라이브러리를 사용해 직접 추론을 수행할 수 있으며 사용자는 복잡한 설정 없이 모델을 쉽게 이용 시작할 수 있다.

딥시크는 아직 DeepSeek-Prover-V2 출시를 공식적으로 발표하지 않았지만 보도에 따르면 근일 내 발표 예정인 새로운 추론 모델 DeepSeek-R2에 대한 기대가 높아지는 가운데 이뤄진 출시라는 평가다. 관련 내용은 이곳에서 확인할 수 있다.