Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
تقدم هذه الورقة البحثية نظام "التركيب الاستقرائي الاستنباطي" (IDS)، وهو نظام لغوي كبير وكيل يقوم بتوليد التنفيذات والبراهين الصورية للأنظمة الموزعة بشكل مشترك، محققاً نسبة نجاح بلغت 100% في مواصفات مخازن القيم المفتاحية مع تقليل الوقت والتكلفة بشكل كبير مقارنة بكل من الخبراء البشريين ووكلاء البرمجة الأكثر تطوراً.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك تقوم ببناء نظام معقد وموزع مثل بنك رقمي أو دفتر ملاحظات مشترك يستخدمه الكثير من الناس في وقت واحد. أنت بحاجة للتأكد من أنه إذا كتب الشخص (أ) ملاحظة، فإن الشخص (ب) يراها فوراً، وأنه لا تضيع أي بيانات ولا تختلط ببعضها البعض، مهما كانت حالة الإنترنت فوضوية.
تقليدياً، هناك طريقتان لبناء ذلك:
- طريقة "التخمين والتحقق" (الذكاء الاصطناعي الحالي): تطلب من ذكاء اصطناعي ذكي كتابة الكود. يقوم بكتابته، ويجري بعض الاختبارات، ثم يقول: "يبدو جيداً!". لكن هذا يشبه فحص جسر عبر قيادة سيارة واحدة فوقه. قد يصمد أمام هذه السيارة، لكنه قد ينهار تحت تأثير شاحنة. إنه لا يضمن السلامة لكل السيناريوهات الممكنة.
- طريقة "البرهان الرياضي" (الخبراء التقليديون): توظف فريقاً من علماء الرياضيات والمهندسين البشر. هم لا يكتفون باختبار الكود فحسب؛ بل يكتبون برهاناً رياضياً رسمياً يثبت أن الكود لا يمكن أن يفشل، مهما حدث. هذا آمن للغاية، ولكنه يتطلب سنوات من الجهد البشري ويكلف ثروة طائلة.
المشكلة:
تقول الورقة البحثية إن حتى أذكى وكلاء الذكاء الاصطناعي الحاليين (مثل Codex أو Claude) يفشلون في طريقة "البرهان الرياضي". فهم يحاولون كتابة الكود أولاً، ثم يحاولون إثبات صحته لاحقاً. هذا يشبه محاولة بناء منزل ثم سؤال مهندس معماري لإثبات أنه لن ينهار بعد أن وُضعت الطوب بالفعل. هذا الأمر صعب للغاية، وهم يعلقون فيه.
الحل: التركيب الاستقرائي الاستنباطي (IDS)
ابتكر المؤلفون نظام ذكاء اصطناعي جديداً يسمى IDS (التركيب الاستقرائي الاستنباطي). فكر في IDS ليس كعامل واحد، بل كفريق من المهندسين المعماريين والمفتشين المتخصصين الذين يعملون في حلقة مترابطة.
إليك كيف يعمل، باستخدام تشبيه بسيط:
حلقة "البناء والتفتيش"
بدلاً من بناء المنزل بأكمله ثم فحصه، يقوم IDS ببناء جزء صغير جداً من المنزل ويتأكد فوراً مما إذا كان ذلك الجزء سليماً من الناحية الرياضية.
- الفريق الاستنباطي (البناؤون): يحاول هؤلاء الوكلاء من الذكاء الاصطناعي كتابة قطعة صغيرة من الكود (مثل إطار باب) وقطعة صغيرة من البرهان (جملة رياضية تقول "إطار هذا الباب قوي").
- المفتش (مساعد الإثبات): روبوت مفتش صارم ولا يغفل (يُسمى Rocq) يتحقق من العمل فوراً.
- إذا لم تكن الرياضيات دقيقة، يقول المفتش: "لا، إطار هذا الباب ضعيف"، ويتوقف الفريق فوراً. هم لا يضيعون الوقت في بناء بقية المنزل على أساس ضعيف.
- إذا اجتاز الفحص، ينتقلون إلى القطعة الصغيرة التالية.
- الفريق الاستقرائي (المخططون الاستراتيجيون): في بعض الأحيان، يتعثر البناؤون. يستمرون في محاولة بناء نفس نوع الباب، لكن الرياضيات لا تعمل أبداً. هنا يأتي دور الجزء "الاستقرائي".
- المقترح: ينظر ذكاء اصطناعي استراتيجي إلى نقطة التعثر ويقول: "مهلاً، ربما لا ينبغي لنا بناء باب خشبي؛ دعونا نجرب باباً فولاذياً". هو يقترح حلاً موضعياً جديداً.
- المعيد للتحميل (Reloader): إذا كانت الاستراتيجية بأكملها خاطئة (مثل محاولة بناء منزل على مستنقع)، يقول هذا الاستراتيجي: "تخلصوا من هذا التصميم. لنبدأ من جديد بمخطط مختلف تماماً".
لماذا يعد هذا أمراً هاماً
تدعي الورقة البحثية أن هذا النظام يغير قواعد اللعبة لثلاثة أسباب:
- السرعة: لقد حل 7 مشكلات معقدة لأنظمة موزعة في حوالي 6.8 ساعة. بينما كان فريق من الخبراء البشر سيستغرق شهوراً أو سنوات للقيام بنفس الشيء. هذا أسرع بنحو 200 مرة.
- معدل النجاح: استطاع أفضل وكلاء الذكاء الاصطناعي الحاليين حل مشكلتين فقط من أصل 7. أما IDS فقد حل السبع مشكلات جميعها.
- الأداء: ليس الكود صحيحاً فحسب، بل هو سريع أيضاً. في بعض الحالات، كان الكود الذي ولّده IDS يعمل أسرع بـ 3 مرات من أفضل النسخ التي كتبها البشر. حدث هذا لأن الذكاء الاصطناعي استكشف خيارات تصميم أكثر مما يستكشفه البشر عادةً، ليجد "النقطة المثالية" التي غفل عنها البشر.
العقبة (القيود)
الورقة البحثية صريحة جداً بشأن ما لا يستطيع IDS فعله حتى الآن:
- يحتاج إلى وصفة مثالية: لا يزال يتعين على خبير بشري كتابة "المواصفات" الأولية (القواعد الرياضية لما يجب أن يفعله النظام). إذا كانت الوصفة خاطئة، فسيقوم الذكاء الاصطناعي ببناء منزل مثالي لكنه لا يطابق ما أردته.
- ليس عصا سحرية لكل شيء بعد: لقد اختبروه خصيصاً على "مخازن المفتاح-القيمة" (نوع من قواعد البيانات). وبينما يعتقدون أنه يمكن أن يعمل على أشياء أخرى (مثل أنظمة التشغيل أو التشفير)، إلا أنهم لم يثبتوا ذلك بعد.
الخلاصة
تقدم هذه الورقة طريقة جديدة لاستخدام الذكاء الاصطناعي تجمع بين البناء والتحقق في آن واحد. بدلاً من سؤال الذكاء الاصطناعي "اكتب الكود وتمنى أن يعمل"، نطلب منه "اكتب الكود وأثبت أنه يعمل، خطوة بخطوة".
إنها تحول عملية إنشاء برمجيات "آمنة تماماً" من ماراثون بشري بطيء ومكلف إلى سباق سريع ومؤتمت، مما قد يجعل البرمجيات التي نعتمد عليها (مثل تطبيقات البنوك أو التخزين السحابي) أكثر أماناً وموثوقية بشكل كبير.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.