Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

خاتمة تقنية: اكتشاف نظريات جديدة عبر النماذج اللغوية الكبيرة (LLMs) باستخدام التعلم القائم على السياق لإثبات النظريات في لغة Lean

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

المنهجية: حلقة التخمين والإثبات (CPL)
يقترح المؤلفون حلقة التخمين والإثبات (CPL)، وهي مسار مصمم لتوليد تخمينات رياضية والتحقق منها تلقائياً في لغة Lean 4. يقوم هذا الإطار بفصل عملية توليد التخمين عن توليد الإثبات، ويستخدم مكتبة من النظريات التي تم التحقق منها مسبقاً كـ "سياق" لكلتا المرحلتين.

يعمل المسار من خلال أربعة مكونات رئيسية: وحدة المُخمّن (وكيل LLM)، وحدة المُثبِت (وكيل LLM)، خادم Lean، ومكتبة (بيانات كود Lean).

1. مرحلة التخمين: يقوم المُخمّن بتوليد عبارات رياضية جديدة بتنسيق Lean 4 بناءً على المكتبة الحالية. ويستعلم من خادم Lean لضمان الصلاحية النحوية والجدّة (لضمان أن العبارة ليست قابلة للإثبات بالفعل بواسطة النظريات الموجودة في Mathlib4 أو المكتبة الحالية).
2. مرحلة الإثبات: لكل تخمين صالح، يحاول المُثبِت بناء إثبات صوري. ومن الأهمية بمكان تزويد المُثبِت بالمكتبة (التي تحتوي على النظريات والبراهين التي تم التحقق منها سابقاً) كـ "سياق". وهذا يتيح للنموذج اللغوي الكبير تعلم استراتيجيات الإثبات من خلال التعلم القائم على السياق (In-context learning) دون الحاجة لإعادة تدريب النموذج. يقوم المُثبِت بالتكرار حتى يصل إلى أقصى عدد من المحاولات (المحدد بـ 16 محاولة في التجارب)، مستفيداً من رسائل خطأ خادم Lean لتنقيح محاولاته.
3. التكرار: تُضاف أزواج التخمينات والبراهين التي تم التحقق منها إلى المكتبة، والتي تعمل بدورها كسياق للتكرارات اللاحقة.

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

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

1. اقتراح المسار: تقديم CPL، وهو إطار يفصل بين توليد التخمين وتوليد الإثبات، مما يسمح باكتشاف براهين أطول وأكثر تعقيداً.
2. التعلم القائم على السياق للنماذج المغلقة: إثبات أن النماذج اللغوية الكبيرة المغلقة (تحديداً ChatGPT-o3) يمكنها تحسين قدراتها في الإثبات من خلال التعلم القائم على السياق من مخرجاتها التي تم التحقق منها سابقاً، مما يلغي الحاجة إلى تحديث المعلمات أو الضبط الدقيق.
3. التحقق النظري والتجريبي: يقدم العمل نموذجاً نظرياً يوضح أن CPL تزيد من احتمالية توليد نظريات صعبة الإثبات مقارنة بأطر التوليد المتزامن. وتجريبياً، تأكد أن CPL نجحت في إعادة اكتشاف نظرية محددة بمستوى بحثي لم يستطع الإطار المرجعي (Baseline) إيجادها.

النتائج التجريبية
قيم المؤلفون CPL مقابل إطار مرجعي يعتمد على الحلقة البسيطة (SL) باستخدام مفاهيم طوبولوجية (المجموعات شبه المفتوحة، والـ $\alpha$-مفتوحة، والـ preopenness) المعرفة داخل Mathlib ولكن لم تُدرج بعد في المكتبة. كان الهدف هو النظرية التي تنص على أن تقاطع مجموعتين من نوع $\alpha$-مفتوحة هو أيضاً $\alpha$-مفتوحة.

• معدل الاكتشاف: في 20 جولة تجريبية، اكتشفت CPL النظرية المستهدفة 5 مرات. وفي المقابل، فشل إطار SL، الذي ولد عدداً أكبر بكثير من النظريات في المتوسط (328 مقابل 106)، في توليد النظرية المستهدفة ولو لمرة واحدة. وقد أكد اختبار فيشر الدقيق أن هذا الفرق ذو دلالة إحصائية ($p = 0.024$).
• طول الإثبات: ولدت CPL نظريات ذات أطوال إثبات أكبر بكثير (من حيث عدد الأحرف) مقارنة بـ SL، مما يدعم الادعاء النظري بأن الإطار يوجه التركيز نحو البراهين الأكثر صعوبة.
• فعالية السياق:
  • إعادة الإثبات: عند إعادة إثبات النظريات المولدة، أدى توفير المكتبة كـ "سياق" إلى زيادة معدل النجاح من 91% إلى 99% ($p = 4 \times 10^{-35}$).
  • النظرية المستهدفة: عند محاولة إعادة إثبات النظرية المتعلقة بتقاطع المجموعات $\alpha$-مفتوحة، نجح المُثبِت 7 مرات من أصل 80 محاولة عندما تم توفير المكتبة المولدة كـ "سياق". وبدون المكتبة، فشل بنسبة 100%.
  • النموذج المرجعي باللغة الطبيعية: عندما سُئل ChatGPT-4o عن إثبات النظرية باللغة الطبيعية، فإنه غالباً ما قيم النظرية بأنها خاطئة أو قدم براهين غير صحيحة؛ بينما قيمها ChatGPT-o3 باستمرار بأنها خاطئة، مما يشير إلى أن النظرية كانت خارج المعرفة المسبقة للنماذج. وقد عُزي النجاح في لغة Lean 4 إلى التعلم القائم على السياق لاستراتيجيات الإثبات من المكتبة المولدة.

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