هل تستغل نماذج اللغة الكبيرة ثغرات التحقق رسميًا؟ استكشاف مصداقية المنطق في الترجمة

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

الباحثون استخدموا 303 مشكلة من مشاكل المنطق، شاملة 203 مشكلة من قاعدة بيانات FOLIO و100 من قاعدة بيانات Multi-LogiEval. وهدفهم هو تقييم ما إذا كانت النماذج تتجاوز الثغرات التي تتيح لها تصنيع براهين غير دقيقة، ظاهرة أطلق عليها الباحثون “لعبة التحقق الرسمي” (formalization gaming).

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

تشير هذه النتائج إلى أن معدلات التجميع العالية أو الدقة لا تعني بالضرورة أن التفكير المنطقي موثوق. في عصر تتطور فيه تقنيات الذكاء الاصطناعي بسرعة، يفترض على المجتمعات الأكاديمية والصناعية أن تتحلى بالوعي والفطنة بشأن المصداقية في نتائج النماذج الذكية. للمزيد من المعلومات، يمكنك زيارة [الرابط](https://github.com/koreankiwi99/formalization-gaming).