💻 computer science

Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?

تُثبت هذه الورقة أن نهجاً عصبياً رمزياً يجمع بين النماذج اللغوية الكبيرة والأدوات الرمزية الصورية يمكنه بنجاح توليد براهين استقرائية صحيحة برهانياً للتحقق من العتاد، محققاً معدل نجاح بنسبة 84% على تصميمات RTL مفتوحة المصدر متوسطة الحجم.

المؤلفون الأصليون: Romy Peled, Daniel Kroening, Michael Tautschnig, Yakir Vizel

نُشر 2026-05-04

📖 4 دقيقة قراءة☕ قراءة في استراحة قهوة

CC BY 4.0

المؤلفون الأصليون: Romy Peled, Daniel Kroening, Michael Tautschnig, Yakir Vizel

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

تخيل أنك تحاول إثبات أن آلة معقدة (مثل دائرة رقمية في شريحة كمبيوتر) لن تقوم أبدًا بشيء خطير، مثل الانهيار أو تسريب البيانات. في عالم هندسة الأجهزة، يُسمى هذا التحقق الرسمي (Formal Verification).

عادةً، يتطلب إثبات ذلك وجود خبير بشري يكتب "درعًا رياضيًا" (يُسمى المتغير الاستقرائي - inductive invariant) يغطي كل حالة ممكنة يمكن أن تكون فيها الآلة. الأمر يشبه محاولة كتابة كتاب قواعد يغطي كل حركة يمكن أن يقوم بها لاعب الشطرنج، وإلى الأبد. وهذا أمر صعب للغاية، ويستغرق وقتًا طويلاً، وغالبًا ما يتطلب من الإنسان ابتكار "قواعد مساعدة" (lemmas) ذكية لجعل الإثبات ناجحًا.

هذه الورقة البحثية تطرح سؤالًا بسيطًا: هل يمكن للذكاء الاصطناعي (وتحديدًا النماذج اللغوية الكبيرة أو LLM) أن يعمل كـ "آلة تعدين" لإيجاد هذه القواعد المساعدة لنا؟

إليك تفصيل نهجهم، باستخدام تشبيهات من الحياة اليومية:

١. المشكلة: جدار "مستوى البت" (Bit-Level)

أدوات الكمبيوتر الحالية تشبه محاسبين مجتهدين ولكن ضيقي الأفق. إنهم يفحصون كل بت من البيانات (الأصفار والآحاد) واحدًا تلو الآخر. إذا كانت الآلة ضخمة، يصاب المحاسب بالإرهاق ويستسلم.
أما الخبراء البشر، فيفكرون في "مفاهيم عالية المستوى". هم لا يعدون كل حبة رمل؛ بل يرون شكل الشاطئ. أراد المؤلفون معرفة ما إذا كان بإمكان الذكاء الاصطناعي تعلم التفكير مثل الخبير البشري وتوليد تلك القواعد المساعدة عالية المستوى.

٢. الحل: فريق "نيوروسيمبوليك" (Neurosymbolic)

لم يكتفِ المؤلفون بسؤال الذكاء الاصطناعي عن "تخمين" الإجابة، بل بنوا فريقًا يتكون من دورين متميزين، مثل الكاتب المبدع والمحرر الصارم.

الكاتب المبدع (النموذج اللغوي الكبير - LLM): هذا هو الذكاء الاصطناعي. مهمته هي العصف الذهني. ينظر إلى تصميم الجهاز وقاعدة السلامة، ثم يخرج قائمة بالقواعد المساعدة المحتملة (lemmas).
- العائق: الذكاء الاصطناعي مبدع ولكنه غير موثوق. أحيانًا يكتب قواعد عبقرية؛ وأحيانًا أخرى يكتب هراءً، أو قواعد لا معنى لها، أو قواعد خاطئة رياضيًا. إنه "يهلوس".
المحرر الصارم (الأداة الرسمية - Formal Tool): هذا برنامج كمبيوتر تقليدي وصارم. لا يهتم بالإبداع؛ بل يهتم فقط بالحقيقة. يأخذ قائمة القواعد التي أنتجها الذكاء الاصطناعي ويفحصها بصرامة. إذا كانت القاعدة خاطئة ولو بشكل طفيف، يرفضها المحرر. وإذا كانت القاعدة تعمل، يحتفظ بها المحرر.

٣. الاستراتيجيتان

جرب الفريق طريقتين مختلفتين لتنظيم العلاقة بين الكاتب والمحرر:

الاستراتيجية (أ): نهج "الدفعات" (غير الوكيل - Non-Agentic)
تخيل أنك تطلب من الذكاء الاصطناعي: "أعطني ٥٠ فكرة لقاعدة مساعدة"، دفعة واحدة. يكتب الذكاء الاصطنا٠ مسودات لـ ٥٠ قاعدة. ثم يقوم المحرر بالمرور على المجموعة، مستبعدًا السيئ منها ومحتفظًا بالجيد ليرى ما إذا كانت ستحل المشكلة.
الاستراتيجية (ب): نهج "المحادثة" (الوكيل - Agentic)
هذا يشبه الحوار الحقيقي أكثر. يقترح الذكاء الاصطناعي قاعدة. يفحصها المحرر ويقول: "لا، هذه القاعدة خاطئة بسبب (س)". يقرأ الذكاء الاصطناعي التعليقات، ويتعلم من خطئه، ثم يحاول مرة أخرى. يستمرون في هذه الحلقة من الذهاب والإياب حتى يجدوا قاعدة تعمل. وجدت الورقة أن أسلوب "المحادثة" هذا كان أكثر كفاءة في كثير من الأحيان.

٤. النتائج: التعدين عن الذهب

اختبر الفريق هذا النظام على ١١٠ تصميمات مختلفة للأجهزة (تتراوح من العدادات البسيطة إلى أنظمة الذاكرة المعقدة).

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

٥. ماذا يعني هذا (وما لا يعنيه)

ما يفعله: إنه يؤتمت عملية "تعدين" القواعد المساعدة. إنه يرفع عن كاهل المهندسين البشريين عبء القيام بعمليات العصف الذهني للقواعد الرياضية (lemmas).
ما لا يفعله: إنه لا يستبدل المهندس البشري تمامًا. فلا يزال يتعين على الإنسان إعداد النظام وتفسير النتائج. كما أن النظام حاليًا يحتاج إلى كود الجهاز بتنسيق محدد (SystemVerilog)؛ ولا يمكنه العمل على "المخططات الخام" (netlists) التي تستخدمها بعض الأدوات القديمة.

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

إليك ملخص تقني مفصل لورقة البحث بعنوان "عمال مناجم الليما الضخام: هل يمكن للنماذج اللغوية الكبيرة (LLMs) إجراء استنتاجات استقرائية للأجهزة؟"

1. بيان المشكلة

تعد التحقق الصوري (Formal Verification - FV) أمراً بالغ الأهمية لضمان صحة تصميمات الأجهزة (RTL). ومع ذلك، لا يزال التحقق من التصميمات الصناعية المعقدة يشكل عائقاً بسبب الطبيعة "على مستوى البت" (bit-level) لمعظم أدوات فحص النماذج. تواجه هذه الأدوات صعوبة في بناء براهين رياضية عالية المستوى وغير مرتبطة بالبتات (bit-agnostic) مطلوبة للخصائص المعقدة.

النهج القياسي لحل هذه المشكلة هو الاستدلال بالاستقراء (Proof by Induction)، والذي يتطلب ليماوات مساعدة (auxiliary lemmas) (تعزيزات استقرائية) لإثبات خاصية ما. حالياً، يعد توليد هذه الليماوات مهمة يدوية شاقة يقوم بها مهندسو التحقق الصوري الخبراء. تعالج ورقة البحث السؤال التالي: هل يمكن للنماذج اللغوية الكبيرة (LLMs) أتمتة عملية تنقيب الليماوات المساعدة لبناء حجج استقرائية صالحة للتحقق من الأجهزة؟

2. المنهجية: نهج عصبي رمزي (Neurosymbolic Approach)

يقترح المؤلفون إطار عمل عصبي رمزي يجمع بين القدرات التوليدية للنماذج اللغوية الكبيرة ودقة الأدوات الرمزية الصورية. لا يعتمد النظام فقط على مخرجات النموذج اللغوي الكبير؛ بل يستخدم النموذج لتوليد مرشحات ويستخدم أداة صورية للتحقق والتصفية.

أ. المكونات الأساسية

أطر عمل التلقين (Prompting Frameworks): تُستخدم استراتيجيتان متميزتان لتوليد الليماوات المرشحة:
- غير الوكيل (Single Prompt): يستخدم تلقيناً بنظام "التعلم من أمثلة قليلة" (Few-Shot) يحتوي على $k$ من الثلاثيات المكونة من (تصميم RTL، الخاصية، الليماوات الاستقرائية). يتم اختيار الأمثلة عبر التشابه الدلالي (باستخدام محولات الجمل - sentence transformers) من مجموعة "سلسلة الأفكار" (CoT) المُعدة مسبقاً. يتم أخذ عينات من النموذج اللغسي $n$ من المرات باستخدام نفس التلقين لجمع مرشحات متنوعة.
- الوكيل (Iterative Interaction): يؤطر توليد الليماوات كحلقة تكرارية. يقترح النموذج اللغوي الليماوات، والتي يتم فحصها بواسطة الأداة الصورية. إذا فشل الفحص، توفر الأداة تغذية راجعة (توضح أي الليماوات فشلت ولماذا) ورسالة "إصلاح". ثم يقوم النموذج اللغسي بتنقيح اقتراحاته في جولات لاحقة (حتى 5 تكرارات).
خوارزمية الاستدلال الصوري (FINDINDSTRENGTH):
- تأخذ هذه الخوارزمية مجموعة الليماوات المرشحة التي ولدها النموذج اللغسي وتحاول إيجاد مجموعة فرعية تشكل تعزيزاً استقرائياً (Inductive Strengthening) صالحاً.
- التعزيز الاستقرائي: مجموعة من الليماوات $L$ بحيث يكون $L \land \text{Property}$ ثابتاً استقرائياً (يحقق التأسيس والتبعية/consecution).
- العملية:
  1. التصفية (Filtering): تتحقق مما إذا كانت الليماوات الفردية هي ثوابت استقرائية (باستخدام الاستقراء أحادي المستوى - 1-induction) أو إذا كانت صالحة حتى عمق محدد (باستخدام فحص النموذج المقيد - BMC).
  2. الترتيب (Sorting): تعطي الأولوية لليماوات المعروفة بأنها ثوابت استقرائية على تلك التي تصمد فقط ضمن حد معين.
  3. البحث عن المجموعات الفرعية (Subset Search): تمر عبر مقدمات القائمة المرتبة للعثور على أصغر مجموعة فرعية تشكل، عند دمجها مع الخاصية المستهدفة، ثابتاً استقرائياً صالحاً.
- الأدوات: تم التنفيذ باستخدام EBMC (أداة تحقق صوري) مع $k$ -induction و BMC.

ب. مجموعة البيانات

تم تقييم إطار العمل على 110 مهمة تحقق تتكون من:

58 تصميماً بلغة SystemVerilog (من مصادر مثل VCEGAR، VIS، v2c، وتصميمات مخصصة لـ FIFO/Arbiter/CAM).
47 مثالاً مشتقاً من برامج C: أكواد C تمت ترجمتها إلى آلات حالة محدودة (FSMs) بلغة SystemVerilog لاختبار التعميم.
مجموعة سلسلة الأفكة (CoT Pool): مجموعة صغيرة من الأمثلة المكتوبة يدوياً لاستخدامها في تلقين "التعلم من أمثلة قليلة".

3. المساهمات الرئيسية

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

4. النتائج التجريبية

أجريت التجارب على مثيلات Amazon EC2 باستخدام ستة من أحدث النماذج اللغوية الكبيرة (GPT-5، Claude 3.7، Claude 4 Sonnet، Claude 4.5 Sonnet، Claude 4.5 Haiku، Claude 4.5 Opus).

معدل النجاح: نجح إطار العمل في توليد حجج استقرائية صحيحة لـ 84% من مهام التحقق الـ 110.
- الإعداد الوكيلي (Agentic): حل 92/110 مثالاً (معدل نجاح 84%).
- الإعداد غير الوكيلي (Non-Agentic): حل 84/110 مثالاً (معدل نجاح 76%).
أداء النماذج: حقق Claude 4.5-Opus أفضل أداء، حيث حل 88 مثالاً في الإعداد الوكيلي.
المقارنة مع أدوات SOTA (أحدث ما توصل إليه العلم):
- حدد المؤلفون 31 معياراً "تحدياً" حيث فشلت أدوات الصناعة المتطورة (مثل JasperGold، VC-Formal، rIC3) في إثبات الخاصية خلال مهلة 10 دقائق.
- حل النهج القائم على النماذج اللغوية الكبيرة الحالات التي لم تستطع فيها هذه الأدوات (SOTA) الحل، خاصة في الحالات التي تتطلب تعزيزات استقرائية معقدة (مثل تصميمات FIFO و Arbiter المحددة).
- في بعض الحالات التي وجدت فيها النماذج اللغوية الليما الصحيح ولكن فشل الفحص الصوري بسبب انتهاء الوقت (timeout)، اعتبرت النتيجة ناجحة من حيث توليد الليما، لأن العائق كان وقت تشغيل أداة التحقق وليس منطق النموذج اللغسي.
تحليل الخطأ:
- هلوست النماذج اللغية أحياناً في قواعد (syntax) لغة SVA (مثل معاملات غير صالحة، متغيرات غير معرفة) أو استخدمت رموزاً غير ASCII.
- كان الإعداد الوكيلي أكثر كفاءة، حيث وجد الحلول غالباً بعدد أقل من الليماوات الإجمالية من خلال تنقيح مساحة البحث بشكل تكراري.

5. الأهمية والأثر

القيمة الصناعية: يمكن لهذا النهج أن يقلل بشكل كبير من الجهد اليدوي المطلوب من مهندسي التحقق الصوري. من خلال أتمتة اكتشاف الليماوات المساعدة، فإنه يخفض الحاجز أمام تطبيق الأساليب الصورية على تصميمات الأجهزة المعقدة.
ما وراء الحفظ: تشير النتائج إلى أن النماذج اللغوية الكبيرة تقوم بعملية استدلال حقيقية بدلاً من مجرد الحفظ، حيث نجحت في التعميم على الأمثلة المشتقة من لغة C وتعاملت مع الاختلافات في تخصيص المعاملات (parameter instantiation) وتسمية السجلات (register naming).
الاتجاهات المستقبلية: يخطط المؤلفون لتوسيع إطار العمل للتعامل مع خصائص متعددة في آن واحد، وتوسيع النطاق ليشمل تصميمات صناعية أكبر، والتحقق من النهج في بيئة صناعية واقعية.

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