Equivalence Checking of ML GPU Kernels
تقدم هذه الورقة Volta، وهو أول فاحص تكافؤ سليم وكامل لنواة وحدة معالجة الرسومات (GPU kernel)، والذي يتحقق رسميًا من صحة حسابات تعلم الآلة المُحسّنة يدويًا، أو بواسطة المترجمات، أو بواسطة النماذج اللغوية الكبيرة (LLMs).
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
في قلب الآلية الضخمة وغير المرئية للذكاء الاصطناعي الحديث، لا يحدث العمل الأكثر حيوية في السحابة، بل في رقائق حاسوبية متخصصة تُسمى وحدات معالجة الرسومات (GPUs). صُممت هذه الرقائق لأداء ملايين الحسابات الصغيرة في وقت واحد، وهو أمر ضروري لتدريب النماذج اللغوية الكبيرة التي تكتب الكود البرمجي الآن، وتترجم اللغات، وتولد الفنون. ولجعل هذه النماذج تعمل بالسرعة الكافية لتكون مفيدة، يجب على المهندسين كتابة تعليمات متخصصة للغاية، تُعرف باسم "النواة" (kernels)، والتي تخبر وحدة معالجة الرسومات بدقة بكيفية نقل البيانات وإجراء العمليات الرياضية. وخلال السنوات القليلة الماضية، بدأت الشركات في استخدام الذكاء الاصطناعي نفسه لكتابة هذه النواة، آملة في إيجاد طرق أسرع لإنجاز العمل مما يمكن للمهندسين البشر القيام به. ومع ذلك، فإن هذه السرعة تأتي مع مخاطرة: فعندما يقوم ذكاء اصطناعي أو "مترجم برمجيات" (compiler) بإعادة كتابة جزء من الكود ليكون أسرع، قد يتسبب دون قصد في إدخال أخطاء دقيقة. قد تتسبب هذه الأخطاء في جعل الكمبيوتر ينتج إجابة خاطئة، أو والأسوأ من ذلك، أن يتوقف عن العمل بشكل صامت بطرق يستحيل العثور عليها عبر الاختبارات القياسية. ويكمن التحدي الجوهري في أن هذه الرقائق تنفذ آلاف المسارات (threads) من العمل في وقت واحد، وإذا لم تنسق فيما بينها بشكل مثالي، فقد تتداخل مهامها، مما يخلق "حالة سباق" (race condition) حيث تعتمد النتيجة النهائية على الترتيب غير المتوقع للأحداث.
لقد طور فريق من الباحثين أداة جديدة تسمى "فولتا" (Volta) لحل هذه المشكلة. فبدلاً من التخمين فيما إذا كانت نسخة جديدة وأسرع من "النواة" صحيحة، تعمل "فولتا" كأداة تحقق رسمية تثبت رياضياً أن النسختين تنتجان نتائج متطابقة. بنى الباحثون نظاماً يأخذ التعليمات منخفضة المستوى لـ "نواة مرجعية" — وهي النسخة الأصلية الموثوقة — و"النواة المحسنة" — وهي النسخة الجديدة الأسرع — ويقوم بتمريرهما عبر محرك رمزي. وبدلاً من تغذية الكود بأرقام محددة لمعرفة النتيجة، يتعامل المحرك مع المدخلات كرموز مجردة. إنه يتتبع كل مسار محتمل يمكن أن يسلكه الكود، متتبعاً كيفية انتقال البيانات عبر آلاف المسارات المتوازية وكيفية تزامنها مع بعضها البعض. وإذا حاول الكود الوصول إلى الذاكرة بطريقة قد تسبب تعارضاً، أو إذا علقت المسارات في انتظار بعضها البعض إلى الأبد، تقوم الأداة فوراً بوضع علامة على الخطأ. وإذا عمل الكود بسلاسة، تقوم الأداة بترجمة المخرجات النهائية لكلا النواتين إلى تعبيرات رياضية معقدة وتتحقق مما إذا كانت تلك التعبيرات متطابقة جوهرياً، بغض النظر عن الأرقام المحددة التي يتم إدخالها إليها.
اختبر الباحثون "فولتا" على مجموعة متنوعة من مهام تعلم الآلة الواقعية، بما في ذلك عمليات ضرب المصفوفات، وعمليات الالتفاف (convolutions)، وآليات الانتباه (attention mechanisms) التي تشغل النماذج اللغوية الكبيرة. ووجدوا أن الأداة يمكنها التحقق بنجاح من النواة التي تم تحسينها يدوياً، أو بواسطة المترجمات، أو حتى بواسطة نماذج اللغات الكبيرة. وفي إحدى الحالات، فحصوا "نواة" أنشأها ذكاء اصطناعي وتم تحسينها من خلال ثلاث عشرة جولة من التحسين الآلي. أكدت "فولتا" أن هذا الكود الناتج عن الذكاء الاصطناعي مكافئ رياضياً للمرجع الأصما الذي كتبه البشر، مما أثبت أن التحسينات المكثفة لم تكسر المنطق البرمجي. كما أثبتت الأداة قيمتها من خلال اكتشاف أخطاء فاتت طرقاً أخرى؛ فعلى سبيل المثال، رصدت "سباقات بيانات" (data races) في درس تعليمي شهير ومستشهد به على نطاق واسٍ لبرمجة وحدات معالجة الرسومات، والذي استخدمه آلاف المطورين لسنوات. كانت هذه الأخطاء مخفية لأنها لا تظهر إلا في ظل ظروف توقيت محددة جداً نادراً ما تلتقطها الاختبارات القياسية. كما حددت الأداة خطأً في "نواة" أنشأها ذكاء اصطناعي حيث حاول الكود قراءة بيانات من موقع في الذاكرة غير موجود؛ وبينما تجاهلت الأجهزة الحالية هذا الخطأ، أظهر الباحثون أن الكود غير آمن أساساً ويمكن أن يفشل في الأجهزة المستقبلية.
تكمن قوة هذا النهج في قدرته على التعامل مع التعقيد الفريد لبرمجة وحدات معالجة الرسومات، حيث يجب على آلاف المسارات تنسيق إجراءاتها. كانت الأدوات السابقة قادرة على فحص البرامج أحادية المسار أو العمليات الرياضية عالية المستوى، لكنها واجهت صعوبة في تفكيك التوازي الهائل لوحدة معالجة الرسومات إلى أجزاء يمكن إدارتها. تتغلب "فولتا" على ذلك بافتراض أن "النوى" التي تحللها تتبع نمطاً هيكلياً محدداً شائعاً في تعلم الآلة، حيث يكون عدد المسارات وحجم البيانات معروفين مسبقاً. وضمن هذا الإطار، يمكن للأداة أن تثبت بيقين وجود "حالة سباق" إذا لم تكن المسارات متزامنة بشكل صحيح، ويمكنها إثبات أن نسختين مختلفتين من البرنامج متكافئتان إذا كانتا تنتجان نفس النتيجة الرمزية. أظهر الباحثون أن أداة تتبعهم يمكنها التحقق من هذه الخصائص في غضون ثوانٍ أو دقائق، حتى بالنسبة للنوى التي تحتوي على مئات الآلاف من التعليمات. كما أثبتوا أن المنطق الرياضي وراء أداتهم سليم، مما يعني أنه إذا قالت الأداة إن برنامجين متساويان، فهما متساويان حقاً لجميع المدخلات الممكنة.
يمثل هذا العمل خطوة هامة نحو جعل تطوير الذكاء الاصطناعي أكثر أماناً وموثوقية. ومع اعتماد الشركات المتزايد على الأنظمة الآلية لتوليد الكود الذي يشغل نماذجها، تصبح الحاجة إلى طريقة صارمة للتحقق من ذلك الكود أمراً بالغ الأهمية. لقد أظهر الباحثون أنه من الممكن تجاوز الاختبار البسيط، الذي يمكنه فقط فحص عدد محدود من السيناريوهات، إلى طريقة توفر ضماناً رسمياً للصحة. ومن خلال التحقق من تكافؤ "النوى" المحسنة، تمنح "فولتا" المطورين الثقة لاستخدام تحسينات أسرع وأكثر عدوانية دون خوف من إدخال أخطاء صامتة. الأداة متاحة حالياً للاستخدام، وقد جعل الباحثون الكود الخاص بهم والإثباتات الكامنة وراءه متاحين للجمهور، مما يسمح للآخرين بالبناء على هذا الأساس. ورغم أن الأداة لا تغطي بعد كل أنواع كود وحدات معالجة الرسومات، إلا أنها تتعامل بنجاح مع الغالبية العظمى من "النوى" التي تقود تعلم الآلة الحديث، مما يقدم معياراً جديداً للثقة في التوليد الآلي لكود الحوسبة عالية الأداء.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.