Nous introduisons DeepSeek-Prover-V1.5, un modèle linguistique open source conçu pour la preuve de théorèmes dans Lean 4, qui améliore DeepSeek-Prover-V1 en optimisant à la fois les processus d'entraînement et d'inférence. En pré-entraînement sur DeepSeekMath-Base, avec une spécialisation dans les langages mathématiques formels, le modèle subit un fine-tuning supervisé à l'aide d'un ensemble de données amélioré pour la preuve formelle de théorèmes, dérivé de DeepSeek-Prover-V1. Une réaffinement supplémentaire est obtenu grâce à l'apprentissage par renforcement à partir des retours d'assistant de preuve (RLPAF). Contrairement à l'approche de génération de preuve en un seul passage adoptée par DeepSeek-Prover-V1, nous proposons RMaxTS, une variante de recherche arborescente de Monte-Carlo qui utilise une stratégie d'exploration pilotée par une récompense intrinsèque afin de générer des chemins de preuve diversifiés. DeepSeek-Prover-V1.5 montre des améliorations significatives par rapport à DeepSeek-Prover-V1, atteignant de nouveaux records d'état de l'art sur l'ensemble de test du benchmark miniF2F de niveau lycée (63,5 %) et sur le benchmark ProofNet de niveau licence (25,3 %).