LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)

إليك ملخص تقني مفصل لورقة البحث: "LEANCAT: مجموعة اختبار لمجال نظرية الفئات في لغة LEAN (الجزء الأول: الفئات أحادية البعد 1-categories)".

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

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

حدد المؤلفون فجوة حرجة: تعتمد الرياضيات الحديثة على واجهات عالية المستوى، وهياكل قابلة لإعادة الاستخدام، والتنقل عبر مكتبات شاسعة من التعريفات (مثل Mathlib في Lean). وتفشل معايير الاختبار الحالية في اختبار قدرة النماذج على:

• التفكير باستخدام واجهات فئوية عالية المستوى (الدوال، التحولات الطبيعية، الحدود).
• إدارة التبعيات طويلة المدى بين التعريفات.
• تركيب المعرفة من مكتبة ناضجة بدلاً من حل الألغاز المنعزلة.

تفترض الورقة أن نظرية الفئات (Category Theory) هي "اختبار الضغط" المثالي لهذه القدرة نظراً لاعتمادها على الاستدلال المخططي والخصائص الشاملة.

2. المنهجية

أ. معيار LeanCat

قدم المؤلفون LeanCat، وهو مجموعة اختبار تتكون من 100 مهمة في نظرية الفئات مصاغة صورياً بالكامل في لغة Lean 4 (باستخدام Mathlib).

• الهيكل: تنقسم المسائل إلى جزأين:
  • تجريدي (Abstract): مستمد من الكتب المدرسية القياسية (مثل Riech و Mac Lane) ويركز على الواجهات الجوهرية (الارتباطات، الحدود، المونادات).
  • ملموس (Concrete): مستمد من كتاب Abstract and Concrete Categories، ويركز على التجسيد والتحقيق.
• توصيف الصعوبة: تم استخدام خط إنتاج هجين لتقييم الصعوبة (سهل، متوسط، عالٍ):
  • تسجيل النماذج (LLM Scoring): حاولت خمسة نماذج أساسية إجراء البراهين؛ واستُخلصت الدرجات من عدد البراهين الناجحة مقابل العبارات الصحيحة.
  • التسجيل البشري (Human Scoring): قام خبيران بتقييم المسائل بناءً على طول البرهان وتعقيد الحجج.
  • التوزيع: 20 سهلاً، 40 متوسطاً، 40 عالياً. هذا التوزيع المنحاز يمنع التشبع المبكر للنماذج الحالية.
• التصميم: المهام هي مهام "على مستوى العبارة"، مما يعني أن على النموذج إثبات نظرية واحدة دون وجود تمهيدات (lemmas) وسيطة مهيأة، مما يجبر النموذج على التعامل مع استرجاع التعريفات والتنقل في التجريد بشكل مستقل.

ب. استراتيجيات التقييم

تقيم الورقة استراتيجيتين مختلفتين للاستدلال:

1. الأسس الثابتة (العينات المتوازية - Static Baselines):
   • النماذج: GPT-5.2، Claude-Opus-4.5، Gemini-3-Pro، DeepSeek-V3.2، Kimi-K2، ونماذج برهنة متخصصة (مثل DeepSeek-Prover-V2، Goedel-Prover، إلخ).
   • البروتوكول: Pass@k (أخذ عينات من $k$ برهان مستقل)؛ لا توجد أدوات خارجية أو بحث؛ تعتمد النماذج فقط على معرفتها الداخلية.
2. LeanBridge (الوكيل المعزز بالاسترجاع - Retrieval-Augmented Agent):
   • البنية: حلقة استرجاع–توليد–تحقق متسلسلة (Retrieve–Generate–Verify).
   • الآلية:
     • الاسترجاع (Retrieve): يستخدم LeanExplore (ترتيب هجين: تضمينات دلالية + BM25 + PageRank) للاستعلام عن التعريفات والتمهيدات ذات الصلة من Mathlib.
     • التوليد (Generate): يحاول النموذج اللغوي الكبير إجراء برهان باستخدام السياق المسترجع.
     • التحقق (Verify): يقوم مترجم Lean بالتحقق من البرهان.
     • التحسين (Refine): إذا فشل التحقق، يتم تغذية رسالة الخطأ إلى النموذج اللغيدي لتحسين استعلام البحث أو استراتيجية البرهان.
   • الإعدادات: تم الاختبار باستخدام مدخلات "اللغة الطبيعية فقط" (NL-only) ومدخلات "اللغة الطبيعية + العبارة الصورية" (NL+Statement).

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

1. معيار LeanCat: أول معيار مخصص لنظرية الفئات، يغطي 8 مجموعات موضوعية (من الخصائص الأساسية إلى المونادات) مصممة لاختبار الاستدلال الهيكلي بدلاً من الحساب الروتيني.
2. خط إنتاج توصيف الصعوبة: نظام تسجيل هجين مبتكر يجمع بين الحكم الخبير وأداء النماذج لإنشاء مقياس صعوبة موثوق.
3. اكتشاف "فجوة التجريد": دليل تجريبي يظهر أن النماذج الحالية المتطورة تعاني من انخفاض كارثي في الأداء في المهام متوسطة إلى عالية الصعوبة التي تتضمن التجريد، رغم أدائها العالي في المهام السهلة.
4. وكيل LeanBridge: إطار عمل معزز بالاسترجاع يثبت أن التفاعل الديناميكي مع المكتبة هو ضرورة حتمية وليس مجرد تحسين.

4. النتائج

أ. فجوة التجريد (الأسس الثابتة)

• الأداء العام: حقق أفضل نموذج (Claude-Opus-4.5) نسبة نجاح قدرها 12.0% فقط عند Pass@4.
• انهيار الأداء مع الصعوبة: انخفض الأداء بشكل حاد مع زيادة الصعوبة:
  • سهل: 55.0%
  • متوسط: 2.5%
  • عالٍ: 0.0%
• البرهنات المتخصصة: حتى النماذج المدربة خصيصاً للرياضيات الصورية (مثل DeepSeek-Prover-V2) فشلت في التعميم، حيث حققت 0% في المهام المتوسطة والعالية رغم ميزانية أخذ عينات ضخمة (Pass@32). يشير هذا إلى الإفراط في التخصيص (overfitting) لبيانات نمط الأولمبياد.

ب. أداء LeanBridge

• معدل النجاح: حقق LeanBridge (مع GPT-5.2 و NL+Statement) ذروة نجاح بلغت 24.0%، وهو ما ضاعف أداء أفضل أساس ثابت.
• كسر حاجز الصعوبة العالية: كان هو النهج الوحيد الذي حل المهام عالية الصعوبة (2.5% نجاح)، بينما فشلت الأسس الثابتة والوكلاء غير المرتبطين بالمكتبة تماماً (0%).
• تأثير التأسيس الصوري: كان توفير العبارة الصورية (NL+Statement) حاسماً؛ حيث حسن أداء المهام المتوسطة من 5.0% إلى 25.0% وفتح المجال لحلول المهام العالية الصعوبة.
• دراسة الاستبعاد (Ablation Study): إزالة قدرة البحث ("No-Search" agent) أدى إلى انخفاض الأداء بشكل كبير في المهام الصعبة، مما يثبت أن التحسين المتكرر وحده لا يكفي بدون استرجاع المعرفة الديناميكي.

ج. تحليل أنماط الفشل

حدد التحليل النوعي للمحاولات الفاشلة خمسة أنماط فشل مهيمنة:

1. فشل رياضي (Math Failure): استراتيجية رياضية غير صحيحة (مثل استخدام الحقائق الفارغة للأهداف الوجودية).
2. فشل قواعد لغة Lean (Lean Grammar Failure): أخطاء في بناء الجملة أو التوضيح (أقواس خاطئة، ترتيب الروابط).
3. الهلوسة (Hallucination): استدعاء تمهيدات أو ثوابت غير موجودة.
4. الفشل الكسول (Lazy Failure): تجنب بناء التمهيدات الوسيطة الضرورية.
5. فشل التحايل (Hack Failure): تغيير المعنى الصوري للعبارة لجعلها قابلة للإثبات بشكل تافه.

5. الأهمية والعمل المستقبلي

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

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