VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
تقدم هذه الورقة VeriSoftBench، وهو معيار قياسي على مستوى المستودعات يضم 500 التزام بإثبات لغة Lean 4 من مشاريع التحقق من البرمجيات مفتوحة المصدر، كاشفةً أن النماذج اللغوية الكبيرة الحالية تعاني في الانتقال من الإعدادات الرياضية إلى الإعدادات المتمحورة حول الكود، ومسلطةً الضوء على التأثير الحاسم للتبعية بين الملفات على نجاح أتمتة الإثبات.
تخيل أنك تحاول تعليم متدرب بارع ولكنه يفتقر للخبرة كيفية إصلاح آلة معقدة.
الطريقة القديمة (المعايير الرياضية) لفترة طويلة، قام الباحثون باختبار هؤلاء "المتدربين" من الذكاء الاصطناعي باستخدام Mathlib. فكر في Mathlib كأنه مكتبة ضخمة ومنظمة بشكل مثالي للحقائق الرياضية العالمية. الأمر يشبه إعطاء المتدرب كتاباً مدرسياً واحداً ضخماً حيث كل تعريف فيه قياسي، وكل فصل فيه مرقم، والإجابات على المسائل توجد دائماً في نفس الأماكن المتوقعة.
المشكلة: البرمجيات في العالم الحقيقي ليست مثل الكتاب المدرسي للرياضيات. إنها أشبه بموقع بناء فوضوي ومتوسع، حيث لكل مبنى مخططاته الخاصة، وأدواته المخصصة، وقواعده المحلية الغريبة التي لا توجد في أي مكان آخر.
التحدي الجديد: VeriSoftBench أدرك مؤلفو هذه الورقة أن الذكاء الاصطناعي أصبح بارعاً في حل المسائل الرياضية لكنه يفشل فشلاً ذريعاً في التحقق من البرمجيات في العالم الحقيقي. لذا، قاموا ببناء VeriSoftBench.
فكر في VeriSoftBench كأنه مستودع ضخم وفوضوي يحتوي على 500 "لغز برهاني" مختلف.
كل لغز هو مهمة محددة من مشروع برمجيات مفتوح المصدر (مثل بلوكشين آمن أو مترجم لغات برمجة).
لحل اللغز، لا يمكن للذكاء الاصطناعي مجرد البحث عن قاعدة قياسية. عليه أن يتجول في المستودع، ليجد الأداة المخصصة التي اخترعها المشروع بالأمس، ويفهم كيف تتصل بأداة أخرى من ملف يبعد ثلاثة ملفات، ثم يكتشف كيفية استخدامها لإصلاح المشكلة الحالية.
إنه الفرق بين حل لغز "سودوكو" (قواعد قياسية) ومحاولة إصلاح محرك سيارة حيث الكتيب الخاص بها مكتوب بشفرة سرية خاصة بهذا الطراز من السيارات فقط.
التجربة: طريقتان لمساعدة المتدرب اختبر الباحثون الذكاء الاصطناعي تحت ظروف مختلفة لمعرفة كيفية تعامله مع هذه الفوضى:
"الصندوق المنسق" (المرشد المتعاون): تخيل مرشداً ينظر إلى اللغز، ويجد فقط الأدوات والمخططات التي يحتاجها الذكاء الاصطناعي بالضبط، ثم يسلمها له في صندوق صغير ومرتب.
النتيجة: أدى الذكاء الاصطناعي بشكل جيد (حوالي 40% نجاح). كان بإمكانه حل اللغز عندما تم القيام بالعمل الشاق المتمثل في العثور على الأدوات الصحيحة نيابة عنه.
"المستودع الكامل" (الغوص في الطوفان): تخيل إلقاء الذكاء الاصطناعي في المستودع بأكمله مع ملايين الأدوات والمخططات والقطع العشوائية الأخرى، وإخباره: "حظاً موفقاً، ابحث عما تحتاجه!"
النتيجة: أصيب الذكاء الاصطناعي بالارتباك. انخفضت معدلات النجاح بشكل كبير. جعل حجم "الضجيج" الهائل من الصعب العثور على "الإشارة".
الاكتشافات الرئيسية (لحظات الـ "آها!")
خبراء الرياضيات ليسوا خبراء برمجيات: نماذج الذكاء الاصطناعي التي تعد أبطالاً في حل المسائل الرياضية (مثل تلك المدربة على Mathlib) انهارت تماماً عند مواجهة هذه الألغاز البرمجية. لقد كانوا مثل لاعب شطرنج عظيم يحاول لعب البوكر؛ فالمهارات لم تنتقل.
تشبيه: تخيل وصفة طعام. الوصفة البسيطة تحتاج دقيقاً وبيضاً. أما الوصفة المعقدة فتحتاج دقيقاً، ولكن الدقيق يعتمد على نوع معين من القمح، والذي يعتمد بدوره على سماد معين، والذي يعتمد بدوره على نمط مطر معين.
في VeriSoftBench، لكي يحل الذكما الاصطناعي مشكلة ما، غالباً ما يتعين عليه تتبع سلسلة من 10 أو 20 تعريفاً مخصصاً داخل الكود. وكلما طالت السلسلة، زاد احتمال ضياع الذكاء الاصطناعي.
السياق سلاح ذو حدين: إعطاء الذكاء الاصطناعي الكثير من المعلومات (المستودع الكامل) كان أسوأ من إعطائه (الصندوق المنسق) الذي يحتوي على القدر المناسب فقط. ومع ذلك، حتى مع وجود "الصندوق المثالي" من الأدوات، ظل الذكاء الاصطناعي يعاني. وهذا يعني أن المشكلة ليست فقط في إيجاد المعلومات الصحيحة؛ بل في الاستنتاج المنطقي عبر منطق مخصص ومعقد لم يره الذكاء الاصطناعي من قبل.
لماذا هذا مهم؟ حالياً، الذكاء الاصطناعي رائع في "الرياضيات المدرسية" لكنه سيء في "الهندسة في العالم الحقيقي". هذه الورقة تطلق جرس إنذار: إذا أردنا للذكاء الاصطناعي أن يساعدنا في كتابة برمجيات آمنة وخالية من الأخطاء (مثل السيارات ذاتية القيادة أو الأجهزة الطبية)، فلا يمكننا فقط تدريبه على المسائل الرياضية. نحن بحاجة لتعليمه كيفية التنقل في قواعد بيانات برمجية مخصصة وفوضوية حيث يتم ابتكار القواعد أثناء العمل.
باختأصر: تقول الورقة: "لقد بنينا اختباراً جديداً يحاكي هندسة البرمجيات الحقيقية. وجدنا أن الذكاء الاصطناعي الحالي يشبه طالباً اجتاز الامتحان النهائي بتفوق، لكنه لا يستطيع إصلاح صنبور يسرب الماء لأن الصنبور يستخدم قطعة مخصصة لم يرها من قبل. نحن بحاجة لتعليمه كيفية التنقل في الورشة الفوضوية، وليس فقط في الفصل الدراسي النظيف."
إليك ملخص تقني مفصل لورقة البحث بعنوان "VeriSoftBench: معايير التحقق الرسمي على مستوى المستودعات لـ Lean".
1. بيان المشكلة
بينما أظهرت النماذج اللغوية الكبيرة (LLMs) وعوداً كبيرة في مجال إثبات النظريات التفاعلي (ITP)، لا سيالما ضمن منظومة Lean، إلا أن المعايير الحالية تعاني من عدم تطابق جوهري في النطاق.
الفجوة: معظم المعايير الحالية (مثل MiniF2F و ProofNet و PutnamBench) مستمدة من الرياضيات (Mathlib)، حيث تعتمد البراهين على منظومة مشتركة ومستقرة من التجريدات القياسية.
الواقع: تُطور البراهين في التحقق من البرمجيات ونظرية الميتا للغات البرمجة داخل مستودعات ضخمة مفتوحة المصدر. تتضمن هذه المهام:
تعريفات خاصة بالمشروع: أنواع بيانات مخصصة، عمليات، وثوابت فريدة من نوعها داخل الكود المصدري. بناءً على هياكل معقدة عابرة للملفات واعتمادات متعددة الخطوات.
ضجيج السياق: السياق ذو الصلة يكون مدفوناً داخل قواعد كود ضخمة، مما يجعل عملية الاسترجاع صعبة.
السؤال: إلى أي مدى يمكن للمثبتات الحالية، التي تم ضبطها لتناسب المعايير الرياضية، أن تتعمم على مهام التحقق من البرمجيات على مستوى المستودعات حيث تكون "المكتبة" عبارة عن قاعدة كود مخصصة لمشروع معين؟
2. المنهجية: VeriSoftBench
يقدم المؤلفون VeriSoftBench، وهو معيار جديد مصمم لتقييم المثبتات في بيئات المستودعات الواقعية.
بناء مجموعة البيانات
المصدر: 500 التزام برهاني (proof obligation) في لغة Lean 4 مستخرجة من 23 مستودعاً متنوعاً من مستودعات الأساليب الرسمية مفتوحة المصدر (تغطي المترجمات، أنظمة النوع، دوائر المعرفة الصفرية، والبروتوكولات).
معايير الاختيار:
يجب أن تكون المهام ذات براهين حقيقية صالحة وخالية من الفجوات (hole-free).
يجب أن تشير النظريات إلى تعريف واحد على الأقل محلي في المستودع.
يتم استبعاد الأهداف البديهية التي يمكن حلها بواسطة الأتمتة القياسية (مثل simp أو omega).
التعبئة: على عكس المعايير السابقة التي تعمل على توحيد المهام في مكتبة مشترية، يحافظ VeriSoftBench على سياق الملف المحلي الأصلي والاعتمادات العابرة للملفات.
مقاييس الصعوبة: يتم تقييم المهام بناءً على تعقيد البرهان (طول نص التكتيك/tactic script) والاعتماد السياقي (عدد التعريفات أو الروابط المميزة المستمدة من المستودع).
التكوينات السياقية
لعزل تحديات استرجاع السياق مقابل القدرة على الاستنتاج، يقيم المعيار المثبتات تحت نظامين:
السياق المنسق (Curated Context): يتلقى المثبت سياق الملف المحلي بالإضافة إلى مجموعة مركزة من تبعات المستودع الضرورية (التعريفات والروابط التي يتم استدعاؤها مباشرة أو بشكل متعدٍ من قبل البرهان الحقيقي). يتم حذف أجسام البراهين لمنع التسريب. يمثل هذا سيناريو "أفضل حالة" للاسترجاع.
سياق المستودع الكامل (Full Repository Context): يتلقى المثبت مكتبة المستودع بأكملها (جميع الملفات، التعريفات، والروابط). هذا يحاكي سيناريو النشر الواقعي حيث يجب على النموذج تحديد الحقائق ذات الصلة من مساحة بحث ضخمة. تتجاوز بعض المستودعات مئات الآلاف من الرموز (tokens)، مما يستلزم عملية قص (truncation) للنماذج الحالية.
3. المساهمات الرئيسية
معيار VeriSoftBench: مجموعة بيانات تضم 500 مهمة من مستوى المستودعات في Lean 4، والتي تصور صراحة الاعتمادات العابرة للملفات والتجريدات الخاصة بالمشاريع، مما يسد الفجوة بين المعايير الرياضية والتحقق من البرمجيات في العالم الحقيقي.
تقييم شامل: تقييم للنماذج اللغوية الكبيرة الرائدة (GPT-5.2، Claude Opus 4.5، Gemini-3-Pro) والمثبتات المتخصصة (Gödel-Prover-V2، Aristotle) تحت كل من إعدادات السياق المنسق والسياق الكامل.
تحليل الاعتماد: تحليل هيكلي يكشف أن عمق الاعتماد المتعدي (سلاسل الاستنتاج متعددة الخطوات) هو العائق الأساسي، أكثر من مجرد حجم التبعات.
4. النتائج التجريبية
أسفر التقييم عن ثلاث ملاحظات رئيسية:
ضعف الانتقال من الرياضيات إلى التحقق: تؤدي المثبتات المحسنة للرياضيات من نمط Mathlib بشكل سيء في بيئات المستودعات.
مثال: حقق Gödel-Prover-V2، وهو مثبت متخصص متطور للرياضيات، نسبة نجاح 0% في سياق المستودع الكامل و 5.6% فقط في السياق المنسق.
أفضل أداء: حقق Gemini-3-Pro أعلى معدل نجاح بنسبة 41.0% (منسق) و 34.8% (كامل)، لكن هذه الأرقام تظل منخفضة مقارنة بالمعايير الرياضية.
الارتباط بالاعتماد المتعدي: يرتبط النجاح ارتباطاً عكسياً قوياً مع تعقيد مخطط الاعتماد.
المهام التي تتطلب الاستنتاج عبر سلاسل طويلة من تعريفات المشروع المحلية (العمق المتعدي ≥ 5) هي أصعب بكثير.
لم يظهر عدد الاعتمادات المباشرة أي ارتباط معنوي بالنجاح، مما يشير إلى أن الصعوبة تكمن في التنقل عبر التجريدات الطبقية وليس مجرد العثور على الرموز.
استرجاع السياق مقابل الاستنتاج:
المنسق > الكامل: يوفر تقديم مجموعة منسقة من التبعات أداءً أفضل من المستودع الكامل (على سبيل المثال، Gemini-3-Pro: 41.0% مقابل 34.8%).
رؤية غير متوقعة: الفجوة في الأداء بين السياق المنسق والسياق الكامل أصغر مما كان متوقعاً. يفترض المؤلفون أن "الضجيج" في المستودع الكامل يوفر تلميحات هيكلية (أنماط تجريد متكررة، هياكل براهين مشابهة في ملفات أخرى) تساعد النماذج على توقع الروابط الضرورية، حتى لو لم يتم استرجاع التبعية الدقيقة صراحة.
تحول نمط البرهان: تعتمد البراهين في VeriSoftBench بشكل أقل على تكتيكات الأتمتة (21% مقابل 51% في Verina) وبشكل أكبر على تحليل الحالات وهياكل التفرع، مما يشير إلى تحول من "فك التعريفات + الأتمتة" إلى الاستنتاج الهيكلي المعقد.
5. الأهمية والأثر
إعادة تعريف المعايير: يوضح VeriSoftBench أن النجاح في إثبات النظريات الرياضية لا يضمن النجاح في التحقق من البرمجيات. فالأخير يتطلب قدرات للتنقل في قواعد كود ضخمة وغير متجانسة والاستنتاج عبر التجريدات الخاصة بالمشروع.
تحديد العقبات: تسلط الورقة الضوء على أن النماذج الحالية تعاني في الاستنتاج متعدد الخطوات عبر تعريفات المشاريع الطبقية، وليس فقط في استرجاع السياق.
الاتجاهات المستقبلية: تشير النتائج إلى أن أنظمة أتمتة البراهين المستقبلية تحتاج إلى:
آليات أفضل للتعامل مع إغلاقات الاعتماد المتعدي (transitive dependency closures).
بنيات قادرة على الاستفادة من الأنماط الهيكلية عبر مستودع كامل، وليس فقط مخططات الاعتماد المنعزلة.
بيانات تدريب تعكس كثافة وتعقيد أكواد التحقق في العالم الحقيقي بدلاً من مجرد النظريات الرياضية.
في الختام، يضع VeriSoftBench معياراً جديداً لتقييم أدوات التحقق الرسمي، كاشفاً أنه بينما أحرزت النماذج اللغوية الكبيرة تقدماً، إلا أن تحديات كبيرة لا تزال قائمة في أتمتة البراهين ضمن الأنظمة المعقدة والمترابطة للتحقق من البرمجيات في العالم الحقيقي.