DeepSeek-Prover-V2: 강화 학습을 통한 형식적 수학적 추론 발전
2025-04-30
DeepSeek-Prover-V2는 Lean 4에서 형식적 정리 증명을 위해 설계된 오픈소스 대규모 언어 모델입니다. DeepSeek-V3 기반의 재귀적 정리 증명 파이프라인과 강화 학습을 활용하여 비형식적 및 형식적 수학적 추론을 통합합니다. 이 모델은 DeepSeek-V3을 사용하여 복잡한 문제를 하위 목표로 분해하고, 이러한 하위 목표의 증명을 합성하여 강화 학습의 초기 데이터를 만드는 것으로 시작합니다. DeepSeek-Prover-V2-671B는 MiniF2F-test에서 88.9%의 통과율을 달성하고 PutnamBench에서 49개의 문제를 해결했습니다. 또한 고등학교 경시대회 및 교과서에서 325개의 형식화된 문제를 포함하는 새로운 벤치마크 데이터 세트인 ProverBench도 도입되었습니다.
AI
정리 증명