تتطور نماذج اللغات الضخمة (Large Language Models) بشكل متزايد في مجال الاستدلال الرياضي، لكن مشكلتين رئيسيتين تظل تعاني منها هذه الأنظمة؛ الأولى تتمثل في عدم موثوقية الإثباتات التي تولدها، والثانية في صعوبة التحقق منها. لطالما كانت أدوات التأكيد التفاعلي مثل Lean 4 رائدة في معالجة هذه المشكلات من خلال قبول الإثباتات المراجعة فقط، مما يضمن دقة النتائج.

ومع ذلك، فإن مدى هذه الأدوات محدود بالمعرفة المعتمدة المتوفرة، مما يمثل تحديًا خصوصًا في بعض المجالات المتخصصة. في هذا السياق، يظهر Mathlib، وهو مستودع للإثباتات الرياضية النظامية ضمن Lean 4، كحل لكنه يظل غير كافٍ في بعض المجالات المحددة، مثل مادة الرياضيات المعروفة بـ Combinatorics on Words (CoW).

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

في دراسة شاملة شملت 90 نظرية رياضية ضمن 8 مجالات و3 مستويات من الصعوبة، حققت LAMP معدل نجاح مذهل يبلغ 96.7% في إثبات النظريات، متجاوزةً بذلك المعايير السابقة والأدوات الخاصة الأخرى. كما أظهر تحليل تجريبي أن إزالة الهيكل المعتمد على الأدوات أو فصل المخطط والبناء يكلفان نحو 12 نقطة مئوية من الأداء، حتى مع بقاء نموذج العظام ثابتًا.

تفتح هذه التطورات الجديدة آفاقاً جديدة في عالم الرياضيات والذكاء الاصطناعي. كيف يمكن تحسين هذه الأدوات لتدعيم التطبيقات المستقبلية في مجالات أوسع؟

ما رأيكم في هذا التطور؟ شاركونا في التعليقات.