우리는 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%)에서 새로운 최고 성능 결과를 달성했습니다.