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

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

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

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

نظم المؤلفون ثلاثة اتجاهات رئيسية لتطور المجال:

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

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

لماذا هذا لا يزال ليس علماً

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

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

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

"يتطلب الاختراق التالي في AI4Math تحولاً حاسماً من حلالات المسائل

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

ما يجب أن يكون عليه النظام التالي

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

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

ماذا يعني هذا

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