الذكاء الاصطناعي يتحقق رياضيًا من جزء من شيفرة Signal في نصف يوم وبأقل من 500 دولار بدل 5 أشهر

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

لماذا الرياضيات بدل الاختبارات

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

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

ولهذا يُستخدم الأسلوب حيث تكون كلفة الخطأ مرتفعة. ووفق ما أعلنته الشركات، توجد شيفرة جرى التحقق منها رسميًا في طائرات Boeing وعلى خوادم Amazon وفي أكثر من 2,5 مليار جهاز نشط من Apple. وتتعلق هذه الشيفرة عادةً بالأمن. ويقول Byron Cook من Amazon Web Services إن التحقق أزال تساؤلات العملاء حول حماية السحابة وسرّع عمل الفرق الداخلية، إذ كانت الأخطاء الكبيرة تُكتشف مبكرًا.

من يراهن على الذكاء الاصطناعي وبماذا

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

• &Truth. جمعت 70 مليون دولار، وانضمت إليها Sun في أغسطس، وأُطلقت علنًا يوم الخميس. هدفها أن تتمكن مع الوقت من فحص الشيفرة بأي لغة برمجة.

ويشبّه المدير العلمي Ilya Sergey هذا النهج بالبناء: الجسور والمباني لا تنهار لأنها حُسبت قبل تشييدها، فلماذا لا نفعل الشيء نفسه مع الشيفرة. • Harmonic. شارك في تأسيسها رئيس Robinhood فلاد تينيف، وقد جمعت 295 مليون دولار.

وأعلنت الشركة هذا الأسبوع أن وكيلها الرياضي Aristotle قادر على فحص برامج C وأوصاف الدوائر المتكاملة بلغة Verilog. ويقيّم التقنيةَ عملاء محتملون، بينهم الشركتان المصنّعتان للرقاقات Tensordyne وNvidia؛ والذراع الاستثمارية لـ Nvidia من بين المستثمرين. • **Anthropic وTheorem.

** أعلنتا قبل أسبوع أنهما اكتشفتا بالذكاء الاصطناعي أخطاءً في برمجيات مفتوحة المصدر لم تلتقطها تريليونات الاختبارات. كما أُطلقت إضافة لـ Claude تساعد المطورين في التحقق. ولم تكشف الشركتان عن كلفة المشروع الأول.

• Truidic. أسسها Madan Musuvathi الذي غادر Microsoft Research بعد أكثر من 20 عامًا من العمل. ويرى أن الذكاء الاصطناعي قوي جدًا في يد المهاجمين، وأن التحقق قد يجعله آمنًا.

• Proofcraft. تعمل منذ زمن طويل في التحقق الكلاسيكي. وتقول قيادتها June Andronick وGerwin Klein إن تدفق الطلبات يفوق قدرتهما وقدرة منافسيهما.

وتجرّب المشاريع المفتوحة الأسلوب أيضًا. فقد فحصت مؤسسة Beneficial AI Foundation غير الربحية هذا العام، بمنحة من Anthropic، شيفرة التشفير نفسها التي فحصتها Sun. ويأمل Michael Rosenberg، أحد القائمين على صيانة مكتبة curve25519-dalek، في تمويل دائم لهذه الأعمال، لكنه لا يعرف من أين سيأتي، ولا يريد الاعتماد على حسن نية شركات الذكاء الاصطناعي.

أين يصطدم الأسلوب بسقفه

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

وهناك اعتراضات مبدئية أيضًا. فالإثبات يستند إلى افتراضات حول كيفية تفاعل الحواسيب والبشر مع البرنامج. وقد لا يرصد أخطاء المستخدم ولا أعطال العتاد. ويصف Will Wilson، رئيس الشركة الناشئة Antithesis (للبحث عن الأخطاء بالذكاء الاصطناعي)، التحقق الرسمي بأنه «فخ» لعشاق الرياضيات مثله. فقد أنفقت شركته ملايين الدولارات على التحقق من جزء من حمايتها، ووصفت العملية بأنها «مصدر إزعاج شديد». ومع ذلك عثرت أداتها الخاصة على أخطاء إضافية لديها، وعلى أخطاء في برمجيات عملاء كانوا قد تحققوا منها رسميًا. وخلاصة Wilson أن التحقق يمنح قدرًا من الثقة، لكن لا يؤكدها إلا الاختبار الشامل. وكتب فيتاليك بوتيرين في مدونته أيضًا أن التحقق الرسمي ليس حلًا سحريًا، وإن رأى أنه حماية مهمة من الهجمات السيبرانية المنفَّذة بالذكاء الاصطناعي.

وترى Andronick وKlein خطرًا آخر: إذا كتب الذكاء الاصطناعي وصف المهمة، تنشأ «ثقة غير مبررة» بالنتيجة. فالإثبات صحيح بقدر صحة وصف ما يُعد صوابًا.

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