Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair

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

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

المحقق الذكي وصندوق الأدوات مفتوح المصدر

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

السر هنا يكمن في كيفية فحص الأخطاء. معظم أدوات الإصلاح المدعومة بالذكاء الاصطناعي تقوم فقط بتشغيل بعض تجارب القيادة (المحاكاة) لترى ما إذا كانت الشريحة تعمل. لكن هذا الفريق يستخدم "محرك خلفي رسمي" (Formal Backend) – وهو محرك رياضي مجاني مفتوح المصدر يتكون من أدوات تسمى Yosys وSymbiYosys وZ3. هذا المحرك لا يخمن فحسب؛ بل يحاول إثبات صحة الشريحة رياضياً. وإذا فشلت الشريحة، فإن المحرك لا يكتفي بالقول "إنها مكسورة"، بل يقدم للذكاء الاصطناعي "مثالاً مضاداً" (Counterexample) محدداً، وهو يشبه عرض فيديو يعيد اللقطات ليظهر بالضبط كيف انهار القصر. يشاهد الذكاء الاصطناعي هذا الفيديو، ويفهم ما الذي سار بشكل خاطئ، ثم يحاول إصلاح الأمر. ويستمرون في هذه العملية – فحص، اكتشاف الانهيار، إصلاح، ثم فحص مرة أخرى – حتى يثبت المنطق الرياضي أن الشريحة مثالية أو حتى تنفد محاولاتهم.

الأخبار الجيدة: إنها تعمل (أحياناً)

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

كان نجم العرض هو الـ ALU (وحدة الحساب والمنطق)، والتي تشبه عقل الآلة الحاسبة في الشريحة. تعمد الباحثون إتلافها عن طريق استبدال عملية "AND" بعملية "OR". اكتشف فريق الذكاء الاصطناعي الخطأ فوراً؛ ففي جولتين فقط من الفحص والإصلاح، تمكنوا من إصلاح الكود. والأهم من ذلك، أثبت المحرك الرياضي مفتوح المصدر بيقين بنسبة 100% أن الإصلاح كان صحيحاً لكل الأرقام الممكنة التي يمكن أن تعالجها الشريحة. حدث هذا في جميع جولات الاختبار الخمس، واستغرق في المتوسط 16.5 ثانية فقط. لقد أثبت ذلك أن الفكرة تنجح: يمكن للذكاء الاصطناعي، بتوجيه من أدوات رياضية مفتوحة المصدر، أن يجد ويصلح خطأً حقيقياً مع ضمان رياضي.

الأخبار السيئة: أين تعثر الذكاء الاصطناعي

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

1. فخ "العمق الزائد" (Bounded-Cover Vacuity): في إحدى الحالات (العداد/Counter)، قال المحرك الرياضي "فشل" رغم أن الإصلاح كان صحيحاً في الواقع. لماذا؟ لأن التصميم كان يحتاج للعمل لمدة 256 دورة للوصول إلى حالة معينة، لكن الأداة نظرت فقط لعمق 256 دورة. كان الأمر أشبه بمحاولة إثبات أن سيارة يمكنها عبور البلاد عبر قيادتها لميل واحد فقط؛ لم تستطع الأداة رؤية الوجهة، لذا استسلمت. تشير الورقة إلى أن هذا قصور في الأداة، وليس في الذكاء الاصطناعي.
2. فخ "التعليمات المربكة" (Specification Ambiguity): بالنسبة لتصميم آخر (المُحكّم/Arbiter)، حاول الذكاء الاصطناعي اتباع القواعد المكتوبة، لكن القواعد طلبت شيئاً مستحيلاً (مثل إشارة مرور تتغير دون وجود ساعة). اتبع الذككاء الاصطناعي التعليمات المستحيلة بأمانة، مما أدى إلى طريق مسدود.
3. فخ "السفر عبر الزمن" (Temporal Logic Bugs): في حالتين (جهاز إرسال UART وذاكرة FIFO)، تضمنت الأخطاء أحداثاً تحدث عبر خطوات زمنية متعددة. كان الذكاء الاصطناعي بارعاً في إصلاح المنطق أحادي الخطوة (مثل الآلة الحاسبة)، لكنه واجه صعوبة في الاستنتاج حول تسلسل الأحداث التي تحدث بمرور الوقت.
4. فخ "كثرة القواعد" (Multi-Property Pressure): في الحالة الأخيرة (AXI Lite slave)، كانت هناك قواعد كثيرة يجب أن تتبعها الشريحة في آن واحد، بحيث أن إصلاح قاعدة واحدة يؤدي لكسر قاعدة أخرى. علق الذكاء الاصطناعي في حلقة مفرغة، غير قادر على إيجاد حل يرضي الجميع.

خلل خفي في صندوق الأدوات

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

الخلاصة

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

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