ملخص تقني: COMPOSE – تأليف النظريات المستقبلية من الاستشهادات والبنية الصورية

تعريف المشكلة

تتناول الورقة تحدي التوليد الرياضي المستقبلي المرتكز على أسس (grounded future mathematical generation): وهي مهمة التنبؤ بادعاء رياضي مستقبلي معقول (بيان يشبه النظرية) لورقة بحثية "مرجعية" (anchor paper). يرى المؤلفون أن التنبؤ الصالح يجب أن يستوفي قيدين متزامنين:

1. المسار العلمي: يجب أن يمتد ليشمل اتجاه البحث الذي يشير إليه مخطط الاستشهادات العلمية وتطور الأفكار في الأدبيات.
2. الارتكاز الصوري (Formal Grounding): يجب أن يحترم التبعيات المنطقية المتأصلة في الرياضيات الصورية، مما يضمن أن يكون الادعاء قابلاً للاشتقاق بشكل صحيح من التعريفات والمبرهنات والتمهيدات الموجودة.

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

المنهجية: إطار عمل COMPOSE

يقترح المؤلفون COMPOSE، وهو إطار عمل ثنائي الرسوم البيانية (dual-graph framework) يقوم بتكييف نموذج لغوي بناءً على سياق الاستشهاد العلمي وبنية النظرية الصورية. يتكون هذا النهج من ثلاثة مكونات رئيسية:

1. بناء البيانات

قام المؤلفون ببناء مجموعة بيانات تحتوي على 108,000 مثال من الرسوم البيانية المزدوجة (علمية-صورية) المستمدة من أوراق الرياضيات على arXiv (من 2000 إلى 2023) ومكتبة Lean Mathlib.

• الرسم البياني العلمي ($G_s$): تم بناؤه من ورقة مرجعية وسياق استشهاداتها (حتى خطوتين). ويتضمن عقدًا مجردة للأوراق وعقدًا للنظريات المستخرجة من النص. تمثل الحواف روابط الاستشهاد والتبعيات الداخلية للورقة.
• الرسم البياني الصوري ($G_f$): تم بناؤه عبر محاذاة النظريات غير الصورية المستخرجة مع النظريات المقابلة لها في Mathlib. تستخدم هذه المحاذاة FrenzyMath (وهي مجموعة بيانات من الأوصاف البشرية غير الصورية لنظريات Mathlib) لإجراء استرجاع (غير صوري إلى غير صوري)، لتجنب الضجيج الناتج عن التحويل التلقائي المباشر إلى صيغة رسمية. يتوسع الرسم البياني الصوري من جذر النظرية المطابقة باستخدام حواف التبعية المستخرجة عبر LeanDojo.
• الاختبار المعياري: مجموعة اختبار مستبعدة زمنياً تتكون من 47,000 ورقة مستقبلية من أواخر عام 2024 وعام 2025، استُخدمت لتقييم قدرة النموذج على التنبؤ بالنتائج المنشورة فعلياً.

2. بنية النموذج

يستخدم COMPOSE بنية مشفر مزدوج (dual-encoder) متبوعة بمفكك شفرة مشروط بالرسم البياني:

• المشفرات المزدوجة: تعالج شبكتان عصبيتان رسوميتان (GNNs) مخصصتان $G_s$ و $G_f$ بشكل منفصل.
  • يتم تهيئة عقد $G_s$ باستخدام تضمينات E5 (النص العلمي).
  • يتم تهيئة عقد $G_f$ باستخدام تضمينات DeepSeek-Math (التواقيع الصورية).
  • يستخدم كلاهما تمرير رسائل موجه ومحدد بنوع الحافة مع اتصالات متبقية محكومة (gated residual connections).
• وحدة الدمج (Fusion Module): يتم إسقاط تمثيلات كلا الرسمين البيانيين في فضاء كامن مشترك ودمجهما عبر آلية الانتباه المتقاطع ثنائي الاتجاه (bidirectional cross-attention). يسمح هذا للنموذج بدمج الاتجاه العلمي مع القيود الصورية.
• مفكك الشفرة (Decoder): نموذج لغوي كبير (LLM) متخصص في الرياضيات (DeepSeek-Math-7B أو Mistral-7B) تم تكييفه باستخدام تقنية LoRA. تُدرج طبقات الانتباه المتقاطع في مفكك الشفرة لتهيئة عملية التوليد بناءً على تضمينات الرسم البياني المدمجة، مما يسمح للنموذج بالانتباه إلى بنية الرسم البياني الكاملة أثناء توليد الرموز (tokens).

3. التدريب على مرحلتين

• المرحلة الأولى (تعلم التمثيل): يتم تدريب المشفرات الرسومية ووحدة الدمج بدون مفكك الشفرة باستخدام ثلاثة أهداف:
  • توقع الروابط (Link Prediction): لضمان قدرة المشفرات على التقاط بنية الرسم البياني.
  • المحاذاة التباينية (Contrastive Alignment): لمحاذاة تمثيل الرسم البياني المدمج مع ملخص الورقة وادعائها الرئيسي.
  • المحاذاة المتقاطعة (Cross-Alignment): لمحاذاة عقد النظريات غير الصورية مع نظيراتها الصورية المطابقة بشكل صريح.
• المرحلة الثانية (التوليد): يتم إضافة مفكك الشفرة وضبطه بدقة باستخدام:
  • خسارة التنبؤ الذاتي (Autoregressive Loss): التنبؤ القياسي بالرمز التالي.
  • خسارة الهامش الرسومي (Graph Margin Loss): حد تنظيمي يعاقب النموذج إذا ولد نفس النص لزوج غير متطابق من الرسوم البيانية، مما يجبره على الاعتماد على سياق الرسم البياني المحدد.

النتائج الرئيسية

أجريت التجارب على الاختبار المعياري المكون من 47 ألف ورقة مستقبلية، مع مقارنة COMPOSE بنماذج أساسية قوية (بما في ذلك GIANTS، وFutureGen، وGoAI، بالإضافة إلى متغيرات تعتمد فقط على النص أو المطالبات فقط).

• أداء الاسترجاع: حقق COMPOSE أعلى فجوة (Gap) بلغت (0.240)، وهي الفرق في تشابه جيب التمام (cosine similarity) بين النص المولد والورقة المستقبلية الحقيقية مقابل الأوراق غير ذات الصلة. وقد تفوق بشكل كبير على النماذج الأساسية في H@10 (50.8%) وفي H@100 (80.8%)، مما يشير إلى أن ادعاءاته المولدة أكثر قدرة على استرجاع الورقة المستقبلية الصحيحة من المجموعة.
• التنبؤ بالادعاء الرياضي الجديد (NMCP): تصدر COMPOSE في الدقة (Precision: 0.560) والمطابقة (Match: 0.730)، مما يثبت أن مخرجاته تتوافق مع النظريات المستقبلية على المستويين الصوري وغير الصوري، وليس فقط من حيث الموضوع.
• تقييم الحكم اللغوي (LLM-Judge): قام حكم لغوي (GPT-4.0) بتقييم المخرجات من حيث المحتوى، والعمق، والجدة، والدقة، والخصوصية. حقق COMPOSE أعلى درجة إجمالية (3.36/5)، لا سيما في العمق التقني (3.52) والخصوصية (3.52)، حيث أنتج مخرجات أكثر مادية وثراءً رياضياً مقارنة بالنماذج الأساسية التي غالباً ما تولد ملخصات غامضة.
• دراسات الاستئصال (Ablation Studies): أدى إزالة أي من مشفري الرسم البياني (العلمي أو الصوري) إلى انخفاض كبير في الأداء، مما يؤكد أن كلا الوسيطين يوفران إشارات متكاملة. كان الرسم البياني الصوري حاسماً للارتكاز، بينما كان الرسم البياني العلمي ضرورياً لتحديد الاتجاه البحثي الصحيح.

الأهمية والادعاءات

تدعي الورقة أن توليد الرياضيات المستقبلية يستفيد من الجمع بين السياق العلمي والبنية الصورية.

• التوليد المرتكز (Grounded Generation): يوضح المؤلفون أن الاعتماد فقط على النصوص العلمية يؤدي إلى ادعاءات ذات صلة موضوعية ولكنها غير مرتكزة منطقياً، بينما الاعتماد فقط على البنية الصورية يحد من النموذج ضمن النظريات المعروفة دون القدرة على استباق اتجاهات جديدة. نجح COMPOSE في جسر هذه الفجوة.
• المساهمة في البيانات: يوفر بناء مجموعة البيانات المزدوجة (108 ألف زوج) والاختبار المعياري للورقة المستقبلية (47 ألف ورقة) مورداً جديداً لتقييم التوليد الرياضي المرتكز، مما يعالج نقص الاختبارات الزمنية في هذا المجال.
• التقدم المنهجي: يقدم إطار العمل ثنائي الرسوم البيانية مع الانتباه المتقاطع نهجاً مبتكراً لدمج مصادر المعرفة غير المتجانسة (الأدبيات غير الصورية مقابل المنطق الصوري) للمهام التوليدية.

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