LLM2SMT: Building an SMT Solver with Zero Human-Written Code
تقدم هذه الورقة LLM2SMT، وهي دراسة حالة تثبت أن وكيل برمجة يعتمد على نموذج لغوي كبير (LLM) يمكنه بناء حل SMT كامل وتنافسي من طراز DPLL(T) لـ QF_UF بشكل مستقل — بما في ذلك خوارزمية Nieuwenhuis-Oliveras للإغلاق التطابقي وانبعاث براهين Lean — دون أي كود مكتوب بشرياً.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك المدير التنفيذي لشركة برمجيات. بدلاً من توظيف فريق من المهندسين لبناء منتج جديد من الصفر، قمت بتوظيف متدرب ذكاء اصطناعي واحد، موهوب للغاية، ولكنه غريب الأطوار قليلاً.
هدفك؟ بناء محقق منطقي (يُسمى SMT Solver). مهمة هذا المحقق هي النظر في مجموعة معقدة من القواعد والقرائن للإجابة على سؤال بسيط واحد: "هل من الممكن أن تكون كل هذه القرائن صحيحة في نفس الوقت، أم أن هناك تناقضاً؟"
إليك الحبكة: أنت، الإنسان، لم تكتب سطراً واحداً من الكود. لم تكتب أي جملة شرطية if أو حلقة تكرارية for. لقد أعطيت المتدرب (الذكاء الاصطناعي) مجموعة من التعليمات فقط، وهو قام ببناء وكالة التحقيق بأكملاء، ونظام الأرشفة، ومحرك الاستنتاج بنفسه.
المهمة: بناء آلة منطقية
أراد الباحثون (Mikoláš Janota و Mirek Olšák) معرفة ما إذا كان بإمكان الذكاء الاصطناعي بناء أداة تقوم بالاستنتاج المنطقي. أعطوا متدربهم (الذكاء الاصطناعي) مهمة: "ابنِ محققاً منطقياً يمكنه حل الألغاز التي تتضمن الدوال غير المفسرة (Uninterpreted Functions) - وهي طريقة فنية لوصف 'صناديق غامضة' نعرف قواعد التساوي الخاصة بها ولكن لا نعرف محتوياتها المحددة".
أخبروه بـ:
- المخطط التوجيهي: "استخدم خوارزمية محددة تسمى 'Congruence Closure' (فكر فيها كوسيلة لتجميع العناصر المتطابقة معاً)".
- الأدوات: "استخدم هذه المكتبة المحددة للقيام بالمهام الشاقة (CaDiCaL) وهذه اللغة لكتابة التقرير النهائي (Lean)".
- اللغة: "تحدث بلغة ++C20".
الرحلة: من الفوضى إلى الكفاءة
1. البداية "الساذجة"
في البداية، حاول الذكاء الاصطناعي بناء المحقق، لكنه ارتكب خطأ المبتدئين الكلاسيكي. فقد بنى محققاً يمكنه فقط النظر في قرائن فردية، لكنه لا يستطيع فهم كيفية ترابط القرائن (مثل "و" أو "أو"). كان الأمر أشبه بتوظيف محقق يمكنه قراءة بصمة إصبع، لكنه لا يفهم مفهوم مسرح الجريمة.
- الإصلاح: قام الباحثون ببساطة بالإشارة إلى الجزء المفقود. أدرك الذكاء الاصطناعي: "أوه، صحيح! المنطق يحتاج إلى روابط!" وأعاد كتابة الكود.
2. مصلح الأخطاء "التعلم الذاتي"
بينما بدأ المحقق في العمل، ارتكب بعض الأخطاء. أحياناً كان يقول إن اللغز مستحيل بينما كان له حل في الواقع.
- اللمسة البشرية: بدلاً من إصلاح الكود بأنفسهم، أعطى الباحثون للذكاء الاصطناعي أداة "fuzzing" (الاختبار العشوائي). تخيل آلة تلقي بآلاف الألغاز الغريبة والعشوائية على المحقق. عندما يخطئ المحقق في أحدها، يقوم الذكاء الاصطناعي بتحليل الفشل، وفهم الخطأ، وإصلاحه من تلقاء نفسه.
- التشبيه: الأمر يشبه طالباً يجري اختباراً تجريبياً، ويخطئ في سؤال ما، ثم يقرأ الشرح، ويقوم فوراً بتعديل ملاحظاته الدراسية دون الحاجة لأن يعيد المعلم شرح الفصل بأكمله.
3. مشكلة "الماسة" (اللغز المعقد)
كان هناك نوع محدد من الألغاز يسمى "Equational Diamond". تخيل متاهة حيث يوجد مساران يبدوان مختلفين ولكنهما يؤديان إلى نفس المكان. المحقق التقليدي سيحاول السير في كل مسار، مما يستغرق وقتاً طويلاً جداً (وقتاً أسياً).
- الاختراق: أعطى الباحثون للذكاء الاصطناعي تلميحاً: "ابحث عن طرق مختصرة قبل أن تبدأ في المشي". اخترع الذكاء الاصطناዊ تقنية "المعالجة المسبقة" (Preprocessing). نظر إلى المتاهة، وأدرك الطرق المختصرة، ودمج المتاهة بأكملها في خط مستقيم واحد. فجأة، الألغاز التي كانت تستغرق ساعات أصبحت تُحل في أجزاء من الثانية.
4. "قاعة المحكمة" (الاعتماد/التوثيق)
الجزء الأكثر إثارة للإعجاب؟ لم يكتفِ الذكاء الاصطناعي بحل الألغاز فحسب؛ بل كان عليه أيضاً إثبات أنه حلها بشكل صحيح باستخدام لغة تسمى Lean (وهي لغة يستخدمها الرياضيون للتحقق من البراهن).
- التحدي: كان على الذكال الاصطناعي ترجمة منطقه الداخلي إلى حجة قانونية رسمية يقبلها "القاضي" (مدقق البراهن في Lean).
- الصراع: كان الذكاء الاصطناعي يحاول باستمرار تقديم حجج معقدة للغاية أمام القاضي. اضطر الباحثون لتعليمه: "لا تكتب رواية؛ فقط اكتب النقاط الرئيسية". بمجرد أن أعطوه نموذجاً لبراهن مثالي، تعلم الذكاء الاصطناعي كتابة مذكراته القانونية الخاصة بشكل مثالي.
النتائج: ما مدى جودة محقق الذكاء الاصطناعي؟
اختبر الباحثون محقق الذكاء الاصطناعي مقابل أفضل المحققين البشريين (Z3 و cvc5).
- النتيجة: حل محقق الذكاء الاصطناعي 7,468 لغزاً من أصل 7,500 لغز.
- المقارنة: كان قريباً جداً من مستوى أبطال البشر، حيث حل عدداً مماثلاً تقريباً من المشكلات.
- العائق: كان أبطأ قليلاً في بعض الألغاز لأنه لم يمتلك "الغرائز" (التحسينات) التي يقضي المهندسون البشريون عقوداً في صقلها. ولكن بالنسبة لآلة كتبت الكود الخاص بها من الصفر؟ هذا يعتبر نجاحاً باهراً.
الدروس الكبرى (الخلاصة)
- الذكاء الاصطناعي قوي ولكنه "متعرج": الذكاء الاصطناعي بارع في المهام المعقدة ولكنه قد يفشل في أشياء بسيطة وسخيفة (مثل نسيان أن
x = xهي دائماً حقيقة). إنه مثل عبقري يمكنه كتابة سيمفونية ولكنه ينسى ربط حذائه. - أنت بحاجة إلى شبكة أمان: لا يمكنك ترك الذكاء الاصطناعي يعمل دون رقابة. أنت بحاجة إلى حدود "وقت انتهاء الصلاحية" (حتى لا يعلق في حلقة مفرغة للأبد) و"الاختبار العشوائي" (fuzzing) للإمساك بالأخطاء.
- المستقبل هو عمل تعاوني: لم يستبدل الذكاء الاصطناعي الإنسان؛ بل أصبح الإنسان هو المهندس والمعلم. وضع الإنسان القواعد، وقدم الأمثلة، وبنى شبكات الأمان، بينما قام الذكاء الاصطناعي بالعمل الشاق المتمثل في كتابة الكود.
باختصار: تثبت هذه الورقة البحثية أنه مع التوجيه الصحيح، يمكن للذكاء الاصطناعي بناء أداة استنتاج متطورة من الصفر، ليعمل فعلياً كـ "مهندس برمجيات يكتب نفسه بنفسه". إنه ليس مثالياً بعد، ولكنه يمثل قفزة هائلة فيما يمكن للآلات أن تبدعه لنفسها.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.