لقد حققت النماذج اللغوية الكبيرة تقدماً ملحوظاً في التفكير الرياضي، الذي يُعدّ مختبرًا مهمًا لذكاء اصطناعي، وقد يُحدث تأثيرًا كبيرًا على الأبحاث العلمية إذا تم تطويره أكثر. من خلال توسيع القدرة على الاستدلال باستخدام التعلم المعزز الذي يُكافئ الإجابات النهائية الصحيحة، تحسّنت أداء النماذج اللغوية الكبيرة من أداء ضعيف إلى تحقيق أداء مُشبِع في المسابقات الكمية مثل AIME وHMMT خلال سنة واحدة فقط. ومع ذلك، يواجه هذا النهج قيودًا جوهرية. فالمُضي قُدمًا نحو دقة أعلى في الإجابة النهائية لا يعالج مشكلة رئيسية: فالإجابة الصحيحة لا تضمن بالضرورة صحة الاستدلال. علاوةً على ذلك، تتطلب العديد من المهام الرياضية، مثل إثبات النظريات، استنتاجات خطوة بخطوة صارمة، بدلًا من مجرد إجابات عددية، ما يجعل مكافآت الإجابة النهائية غير مناسبة في هذه السياقات. ولدفع حدود التفكير العميق، نعتقد أنه من الضروري التحقق من شمولية وصرامة التفكير الرياضي. ويُعد التحقق الذاتي أمرًا بالغ الأهمية عند توسيع حسابات وقت الاختبار، خاصة في المسائل المفتوحة التي لا توجد لها حلول معروفة. تجاه التفكير الرياضي القابل للتحقق ذاتيًا، نستعرض كيف يمكن تدريب نموذج مُحقق دقيق وموثوق مبني على النموذج اللغوي الكبير لغرض إثبات النظريات. ثم نُدرّب مُولِّد البراهين باستخدام هذا المُحقق كنموذج مكافأة، ونُشجع المُولِّد على اكتشاف وحل أكبر عدد ممكن من المشكلات في براهينه قبل تثبيتها نهائياً. ولضمان بقاء الفجوة بين التوليد والتحقق مع تقوية المُولِّد، نقترح توسيع قدرات التحقق تلقائيًا لتسمية البراهين الصعبة التي يصعب التحقق منها، مما يُنتج بيانات تدريب لتحسين المُحقق بشكل مستمر. وقد أظهر النموذج الناتج، DeepSeekMath-V2، قدرات قوية في إثبات النظريات، حيث حقق درجات ذهبية في IMO 2025 وCMO 2024، وحقق تقريبًا الدرجة الكاملة 118/120 في مسابقة Putnam 2024 باستخدام حسابات مُوسّعة وقت الاختبار. وعلى الرغم من أن هناك الكثير من العمل المتبقي، فإن هذه النتائج تشير إلى أن التفكير الرياضي القابل للتحقق ذاتيًا يُعدّ اتجاهًا بحثيًا واقعيًا، وقد يسهم في تطوير أنظمة ذكاء اصطناعي رياضية أكثر كفاءة.