برهان OpenAI لمعادلات Navier-Stokes بلغة Lean لا يطابق النسخة باللغة الطبيعية، وفقًا لرياضيين

عدم التطابق بين برهانين

أعلنت OpenAI في 8 سبتمبر أنها وجدت حلاً لمسألة Navier-Stokes، وهي واحدة من أشهر المسائل المفتوحة في الرياضيات. نشرت الشركة البرهان بنسختين: إحداهما مكتوبة باللغة الطبيعية، مزيج من الإنجليزية والرموز الرياضية كما يكتب الرياضي البشري، والأخرى مكتوبة بلغة حاسوبية هي Lean، صُممت كتصيغ شكلي تتيح للحاسوب التحقق ميكانيكيًا من كل عبارة منطقية.

يقول الآن فريق من الرياضيين إن هاتين النسختين لا تتطابقان. يؤكد أندرس هانسن من جامعة كامبريدج وفابيان شيرشل، مع ألكسندر باستون من King's College في لندن، أن نموذج OpenAI ترجم جزءًا من البرهان بشكل غير صحيح عند نقله إلى Lean. ويشدد الباحثون على أن هذا لا يعني أن البراهين غير صحيحة أو أن OpenAI لم تحل المسألة، لكنه يثير شكوكًا حول إمكانية الاعتماد دائمًا على النتائج الرياضية التي يولّدها الذكاء الاصطناعي.

المبرهنة المُضعَفة

يشير إثبات الفريق إلى جزء من البرهان يُسمى المبرهنة 8.6. في البرهان المكتوب باللغة الطبيعية، تتطلب مقارنة هذا الجزء أن تكون قيمة معينة أقل من m + 4، حيث m عدد صحيح. في برهان Lean، يجب أن تكون القيمة المكافئة أقل من m + 5، وهو أضعف رياضيًا. كلا العبارتين قد تكونان صحيحتين، لكنهما تقولان شيئًا مختلفًا، ونسخة Lean تقدم إجابة أعم.

يقول الباحثون إن الانحراف يحدث لأن الذكاء الاصطناعي يجب أن ينشئ برهان Lean يُصرَّف، أي أن الشيفرة متسقة ذاتيًا تمامًا ولا تقبل الأخطاء. إذا وجد النموذج جزءًا لا يُصرَّف، سيحاول إيجاد طريق ملتوٍ، حتى لو كان ذلك يعني الانحراف عن البرهان المكتوب باللغة الطبيعية. تقدم OpenAI البرهانين على أنهما متطابقان وتعلن على Github أن المستودع يحتوي على صياغات Lean 4 للنتائج الواردة في الورقة البحثية.

عبء التحقق من براهين الذكاء الاصطناعي

تبين أن العثور على الانحراف أمر شاق. طلب الفريق من ChatGPT البحث عن عدم التطابقات المحتملة بين النسختين، ثم تحقق يدويًا من كل واحدة منها. تبين أن العديد من عدم التطابقات المقترحة غير صحيحة بعد التحقق. إجمالاً، استغرق الفريق حوالي أسبوعين لتحديد الانحراف الحقيقي، بينما يُقال إن وكلاء OpenAI استغرقوا 88 ساعة لتوليد البراهين.

المشكلة خاصة بالأهمية لأن OpenAI نشرت دفعة من 722 ورقة بحثية رياضية، جزء فقط منها مصحوب ببراهين Lean لم يتم التحقق منها يدويًا. قال كيفين بازارد من Imperial College في لندن إنه مقتنع بأن مسألة Navier-Stokes حُلّت بشكل صحيح، لكنه أقل اقتناعًا بكثير بأن البرهان الموصوف في PDF صحيح. وقال هانسن إن هناك حاجة إلى مزيد من العمل على تطوير تقنيات أتمتة شكلية قوية وأن الطريق النهائي لذلك غير معروف تمامًا.

المصادر: newscientist.com