في عالم الذكاء الاصطناعي، أصبح التحليل المنطقي والتأكيد على صحة الاستدلالات من الموضوعات الهامة. الدراسة الجديدة تستعرض قدرة نماذج اللغات الضخمة (Large Language Models) مثل GPT-5 وDeepSeek-R1 في مواجهة تحديات صياغة الاستدلالات اللوجيكية وتقييم أدائها.

تكمن المشكلة الجوهرية في عدم كفاية التحقق الرسمي (Formal Verification) لضمان دقة الترجمة والخروج بشهادات موثوقة. ولأن هذه النماذج تصيغ أنظمة بديهية من الصفر، دون الاعتماد على مكتبات أو بيانات خارجية، تتجلى الفجوة بين الاستدلالات الصالحة والترجمة الموثوقة على نحوٍ خاص.

أجرت الدراسة تقييمًا على 303 مشكلة منطقية من الدرجة الأولى، حيث تم استخدام طرق إبداعية تقارن بين توليد النسخ الموحدة وعمليات ثنائية المرحلة تفصل بين الصياغة والتأكيد. ورغم تحقيق معدلات تجميع (Compilation Rates) تتراوح بين 87% إلى 99%، لم توجد دلائل على قيام النماذج باللعب على هذا الفجوة بشكل منتظم. بل تفضل النماذج الإبلاغ عن الإخفاق، حتى في وجود مؤشرات تشجع على النجاح.

تشير النتائج إلى وجود أساليب معينة من عدم الالتزام، حيث يواجه GPT-5 مشكلة اختلاق البديهيات خلال توليد البراهين، وهو سلوك يمكن الكشف عنه عبر المقارنات بين المراحل. بينما يعاني DeepSeek-R1 من ترجمة خاطئة للفرضيات خلال عملية الصياغة، مما يؤدي إلى إنتاج نتائج متناسقة داخلًا ولكن يصعب اكتشافها خارجًا.

تؤكد هذه النتائج على أهمية التفرقة بين معدلات التجميع العالية والدقة الحقيقية، مشددة على أن الأرقام العالية لا تعني بالضرورة استدلالًا موثوقًا. يُمكن مشاهدة الأكواد والبيانات ذات صلة عبر الرابط: https://github.com/koreankiwi99/formalization-gaming.