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

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

المشكلة: فخ "اكتب ثم تحقق"

تعالج الورقة البحثية، التي تحمل عنوان "التخطيط المشترك للبرنامج والإثبات لتوليد الكود الموثق" (Joint Program-and-Proof Planning for Verified Code Generation)، عقبة محبطة في كيفية كتابة الذكاء الاصطناعي للبرمجيات الموثقة. حالياً، تتبع معظم الأنظمة سير عمل "البرنامج ثم الإثبات". الأمر يشبه طلب من طاهٍ إعداد وجبة معقدة، ثم بعد تقديم الطعام على الطاولة، سؤال ناقد طعام عما إذا كانت المكونات طازجة وطريقة الطهي آمنة. إذا وجد الناقد مشكلة (مثل دجاج غير مطهو جيداً)، يتعين على الطاهي العودة وإعادة طهي الطبق، والأمل في أن ينال إعجاب الناقد هذه المرة.

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

الحل: P3 (المخطط "يداً بيد")

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

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

1. كيف سيعمل الكود؟ (مسودة البرنامج - Program Sketch)
2. كيف سنثبت أنه يعمل؟ (مسودة الإثبات - Proof Sketch)

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

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

ميدان الاختبار الجديد: Lean4Commit0

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

قاموا بجمع بيانات من 108 مكتبة برمجية مفتوحة المصدر (مكتوبة بلغات Python و Rust و C/C++ و Java) وحولوا ميزاتها الأساسية إلى تحديات "كود موثق". بدلاً من مهام بسيطة مثل "جمع رقمين"، تتضمن هذه التحديات علاقات معقدة بين أجزاء مختلفة من البرنامج. على سبيل المثال، في نظام إعدادات، قد يطلبون من الذكاء الاصطناعي إثبات أنه "إذا قمت بضبط إعداد على 'مرتفع' ثم قمت لاحقاً بضبطه على 'منخفض'، فإن النظام يتذكر الإعداد 'المنخفض' بشكل صحيح". تتطلب هذه المهام من الذكاء الاصطناعي فهم كيفية تواصل الوظائف المختلفة مع بعضها البعض، مما يجعلها أصعب بكثير من المسائل المدرسية.

ماذا وجدوا: التخطيط المشترك يفوز

اختبر الفريق P3 مقابل أربعة من أقوى نماذج الذكاء الاصطناعي المتاحة (بما في ذلك نسخ من Codex و Gemini و Claude) عبر ثلاثة معايير مختلفة: Verina و AlgoVeri و معيارهم الجديد Lean4Commit0.

كانت النتائج واضحة: التخطيط معاً يعمل بشكل أفضل من الكتابة بشكل منفصل.

• معدل النجاح: حل P3 مهام أكثر من أي طريقة أخرى في كل اختبار. وفي المهام الأكثر صعوبة، رفع معدل النجاح بنسبة تترا_وح بين 4.6 إلى 11.2 نقطة مئوية مقارنة بأفضل الطرق الموجودة.
• الكفاءة: لم يكن الأمر يتعلق فقط بحل المزيد من المشكلات، بل بحلها بشكل أسرع وأرخص. في المهام الصعبة، قلل P3 من تكلفة استدعاءات الواجهة البرمجية (API calls) بنسبة تصل إلى 40% وقلل الوقت المستغرق بنسبة تصل إلى 37%. وذلك لأن الذكاء الاصطناعي لم يضع وقته في محاولة إثبات أشياء مستحيلة أو إعادة كتابة كود خاطئ بنيوياً.
• ميزة "العمل المشترك": لإثبات أن "التخطيط المشترك" كان هو السر، أجروا اختباراً حيث خطط الذكاء الاصطناست الكود ولكن لم يخطط للإثبات مسبقاً. طريقة "التخطيط للكود فقط" هذه كانت أداءها أسوأ من P3، مما أكد أن التفكير في الإثبات أثناء التخطيط للكود هو ما يصنع الفارق.

مثال من الواقع: شجرة Red-Black Tree

لإظهار كيف يعمل هذا في الممارسة العملية، نظر المؤلفون في مشكلة كلاسيكية في علوم الحاسوب: حذف عقدة من "شجرة Red-Black" (هيكل بيانات معقد يُستخدم لتنظيم البيانات بكفاءة).

• الطريقة القديمة (البرنامج ثم الإثبات): التزم الذكاء الاصطناعي بطريقة معينة لحذف العقدة. تبين أن هذه الطريقة كانت فوضوية بنيوياً لدرجة أن الإثبات تطلب أكثر من 6,300 سطر من الكود فقط لإصلاح الثغرات، أو فشل تماماً.
• طريقة P3: خطط الذكاء الاصطناዊ أولاً لعملية الحذف. أدرك أن نهجاً بنيوياً مختلفاً سيكون أسهل في الإثبات. التزم بهذا المخطط وحل المشكلة في 1,105 سطر فقط.

لماذا هذا مهم؟

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