DeepSeek-Prover-V2를 소개합니다!
Lean 4 기반 **형식 정리 증명(formal theorem proving)**을 위해 설계된 **오픈소스 대규모 언어 모델(LLM)**입니다! 🚀
이번 연구에서는 DeepSeek-V3를 활용한 재귀적 정리 증명 파이프라인을 통해 복잡한 문제를 **서브골(subgoal)**로 분해하고, 각 서브골에 대한 해결 과정을 chain-of-thought reasoning 형태로 구조화하여 초기 cold-start 학습 데이터로 활용했습니다.
이 과정을 통해 비형식적인 자연어 추론과 형식적인 수학 증명을 통합한 모델을 구축할 수 있었습니다.
그 결과 탄생한 모델이 바로 DeepSeek-Prover-V2-671B입니다:
• MiniF2F-test에서 88.9% 통과율 달성
• PutnamBench 문제 658개 중 49개 해결
• 새로운 벤치마크인 ProverBench 공개 (총 325문항 포함, AIME 2024–2025 문제 15개 포함)
AIME 문제 15개 중 DeepSeek-Prover-V2는 6개를 정확히 해결, 비교 모델인 DeepSeek-V3는 다수결 방식으로 8개 해결.
이는 형식과 비형식 수학 추론의 간극이 빠르게 좁혀지고 있음을 보여줍니다! 🔍📐
형식 수학 분야에서도 논리적, 체계적, 자율적으로 사고할 수 있는 LLM의 시대가 도래하고 있습니다.
#인공지능 #AI #LLM #정리증명 #형식검증 #Lean4 #DeepSeek #오픈소스 #수학AI #수학문제해결 #ChainOfThought #ReinforcementLearning #FormalMethods #AIME #Putnam #AI연구 #수학과AI
