التحقق الرياضي ضرورة لضبط برمجيات الذكاء الاصطناعي

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

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

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

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

ويمتد هذا القلق، بحسب المقال، إلى الشيفرات التي تشغّل المستشفيات والمصارف وشبكات الكهرباء. ويشير النص إلى إعلان شركة أنثروبيك في أبريل عن قدرة نموذج «ميثوس» على اكتشاف ثغرات غير معروفة في أنظمة تشغيل ومتصفحات رئيسية، مع تقييد الوصول إليه لخمسين جهة تعمل على معالجة تلك الثغرات. كما أورد أن مهندسين في مايكروسوفت رصدوا لاحقاً 90 خللاً حرجاً في منتج واسع الاستخدام، وأن السيناتور مارك وارنر نقل في جلسة استماع بمجلس الشيوخ، استناداً إلى مدير وكالة الأمن القومي، أن الأداة تمكنت من اختراق معظم الأنظمة الأميركية المصنفة خلال ساعات.

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

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

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