LLM2Cert يتحقق من 81 شهادة من أصل 105 لضمان الاستقرار والأمان

تعلّمت النماذج اللغوية كتابة الشيفرة وإثبات المبرهنات. والآن يجري اختبارها في مهمة هندسية يكلّف الخطأ فيها كثيرًا: التأكد من أن نظامًا ديناميكيًا يبقى مستقرًا وآمنًا. بنى مؤلفو الورقة البحثية LLM2Cert (arXiv 2610.30524) إطارًا يقترح فيه LLM الشهادات، بينما تتحقق منها أدوات تحقق رسمية. وعلى معيار DynaCertBench الجديد الذي يضم 105 مهام، يتحقق النظام من 81 مهمة، أي 77,1%. وهذا أفضل بـ 17,1 نقطة مئوية من التوليد من محاولة واحدة دون تغذية راجعة (نحو 60%).

لماذا تظل الشهادات حتى الآن عنق الزجاجة؟

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

تفحص خطوط المعالجة الحالية المرشحين بثلاث طرق: الحلّالات العددية (برامج sum-of-squares)، والطرق الفترية، وحلّالات SMT. وتشترك الطرق الثلاث في مجموعة مشكلات. فهي تحتاج إلى تخفيفات (relaxations)، وتتسم بالتحفظ، أو لا تتوسع جيدًا مع ازدياد أبعاد النموذج ودرجة لاخطيته.

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

DynaCertBench وتوجيه الالتزامات

يتعلق الجزء الأول من العمل بمجموعة الاختبار. يضم DynaCertBench ‏105 مهام:

• 80 نظامًا غير مكرَّر، مختارة من الأدبيات العلمية؛
• توسيعات لهذه الأنظمة بصيغ متعددة الأبعاد وصيغ بقيود على التحكم؛
• أنظمة جديدة مترابطة بشكل غير خطي؛
• أربع فئات من المهام: الاستقرار، ومنطقة الجذب (region of attraction)، والثبات الأمامي (forward invariance)، والأمان.

أما الجزء الثاني فهو LLM2Cert نفسه. يولّد النموذج مرشحًا للشهادة، ثم يفكّكه الإطار إلى التزامات إثباتية. ويُوجَّه كل التزام عبر أحد مسارين: إلى حلّال SMT، أو مباشرة إلى وكيل Lean Proof-Repair. يعمل Lean هنا كمدقق رسمي صارم، بينما يصلح الوكيل الإثبات إذا لم يتقارب. والتغذية الراجعة من أدوات التحقق هي التي تحقق المكسب الأساسي: فمن دونها يحلّ النموذج الذي يقدّم مرشحًا واحدًا عددًا أقل بوضوح من المهام.

الأرقام التي يجدر تذكّرها

• DynaCertBench: ‏105 مهام، منها 80 من الأدبيات العلمية.
• يتحقق LLM2Cert من 81 مهمة من أصل 105، أي 77,1%.
• الفارق عن اقتراح one-shot دون تغذية راجعة: 17,1 نقطة مئوية.
• من بين 81 شهادة جرى العثور عليها، جرى التحقق من 22 شهادة في حالات يترك فيها نهج All-SMT، الذي يرسل كل شيء إلى حلّال SMT، المسألة مفتوحة.

ولعل الرقم الأخير هو الأكثر دلالة. فهو يمثل نحو ربع الشهادات في المجموعة التي لا يصل إليها SMT الخالص. ويحلّ التوجيه الهجين جزءًا من المهام التي يعجز SMT عن حلها بمفرده.

أعدّ الورقة Zhipeng Cao وPeiyang Song وNikolaus Vertovec وWeiru Cui وZhihao Yang وMingkang Liu وLuxia Lin وBai Xue وAlessandro Abate. والشيفرة والبيانات منشورتان في المستودع FormalCert-AI/llm2cert.

من سيستفيد أولًا؟

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

وبالنسبة إلى الباحثين، يفيد DynaCertBench نفسه: إذ يمكن عليه مقارنة طرق التوليف الجديدة على مهام أقرب إلى الأنظمة الواقعية من كثيرات الحدود منخفضة الأبعاد المعتادة. ويتيح الكود المفتوح إعادة إنتاج النتائج وتوصيل نموذج آخر. وتبقى 24 مهمة من أصل 105 لم يتمكن LLM2Cert من حلها، وهي تُظهر موضع حدود الطريقة.