Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification
تقترح هذه الورقة رسمًا بيانيًا للمعرفة (Knowledge Graph) متمحورًا حول التحقق، يدمج تمثيلات وسيطة مهيكلة من المواصفات، وRTL، وتغذية أدوات التحقق الرسمية الراجعة لتوجيه سير عمل متعدد الوكلاء، مما يحسن بشكل كبير من دقة الربط، وقابلية التجميع، والتغطية لـتأكيدات SystemVerilog المولدة بواسطة النماذج اللغوية الكبيرة (LLMs) لأغراض التحقق الرسمي.
البحث الأصلي مُهدى إلى الملك العام بموجب CC0 1.0 (http://creativecommons.org/publicdomain/zero/1.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تحاول بناء قلعة "ليجو" ضخمة ومعقدة للغاية بناءً على دليل تعليمات مكتوب. الدليل مكتوب بلغة إنجليزية بسيطة، لكن القلعة مبنية من آلاف القطع الصغيرة والمحددة (تصميم الأجهزة/العتاد).
المشكلة:
في عالم تصميم الرقائق الإلكترونية، يستخدم المهندسون "التحقق الرسمي" (Formal Verification) لإثبات أن القلعة لن تنهار رياضياً. وللقيام بذلك، يكتبون مجموعة من القواعد الصارمة تسمى "تأكيدات لغة سيستيم فيريلاغ" (SystemVerilog Assertions - SVAs). هذه القواعد تقول أشياء مثل: "إذا تم الضغط على الزر الأحمر، يجب أن يفتح الباب الأزرق خلال 3 ثوانٍ".
تقليدياً، كتابة هذه القواعد هي كابوس. فهي تتطلب من الإنسان قراءة الدليل الإنجليزي الفوضوي، والنظر إلى هيكل "الليجو" المعقد، ثم ترجمة ذلك إلى كود برمجي مثالي وخالٍ من الأخطاء. إذا كان الدليل غامضاً أو فات الإنسان تفصيل صغير حول قطعة معينة، فإن القاعدة ستفشل، وتنهار عملية التحقق بأكملها.
مؤخراً، تم استخدام الذكاء الاصطناعي (AI) لكتابة هذه القواعد تلقائياً. ولكن الذكاء الاصطناعي غالباً ما يصاب بالارتباك؛ فهو يقرأ الدليل ولكنه لا "يرى" قطع "الليجو"، مما يؤدي إلى قواعد خاطئة برمجياً أو لا معنى لها بالنسبة للتصميم الفعلي.
الحل: "أمين مكتبة رقمي" (الرسم البياني للمعرفة - Knowledge Graph)
تقترح هذه الورقة طريقة جديدة لمساعدة الذكاء الاصطناعي. بدلاً من ترك الذكاء الاصطناعي يقرأ الدليل ويخمن فقط، قام المؤلفون ببناء "رسم بياني للمعرفة" (Knowledge Graph).
فكر في الرسم البياني للمعرفة كـ أمين مكتبة رقمي فائق التنظيم يربط بين ثلاثة أشياء:
- التعليمات: المتطلبات الأصلية باللغة الإنجليزية.
- المخطط الهيكلي: تصميم الأجهزة الفعلي (قطع الليجو).
- التغذية الراجعة: نتائج أدوات التحقق (على سبيل المثال: "فشلت هذه القاعدة لأن الباب لم يفتح بالسرعة المطلوبة").
أمين المكتبة لا يخزن هذه الأشياء كمجرد أكوام منفصلة من الأوراق؛ بل ينشئ شبكة من الروابط. إذا سألت أمين المكتبة عن قاعدة معينة، فسيستخرج لك فوراً الجملة المحددة من الدليل، والقطعة المحددة التي تشير إليها، وأي أخطاء سابقة حدثت مع قواعد مشابهة.
كيف يعمل الفريق (سير عمل الوكلاء المتعددين - Multi-Agent Workflow)
لم يكتفِ المؤلفون ببناء أمين المكتبة فحسب، بل وظفوا فريقاً من "الوكلاء" المتخصصين في الذكاء الاصطناعي للعمل معه. تخيل طاقم بناء لكل فرد فيه وظيفة محددة:
- المهندس المعماري (توليد الخصائص): ينظر هذا الوكيل إلى الدليل والروابط الموجودة في "أمين المكتبة" لكتابة القواعد الأولية. ولأن أمين المكتبة يوفر السياق الدقيق، فمن المرجح جداً أن تكون القواعد صحيحة منذ البداية.
- شرطة القواعد (تصحيح الصيغة البرمجية): إذا احتوت القواعد على أخطاء مطبعية أو أخطاء برمجية، يقوم هذا الوكيل بإصلاحها. وهو يستخدم "أمين المكتبة" للتحقق مما إذا كانت "القطعة المفقودة" هي في الواقع نقص في التعريف داخل الكود.
- المحقق (تصحيح CEX): أحياناً تفشل القاعدة لأن التصميم نفسه معطل، أو لأن القاعدة كانت صارمة للغاية. ينظر هذا الوكيل إلى "مسرح الجريمة" (تقرير الخطأ)، ويفحص المخطط الهيكلي، ويعيد كتابة القاعدة لتكون أكثر إنصافاً أو لإصلاح سوء الفهم.
- المفتش (تحسين التغطية): يتحقق هذا الوكيل مما إذا كانت هناك أجزاء من القلعة لم يتم اختبارها بعد. وإذا وجد ذلك، فإنه يطلب من "أمين المكتبة" قواعد جديدة لاختبار تلك المناطق المحددة.
النتائج
اختبر الفريق هذا النظام على سبع "قلاع" مختلفة (تصاميم رقائق)، تتراوح من العدادات البسيطة إلى أنظمة الذاال المعقدة.
- النجاح: أنتج النظام باستمرار قواعد يمكن للكمبيوتر قراءتها وتشغيلها بالفعل (كود قابل للتجميع/Compilable code). وقد قلل بشكل كبير من عدد "الأخطاء المطبعية" والأخطاء الأساسية.
- التغطية: تمكن النظام من التحقق من ما بين 78.5% و99.4% من سلوك التصميم، وهي نسبة نجاح عالية جداً.
- الحدود: بينما يتفوق النظام في إصلاح الأخطاء الصغيرة وربط النقاط ببعضها، إلا أنه لا يزال يعاني مع الألغاز الأكثر صعوبة. إذا كانت القاعدة تتطلب منطقاً معقداً وطويل الأمد (مثل: "إذا حدث هذا اليوم، فيجب أن يؤثر على ذلك الحدث بعد ثلاثة أيام من الآن")، فقد يتعثر الذكاء الاصطناعي أحياناً، حتى مع مساعدة أمين المكتبة.
باخت-صار
تقدم هذه الورقة نظاماً لا يقوم فيه الذكاء الاصطناعي بمجرد التخمين حول كيفية التحقق من الرقائق الإلكترونية. بدلاً من ذلك، يستخدم خريطة مهيكلة (الرسم البياني للمعرفة) لربط المتطلبات المكتوبة مباشرة بتصميم الأجهزة ونتائج الاختبار. وهذا يسمح لفريق من متخصصي الذكاء الاصطناعي بكتابة وتصحيح وتحسين قواعد التحقق بشكل أكثر موثوقية من ذي قبل، محولين عملية التخمين الفوضوية إلى عملية منظمة وقابلة للتتبع.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.