2달 전
DeepSeek-Prover-V1.5: 증명 보조 피드백을 활용한 강화 학습 및 몬테카를로 트리 검색
Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, Chong Ruan
초록
우리는 Lean 4에서 정리 증명을 위한 오픈 소스 언어 모델인 DeepSeek-Prover-V1.5를 소개합니다. 이 모델은 훈련 및 추론 과정을 최적화하여 DeepSeek-Prover-V1의 성능을 향상시킵니다. DeepSeekMath-Base에서 사전 훈련되었으며, 형식적인 수학 언어에 특화되어 있습니다. 또한, DeepSeek-Prover-V1에서 파생된 개선된 형식적 정리 증명 데이터셋을 사용하여 감독 학습으로 미세 조정됩니다. 더욱이, 증명 보조 도구 피드백을 활용한 강화 학습(RLPAF)을 통해 추가적인 개선이 이루어집니다.DeepSeek-Prover-V1의 단일 패스 전체 증명 생성 방식을 넘어, 우리는 RMaxTS라는 Monte-Carlo 트리 탐색의 변형 방법을 제안합니다. RMaxTS는 내재 보상 주도 탐색 전략을 사용하여 다양한 증명 경로를 생성합니다. DeepSeek-Prover-V1.5는 DeepSeek-Prover-V1보다 크게 개선되었으며, 고등학교 수준의 miniF2F 벤치마크 테스트 세트(63.5%)와 대학 수준의 ProofNet 벤치마크 테스트 세트(25.3%)에서 새로운 최고 성능 결과를 달성했습니다.