نُقدِّم نموذج اللغة المفتوح المصدر DeepSeek-Prover-V1.5، المُصمم لبرهان النظريات في بيئة Lean 4، والذي يُحسِّن نموذج DeepSeek-Prover-V1 من خلال تحسين عمليتي التدريب والاستدلال. تم تدريب النموذج مبدئيًا على DeepSeekMath-Base، مع تخصُّص في اللغات الرياضية الرسمية، ثم تمت عملية التدريب المُراقبة الدقيقة باستخدام مجموعة بيانات مُحسَّنة لبرهان النظريات الرسمية المستمدة من DeepSeek-Prover-V1. وتم تحقيق تحسين إضافي من خلال التعلُّم التكراري من خلال تغذية راجعة مُقدَّمة من مساعدات البرهان (RLPAF). وبالإضافة إلى النهج القائم على إنتاج البرهان ككل في عملية واحدة المُتَّبَع في DeepSeek-Prover-V1، نُقدِّم RMaxTS، وهي نسخة مُعدَّلة من خوارزمية بحث شجرة مونت كارلو، تُستخدم فيها استراتيجية استكشاف مُشَوَّقة بعوائد داخلية لِتوليد مسارات برهان متنوعة. وقد أظهر DeepSeek-Prover-V1.5 تحسينات كبيرة مقارنةً بـ DeepSeek-Prover-V1، محقِّقًا نتائجًا جديدة على مستوى الحالة الراهنة (SOTA) على مجموعة اختبار معيار miniF2F بمستوى المدرسة الثانوية (63.5%) وعلى معيار ProofNet بمستوى الجامعة (25.3%).