DeepSeek, 재귀적 증명 탐색과 새로운 ProverBench 벤치마크를 갖춘 DeepSeek-Prover-V2 출시

DeepSeek AI가 DeepSeek-Prover-V2를 발표했습니다. 이는 Lean 4에서 형식 정리를 증명하기 위한 오픈소스 대규모 언어 모델입니다. 이 모델은 재귀적 정리 증명 파이프라인을 사용하며, DeepSeek-V3를 활용해 복잡한 정리를 하위 목표로 분해하고 형식화하여 고품질 초기화 데이터를 생성합니다. 그런 다음 70억 파라미터 모델이 이 하위 목표들을 증명하고, 완전한 증명은 DeepSeek-V3의 사고 연쇄 추론과 쌍을 이루어 학습에 사용됩니다. 이진 피드백을 이용한 강화 학습은 모델을 더욱 정교하게 만듭니다. 6710억 파라미터 버전은 MiniF2F-test에서 88.9%의 성과를 달성했으며, PutnamBench 문제 658개 중 49개를 해결했습니다. DeepSeek는 또한 수학적 추론 평가를 위한 AIME 대회와 교과서의 325개 문제로 구성된 데이터셋인 ProverBench를 도입했습니다. 이 모델은 70억 파라미터와 6710억 파라미터 두 가지 크기로 제공됩니다.