نماذج LLM تثبت النظريات لكنها لا تكتشف الرياضيات: باحثون يرسمون الخطوة التالية

نشرت مجموعة من الباحثين في مطلع يوليو 2026 على arXiv ورقة موقف تلخّص إنجازات أنظمة LLM المخصصة لإثبات النظريات، وتكشف حدّها الجوهري: الأنظمة الحالية تثبت النظريات لكنها لا تستطيع اكتشاف الرياضيات. كما اقترحت الورقة خارطة طريق استراتيجية للانتقال إلى وكلاء بحثيين متكاملين.

ما الذي تستطيع أنظمة AI4Math فعله اليوم

حققت أنظمة LLM الموجّهة للرياضيات الصورية خلال سنوات قليلة تقدماً ملموساً. فهي تعمل بلغات الإثبات التفاعلي للنظريات (ITP)، وفي مقدمتها Lean 4 وIsabelle وCoq، وقد تعلّمت توليد براهين صورية لمسائل محددة بدقة. تتيح هذه اللغات كتابة البراهين بطريقة تمكّن الحاسوب من التحقق آلياً من كل خطوة، وهو ما يجعل النتيجة أكثر موثوقية بكثير من البراهين المكتوبة بخط اليد.

وقد لخّص المؤلفون ثلاثة اتجاهات رئيسية لتطور المجال:

• مجموعات البيانات — تراكمت مدوّنات من المسائل المصاغة صورياً، من المستوى المدرسي حتى الجامعي، تتيح تدريب النماذج على أمثلة لبراهين صحيحة
• الصياغة الصورية الآلية — تحسّنت النماذج في ترجمة شروط المسائل المكتوبة بلغة طبيعية إلى صياغة ITP صارمة
• توليد البراهين — تجد الأنظمة براهين خطوة بخطوة بثقة متزايدة عند توفر صياغة أولية واضحة

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

لماذا لا يُعدّ هذا علماً بعد

يختلف العلم الرياضي الحقيقي جوهرياً عن حلّ مسائل الكتب المدرسية. فهو يتطلب القدرة على صياغة الفرضيات، والكشف عن روابط غير متوقعة بين مجالات مختلفة، ومهاجمة المسائل المفتوحة، وهي مسائل تمتد غالباً لسنوات ولا تكون صياغتها واضحة وتنطوي على عدة مستويات من التجريد. وهنا تحديداً تُظهر أنظمة LLM الحالية قيوداً منهجية.

يحدّد المؤلفون خمس مشكلات رئيسية:

• البيانات: لا تحتوي مجموعات البيانات على أمثلة لكيفية ولادة النظريات الجديدة، بل على حلول لمسائل طُرحت مسبقاً فقط
• البنية: تعتمد الرياضيات على تسلسلات هرمية معقدة من المفاهيم وعلى تبعيات ضمنية بين فروعها، ولا تستوعبها نماذج LLM جيداً
• البحث: تستطيع النماذج الإجابة عن الأسئلة، لكنها لا تستطيع صياغة أسئلة جديدة، وهذا ما يقوم عليه العلم
• الأدوات: لا يوجد تكامل مع أنظمة الجبر الحاسوبي وقواعد البيانات الرياضية المتخصصة
• التعاون: لا تستطيع النماذج أن تكون مؤلفاً مشاركاً حقيقياً، إذ لا تفهم السياق غير الرسمي الذي يتبادله العلماء فيما بينهم

«يتطلب الاختراق التالي في AI4Math تحولاً حاسماً من أنظمة تحلّ مسائل

محددة مسبقاً إلى وكلاء بحثيين قادرين على العمل في الصفوف الأمامية للرياضيات» — الفكرة المحورية للورقة.

كيف ينبغي أن يكون النظام التالي

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

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

ماذا يعني ذلك

تشير الورقة إلى تحول مهم في أفق مهام AI4Math: من أنظمة للتحقق من البراهين إلى أنظمة قادرة على المشاركة في اكتشاف رياضيات جديدة. ويتطلب هذا الانتقال بنية مختلفة جذرياً عن مجرد توسيع نطاق الأساليب القائمة. وإذا نُفّذت خارطة الطريق المقترحة، فقد تصبح الرياضيات من أوائل المجالات التي يظهر فيها الذكاء الاصطناعي شريكاً بحثياً حقيقياً للعالِم.