Benchmarking Testing in Automated Theorem Proving

إليك ملخص تقني مفصل لورقة البحث "Benchmarking Testing in Automated Theorem Proving" (تقييم الاختبار في إثبات النظريات الآلي) للباحثين: Jongyoon Kim، وHojae Han، وSeung-won Hwang.

1. بيان المشكلة

أدى التقدم السريع في النماذج اللغوية الكبيرة (LLMs) إلى تحسين قدرتها على توليد البراهين الصورية في أنظمة مثل Lean. ومع ذلك، تعاني طرق التقييم الحالية من خلل جوهري: فهي تخلط بين الصلاحية النحوية (Syntactic Validity) والصحة الدلالية (Semantic Correctness).

• قصور عملية التجميع (Compilation): تقيم المعايير المرجعية الحالية (مثل MiniF2F وProofNet) النماذج بشكل أساسي من خلال التحقق مما إذا كان البرهان المولد يتوافق برمجياً (Compiles). وبينما يتحقق التجميع من أن الكود سليم نحوياً ومتسق منطقياً بمعزل عن غيره، فإنه لا يضمن أن النظرية تجسد المعنى الرياضي المقصود.
• مشكلة "التكرار البديهي" (Tautology Problem): يمكن للنموذج أن يولد تكراراً بديهياً تافهاً (مثلاً: $a + b = a + b$) يتوافق برمجياً بنجاح، ولكنه يفشل في إثبات العبارة غير البديهية المقصودة (مثلاً: خاصية الإبدال $a + b = b + a$).
• عدم كفاية المؤشرات البديلة: تعتمد المحاولات الحالية لقياس الصحة الدلالية على مؤشرات غير موثوقة مثل التداخل اللفظي (درجات BLEU) مقابل مراجع مكتوبة بشرياً أو الفحص اليدوي. هذه الطرق إما أنها مشوشة، أو تتطلب جهداً بشرياً مكلفاً، أو تفشل في التمييز بين المعاني الدلالية الصحيحة والخاطئة.

2. المنهجية

يقترح المؤلفون تحولاً جذرياً مستوحى من اختبار التكامل (Integration Testing) في هندسة البرمجيات. فبدلاً من تقييم نظرية بمعزل عن غيرها، يقومون بتقييمها بناءً على كيفية تفاعلها مع بقية قاعدة الكود (Codebase).

المفهوم الجوهري: اختبار النظرية (T2)

استناداً إلى مراسلة كوري-هوارد (حيث تقابل البراهين البرامج)، يعامل المؤلفون النظرية المولدة كدالة (Function)، والنظريات التي تعتمد عليها كـ "حالات اختبار" (Test Cases).

• رسم بياني للتبعية (Dependency Graph): قاموا ببناء رسم بياني للتبعية حيث تمتلك النظرية المستهدفة ($t_{GT}$) سوابق (تعريفات/تمهيدات تستخدمها) ولواحق (نظريات تستدعيها أو تبني عليها).
• منطق اختبار التكامل: إذا كانت النظرية المولدة ($t_{fl}$) غير صحيحة دلالياً (على سبيل المثال، إذا عرفت تكراراً بديهياً بدلاً من الخاصية المقصودة)، فإن أي نظرية لاحقة تعتمد عليها ستفشل في عملية التجميع.
• تشبيه حذف القطع (Cut Elimination): العملية متجذرة رسمياً في المبدأ المنطقي لـ "حذف القطع". إذا فشلت سلسلة من البراهين ($X \to Y \to Z \to W$) عند استبدال التمهيد الوسيط ($Y$) بالمرشح المولد، فإن المرشح يكون غير صحيح دلالياً.

معيار T2

أنشأ المؤلفون معياراً واسع النطاق، T2، لتسهيل هذا التقييم:

• المصدر: مستخرج من 5 مستودعات حقيقية للغة Lean 4 (تغطي الجبر، الطوبولوجيا، نظرية الأعداد، إلดับ).
• النطاق: 2,206 مسألة، كل منها مقترن بمتوسط 41 نظرية لاحقة.
• المجموعة الصعبة (Hard Subset): مجموعة فرعية من 389 مسألة "صعبة" حيث يجب على النموذج توليد كل من القضية (العبارة) والبرهان معاً، بدلاً من مجرد ملء فراغ برهان لعبارة معطاة.
• الأتمتة: عملية الاستخراج مؤتمتة بالكامل، ولا تتطلب أي توصيف بشري لهيكل التبعية. تم توليد الأوصاف باللغة الطبيعية (NL) بواسطة نموذج لغوي قوي (Claude Sonnet 4.5) وتم التحقق منها يدوياً لعينة مختارة.

المقياس: دقة الاختبار (Testing Accuracy - TA)

يقدم البحث دقة الاختبار (TA) كمقياس تقييم أساسي:
$$TA = E_{P \sim D} \left[ \prod_{i=1}^{k} \text{compiles}(t^{(i)}_{succ} \mid t_{fl}) \right]$$
لا تنجح النظرية المولدة إلا إذا نجحت جميع نظريات التبعية اللاحقة في التجميع بنجاح عند استبدال النظرية الأصلية بالنظرية المولدة.

3. المساهمات الرئيسية

1. معيار T2: أول معيار واسع النطاق وغني بالتبعية لإثبات النظريات الصورية، ينتقل من المسائل المعزولة إلى سياقات المستودعات الحقيقية.
2. دقة الاختبار (TA): مقياس جديد، آلي، وخالٍ من المراجع، يتحقق مباشرة من الصحة الدلالية من خلال تجميع الوحدات المعتمدة.
3. تحليل الفجوة التجريبية: تقييم شامل لـ 18 نموذجاً من أحدث النماذج (المفتوحة والمغلقة المصدر) يكشف عن انفصال هائل بين نجاح التجميع والصحة الدلالية.
4. رؤى سياقية: أثبت البحث أن توفير النظريات اللاحقة كـ سياق (Context) يحسن الصحة الدلالية بشكل كبير، بينما توفير البراهين باللغة الطبيعية فقط لا يفعل ذلك.

4. النتائج التجريبية

قيم المؤلفون 18 نموذجاً (بما في ذلك GPT-5، وClaude-Sonnet-4.5، وLlama-3.1، ونماذج متخصصة في الرياضيات مثل DeepSeek-Prover) على معيار T2.

• الفجوة الدلالية:

  • دقة التجميع (Compilation Accuracy): حققت النماذج معدلات تجميع عالية (مثلاً، Claude-Sonnet-4.5 حقق 80.3% في المجموعة الكاملة).
  • دقة الاختبار (TA): حققت نفس النماذج درجات TA أقل بكثير (مثلاً، Claude-Sonnet-4.5 حقق 38.9% في المجموعة الكاملة؛ و 4.5% في المجموعة الصعبة).
  • الإيجابيات الكاذبة (False Positives): وُجد أن ما يصل إلى 93.1% من النظريات القابلة للتجميع كانت غير صحيحة دلالياً عند اختبارها مقابل النظريات اللاحقة.

• فشل المقاييس الحالية:

  • BLEU: لم يظهر التداخل اللفظي العالي (درجات BLEU) أي ارتباط يذكر بالصحة الدلالية (الارتباط: 0.123). يمكن للنماذج توليد براهين متشابهة نصياً ولكنها خاطئة منطقياً.
  • النماذج المتخصصة: غالباً ما حققت النماذج التي تم ضبطها بدقة (Fine-tuned) خصيصاً لإثبات النظريات معدلات تجميع أعلى، لكنها أدت بشكل أسوأ أو مماثل للنماذج العامة في مقياس TA، مما يشير إلى أنها تفرط في التكيف (Overfit) مع القواعد النحوية بدلاً من الدلالات.

• تأثير السياق:

  • توفير النظريات اللاحقة (Successor Theorems) كـ سياق مدخل أدى باستمرار إلى تحسين TA (مثلاً، +4.9% لـ Claude-Sonnet-4.5).
  • توفير البراهين باللغة الطبيعية (NL Proofs) وحدها دون النظريات اللاحقة لم يحسن الأداء بل أدى أحياناً إلى تراجعه.
  • التلقين بأسلوب القليل من الأمثلة (Few-shot prompting) و التحسين التكراري (Iterative refinement) (باستخدام تغذية راجع المترجم) لم يحققا تحسينات تذكر في المجموعة الصعبة، مما يشير إلى أن الصعوبة تكمن في الاستدلال الدلالي العميق، وليس فقط في تنسيق المهمة.

5. الأهمية والخاتمة

يتحدى هذا البحث بشكل جوهري الوضع الراهن لتقييم إثبات النظريات الآلي (ATP).

• إعادة تعريف النجاح: يثبت أن "التجميع" هو شرط ضروري ولكنه غير كافٍ لتوليد النظريات. يمكن للنموذج أن يكون مثالياً من الناحية النحوية ولكنه عديم الفائدة دلالياً.
• الموثوقية: يوفر معيار T2 ومقياس TA طريقة صارمة وآلية لتقييم ما إذا كان النموذج اللغوي الكبير يفهم حقاً المفاهيم الرياضية أم أنه يكتفي بهلوسة كود سليم نحوياً.
• الاتجاه المستقبلي: تشير هذه الدراسة إلى أن أنظمة ATP المستقبلية يجب أن تُقيم بناءً على قدرتها على التكامل في قواعد الكود الموجودة (التوليد المدرك للتبعية) بدلاً من مجرد حل ألغاز معزولة. كما تسلط الضوء على أن توفير "مجموعة الاختبار" (النظريات اللاحقة) للنموذج أثناء عملية التوليد هو استراتيجية حاسمة لتحسين التوافق الدلالي.

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