نماذج اللغة والتحقق الرسمي: ماذا تعني كلمة "أُثبت" في 123 مكتبة

في 22 أكتوبر 2026 نشر فريق ⁨Frontier Red Team⁩ في ⁨Anthropic⁩، بالتعاون مع شركة اسمها ⁨Theorem⁩، نتيجة تستحق القراءة بتأنٍّ. استخدموا ⁨Claude⁩ لكتابة براهين رسمية لكود حقيقي مفتوح المصدر على مستوى لغة التجميع، في 123 مكتبة، ووجدوا في الطريق أخطاء صمدت أمام سنوات من الاختبار. إليك معنى ذلك ببساطة، وأين تتوقف كلمة "أُثبت"، وما الذي يأخذه منه فريق عادي اليوم.

التحقق الرسمي بلا مصطلحات

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

المشكلة كانت دائمًا الكلفة. يذكر المقال المثال المعروف: نواة ⁨seL4⁩ احتاجت سنتي عمل لبنائها و20 سنة عمل للتحقق منها. لذلك بقي التحقق الرسمي في مجالات مثل برمجيات الطيران.

ما الذي فعلوه بالضبط

كتابة المواصفة هي الجزء الأصعب عادة، فأعادوا استخدام مواصفة موجودة أصلًا: اختبارات الإدخال العشوائي (⁨fuzz tests⁩) في مشروع ⁨OSS-Fuzz⁩ من ⁨Google⁩. اختبار كهذا نقطة دخول تنهار حين يحدث خطأ، والأداة ترمي عليها أعدادًا هائلة من المدخلات المولّدة. قد تعمل سنوات ولا تكتمل أبدًا. حوّل الفريق كل اختبار إلى عبارة: نقطة الدخول هذه لا تنهار أبدًا، لأي مدخل أصغر من ⁨64 MB⁩، على الملف التنفيذي المترجم لمعمارية ⁨RISC-V⁩.

خلال بضعة أسابيع أصلح ⁨Claude⁩ الأخطاء التي صادفها وأثبت تلك العبارة لـ239 نقطة دخول في 123 مكتبة. مجموع البراهين نحو 180 مليون سطر بلغة ⁨Rocq⁩، والبرهان النموذجي نحو 600 ألف سطر، لملفات تنفيذية متوسطها 18 ألف تعليمة ⁨RISC-V⁩. لا أحد يقرأ ذلك يدويًا، بل يفحصه مدقق براهين ⁨Rocq⁩. ويحدد المقال ما يبقى عليك أن تثق به: النماذج الرسمية لمعمارية ⁨RISC-V⁩ ولعمليات ⁨Linux⁩، ونصوص المبرهنات بالضبط، والمدقق نفسه.

الأخطاء هي ما يستحق الانتباه

أدوات الاختبار العشوائي تعدّل مدخلات صغيرة، محدودة عادة بـ⁨1 MB⁩. وبعض ما كشفته البراهين يقع بعيدًا عن ذلك: نقصان عدّاد تحت الصفر في أداة فك ضغط سبّب كتابة خارج الحدود، لكن فقط مع مدخلات بحجم نحو ⁨20 MB⁩ وبترتيب نادر محدد؛ وقراءة خارج الحدود في فاك صور احتاجت مدخلًا بحجم ⁨64 MB⁩ وأكثر من ⁨2 GB⁩ من الذاكرة؛ وإعادة اكتشاف الثغرة ⁨CVE-2026-56132⁩ في ⁨libexpat⁩. وكشف أحد البراهين خطأ منطقيًا لا يسبب انهيارًا أصلًا: ميزة لتقييد الملفات التي يمكن للتطبيق تحميلها لم تكن تُطبَّق دائمًا. وخلاصة الكاتبين أن مجرد محاولة البرهان تجد أخطاء حقيقية، اكتمل البرهان أم لا.

أين تتوقف كلمة "أُثبت"

المقال صريح في هذا، وأراه أنفع أقسامه. "متحقَّق منه رسميًا" لا تعني "خالٍ من الأخطاء"، بل تعني أن الكود يلتزم القواعد المكتوبة، على الآلة التي جرت نمذجتها. ويسمّي فجوتين:

• الآلة. البراهين تخص ملفات ⁨RISC-V⁩ ثابتة الربط وأحادية الخيط ومربوطة بمكتبة ⁨musl⁩. أما أغلب الناس فيشغّلون هذه المكتبات على ⁨x86⁩ أو ⁨ARM⁩ بربط ديناميكي مع ⁨glibc⁩.
• العبارة. أداة ⁨AddressSanitizer⁩ لا تلتقط كل أخطاء الذاكرة، ولم يجرِ التحقق من كل نقاط الدخول، وما زال بوسع الكود المستدعي أن يسيء استخدام المكتبة.

ماذا يعني هذا لفريق عادي

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

#include <assert.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>

/* your library's own functions; the names are placeholders */
size_t encode(const uint8_t *in, size_t n, uint8_t **out);
size_t decode(const uint8_t *in, size_t n, uint8_t **out);

int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
  uint8_t *packed = NULL, *back = NULL;
  size_t packed_n = encode(data, size, &packed);
  size_t back_n = decode(packed, packed_n, &back);
  assert(back_n == size && (size == 0 || memcmp(back, data, size) == 0));
  free(packed);
  free(back);
  return 0;
}

كتابة اختبارات كهذه، يعني فشلها أن قاعدة معلنة قد انكسرت، مفيدة اليوم مع أداة اختبار عشوائي عادية، وهي بالضبط ما يمكن لهذا النوع من الأدوات أن يحوّله لاحقًا إلى برهان. وتقول ⁨Theorem⁩ إنها تعرض تشغيل المسار نفسه لمشاريع مفتوحة المصدر أخرى، وتنشر مهارة لـ⁨Claude⁩ تساعد المطورين على البدء بالتحقق من كودهم.

الخطوة التالية: اختر محللًا أو مرمّزًا واحدًا في كودك، واكتب الخاصية التي يجب أن يحفظها دائمًا على شكل اختبار يفشل بوضوح. ثم اقرأ قسم الحدود في المقال الأصلي قبل أن تثق بأي وصف "متحقَّق منه رسميًا". المصدر: مقال فريق ⁨Frontier Red Team⁩ في ⁨Anthropic⁩ عن التحقق الرسمي بنماذج اللغة.