يتطلب تدريب نماذج اللغة الكبيرة (LLMs) على نطاق واسع تنفيذًا متوازيًا عبر آلاف الأجهزة، مما يؤدي إلى تكاليف حسابية ضخمة. ومع ذلك، فإن عمليات التدريب الموزعة هذه، رغم تكلفتها العالية، نادرًا ما يتم التحقق منها، مما يجعلها عرضة للأخطاء الصامتة وقد يضيع ملايين ساعات GPU. نقدم TrainVerify، وهو نظام للتحقق من التدريب الموزع لنماذج اللغة الكبيرة. بالنظر إلى المواصفة المنطقية لنموذج التعلم العميق كحقيقة أساسية، يتحقق TrainVerify رسميًا من أن خطة التنفيذ المتوازي الموزع تعادل رياضيًا لها. يعتبر التحقق المباشر صعبًا بشكل ملحوظ بسبب الحجم الهائل لنماذج اللغة الكبيرة التي غالبًا ما تتضمن مليارات المتغيرات ورسوم بيانية لحسابات معقدة للغاية. لذلك، يقدم TrainVerify تقنيات تقليل الشكل وخوارزمية تحقق متوازٍ مرحلة بمرحلة تقلل بشكل كبير من التعقيد بينما تحتفظ بالصواب الرسمي. يتوسع TrainVerify ليشمل نماذج اللغة الكبيرة المتقدمة، بما في ذلك التحقق الناجح من خطط تدريب Llama3 (405B) وDeepSeek-V3 (671B).
درس لو وآخرون (الخميس) هذا السؤال.