مع تزايد الاعتماد على نماذج الذكاء الاصطناعي (AI) في مختلف المجالات، أصبح تقييم قدرات التفكير المنطقي لهذه النماذج ضرورة ملحة. وقد ظهرت برهنة النظريات الرياضية الرسمية (Formal Theorem Proving) كأداة رئيسية تتيح إمكانية التحقق الآلي من صحة الإثباتات الرياضية على نطاق واسع. لكن، قد يواجه الباحثون تحديات تتعلق بنقص البيانات المتاحة بسبب تكاليف التنسيق اليدوي المرتفعة ونقص المشكلات المثيرة للاهتمام.

هنا تأتي الفكرة المبتكرة: الاعتماد على علم الكمبيوتر النظري (Theoretical Computer Science) كمصدر شامل لمشكلات الإثبات الصارمة. من خلال التعريفات الخوارزمية، يمكن توليد العديد من أزواج تحديات البرهنة بشكل آلي. في هذه الدراسة، تم تطبيق هذه المنهجية على منطقتين في علم الكمبيوتر النظري: مشكلات Busy Beaver التي تتطلب إثبات حدود سلوك توقف آلات تورنج، ومشكلات Mixed Boolean Arithmetic التي تجمع بين التفكير المنطقي والحسابي.

من خلال إطار عملنا، تم توليد المشكلات بشكل متوازي، حيث توفر المواصفات الرسمية (Lean4) وغير الرسمية (Markdown) مسارًا قابلاً للتوسع لإنشاء تحديات إثبات موثوقة. وتظهر التقييمات التي تمت على نماذج الذكاء الاصطناعي الرائدة نقصًا كبيرًا في كفاءة البرهنة الآلية: حيث حقق نموذج DeepSeekProver-V2-671B نسبة نجاح تصل إلى 57.5% في مشكلات Busy Beaver، لكنه حصل على 12% فقط في مشكلات Mixed Boolean Arithmetic.

تسلط هذه النتائج الضوء على الصعوبة التي تواجهها نماذج الذكاء الاصطناعي في توليد الإثباتات المطولة حتى في المشكلات القابلة للتحقق حسابيًا، مما يبرز قيمة علم الكمبيوتر النظري في دفع البحث نحو المزيد من التقدم في الأبحاث المتعلقة بالتفكير الآلي.