딥시크, 수학 정리 증명 특화 AI 모델 Prover V2 공개

중국 AI 연구소 딥시크(DeepSeek)가 형식적 수학 추론과 정리 증명에 특화된 AI 모델 '딥시크-프루버-V2(DeepSeek-Prover-V2)'를 공개했다. 7B와 671B 두 가지 파라미터 크기로 제공되며, 평가 데이터셋과 함께 허깅페이스(Hugging Face) 플랫폼에 업로드되었다.

프루버-V2는 전 세계 수학자들이 사용하는 증명 보조 도구 린(Lean) 4에서의 정리 증명을 위해 설계된 오픈소스 대규모 언어 모델이다. 671B 버전은 딥시크-V3-Base 위에서 훈련되었고, 소형 7B 버전은 최대 32K 토큰의 확장된 컨텍스트 길이를 지원한다.

훈련 방법론이 특히 혁신적이다. 먼저 딥시크-V3를 활용해 복잡한 수학 문제를 일련의 하위 목표(subgoal)로 분해한다. 해결된 하위 목표의 증명들을 단계별 추론과 결합한 사고 과정으로 합성하고, 이를 강화학습의 초기 토대로 삼아 모델의 능력을 더욱 정제하는 방식이다.

성능은 인상적이다. 671B 버전은 MiniF2F-test 벤치마크에서 88.9%의 통과율을 기록하며 신경망 기반 정리 증명 분야에서 최첨단 성능을 달성했다. 고난도 수학 경시대회 문제 모음인 PutnamBench에서는 658문제 중 49문제를 풀었고, 2024-2025 AIME 경시대회 문제 15개 중 6개를 해결했다.

이번 공개는 수학적 추론이라는 특수 분야에 대한 딥시크의 지속적인 투자를 보여준다. 과학 연구, 소프트웨어 검증, 교육 등 다양한 분야에 파급 효과를 미칠 수 있는 영역이다. 325개의 형식화된 문제를 담은 ProverBench 데이터셋도 함께 공개되어 전 세계 연구자들이 이 성과를 기반으로 후속 연구를 진행할 수 있게 되었다.