DeepMind تتحقق خلال شهر من جزء من تشفير Signal بمساعدة الذكاء الاصطناعي

الاختبارات تنجح، والمراجعة لا تجد مشكلات، ومع ذلك لا تزال الثقة في الشيفرة الحرجة غائبة. وهذا مزعج على وجه الخصوص في التشفير: فقد تكون تركيبة نادرة من الشروط أهم من ألف تشغيل ناجح. وبحسب ما نقلته ZDNET، طبّقت Google DeepMind أداة AlphaProof Code على جزء من الشيفرة التشفيرية في Signal وأنجزت التحقق خلال شهر. وتكمن الأهمية العملية هنا في محاولة تقليص الجهد اليدوي اللازم لبناء البراهين الرياضية.

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

ما الذي يُتحقَّق منه رياضيًا

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

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

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

كيف وُزّع العمل بين البشر والوكلاء

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

تذكر الوسيلة الإعلامية أنه جرى تعليم نحو 1% من قاعدة الشيفرة لإعادة فحصها يدويًا. وينبغي قراءة هذا الرقم بحذر: فالنص لا يوضح كيف حُدّد المقام ولا ما الذي عُدّ جزءًا مُتحقَّقًا منه. وهو لا يعني أن الذكاء الاصطناعي أكّد بنفسه أمان الـ99% المتبقية من تطبيق Signal كله.

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

أما المدة الشهرية فتحتاج بدورها إلى سياق. فـ ZDNET تقارنها بعمل كان قد يستغرق من الخبراء سنوات، لكنها لا تذكر مشروعًا مماثلًا للمقارنة ولا تكلفة الحوسبة ولا حسابًا مفصلًا للجهد البشري. لذلك من المبكر أن نَعِد الفرق بتسريع مماثل.

ماذا يفعل المطوّر ومدير المنتج

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

ومن المفيد لمدير المنتج أن يحدّد مسبقًا حدود الوعد المقدَّم للمستخدم. فالخاصية المُثبتة لوحدة تشفيرية لا تقول تلقائيًا شيئًا عن حماية الجهاز أو الواجهة أو النسخ الاحتياطية أو سلامة التحديثات. وهذه المسائل تتطلب فحوصًا خاصة بها.

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