عالم رياضيات يرفض اختراق conjectures من OpenAI خلال 24 ساعة: 'الذكاء الاصطناعي أثبت كل جملة، لكنه لم يعد يتعلق بالفرضية الأصلية'

ادعت شركة OpenAI أن نموذج الذكاء الاصطناعي من الجيل التالي قام بحل عشر مسائل رياضية عالمية المستوى، بما في ذلك دحض حدسية صلابة كونيس. وفي اليوم التالي، ردت عالمة رياضيات بشرية بورقة بحثية تجادل بأن المثال المضاد الذي قدمه الذكاء الاصطناعي غير صالح. المؤلفة، ج. ل. نيلسن من مركز فيزياء الطوبولوجيا في جامعة كانساس، تتبعت 37,000 سطر من كود Lean 4 الذي كتبته OpenAI من البداية إلى النهاية، وعينت كل كائن إلى نظيره الرياضي، وحددت مسارين مستقلين للفشل. تنص حدسية صلابة كونيس على أنه إذا كانت مجموعتان لهما نفس البنية الجبرية المرتبطة وتحققت فيهما شرطان إضافيان (ICC وخاصية كازدان (T))، فإن المجموعتين يجب أن تكونا متشاكلتين. قام نموذج OpenAI ببناء مجموعتين غير متشاكلتين تولدان نفس الجبر، مع براهين على أن كلا المجموعتين تحققان خاصية ICC وخاصية (T). أشارت نيلسن إلى أن إحدى المجموعتين التي بناها الذكاء الاصطناعي لا تحقق في الواقع الشروط الإضافية، حيث أنها ليست ذات خاصية ICC ولا تمتلك خاصية (T). وذكرت ثلاثة أسباب محتملة: تمثيل الكود لخاصية (T) لا يطابق تعريف كازدان الأصلي؛ أو أن البرهان ينطبق فقط على جزء من المجموعة ولكن تم تطبيقه على المجموعة كاملة؛ أو أن المجموعة في الكود ليست هي ما تصفه الوثيقة التوضيحية. كما قامت نيلسن بفحص سطر بسطر للكود، مدرجة اسم كل كائن رياضي ورقم السطر في جدول مرجعي متقاطع. وجدت أن اللمّات المستخدمة لإثبات خاصية ICC تنطبق على الكائنات بعد تحويل مزدوج، وليس على المجموعة الأصلية مع عناصرها المركزية، لذا فهي لا تغطي العناصر الحرجة مباشرة. كتبت نيلسن تفنيديها ككود Lean ونفذتهما في إصدار Lean 4.32.2. يناقش القسم الأخير من الورقة السياق الأوسع: نواة Lean تضمن الصحة الشكلية، لكنها لا تضمن أن العبارة تثبت بالفعل الاستنتاج المقصود. نقلاً عن تيرينس تاو، التحقق من البرهان يفحص العبارة الشكلية نفسها، وليس توافقها مع النية، لذلك لا يمكن استبدال المراجعة البشرية. كشفت عمليات تدقيق سابقة لخمسة معايير شائعة لـ Lean عن 4,833 مشكلة، بما في ذلك أمثلة مضادة ونظريات فارغة وبديهيات غير موثوقة، وكلها تم التحقق منها آليًا، وبعد ذلك قام البشر ببناء أمثلة مضادة لإظهار أن العبارات المثبتة كانت خاطئة. كتبت نيلسن أن الصياغة الرسمية من OpenAI ربما تكون قد أثبتت بشكل صحيح كل استنتاج تدعيه، لكن ما لم تثبته - وما لا يمكن لنواة Lean التحقق منه - هو ما إذا كانت هذه الاستنتاجات تتعلق بصياغة الحدسية الأصلية. تظل حدسية صلابة كونيس مفتوحة.