جامعة إلينوي تجمع 12 151 مسألة مفتوحة وتختبر قدرة الذكاء الاصطناعي على حلّها

أصدر فريق من جامعة إلينوي في أوربانا-شامبين مشروع OpenFrontiers، وهو فهرس يضم 12 151 مسألة علمية مفتوحة، إضافة إلى اختبار من 200 مسألة رياضية. ويجيب الاختبار عن سؤال بسيط: هل يستطيع وكيل الذكاء الاصطناعي أن يعيد اكتشاف حل صار معروفًا للعلم للتو؟ يرى الوكيل المسائل بالصيغة التي طُرحت بها قبل حلّها. ولا يراجع الإجابة إنسان، بل برنامج تحقق. والنتيجة مخيّبة لأنصار فكرة أن «الذكاء الاصطناعي يدفع العلم إلى الأمام فعلًا»: ففي وضع عدم الاتصال بالإنترنت، بلغ أفضل نتيجة 7 مسائل محلولة من أصل 40.

خريطة غير المحلول: ما الذي يحتويه الفهرس

كانت المسائل المفتوحة حتى الآن موزعة بين قوائم المؤتمرات وصفحات الجوائز والمدونات وأقسام المقالات المرجعية. ولكل مصدر قواعده الخاصة: كيف تُصاغ المسائل، وكيف يوسَم وضعها، وبأي ترخيص تُحفظ. وقد وحّد المؤلفون 71 مصدرًا في مخطط واحد، قدّم 62 منها نصوص المسائل نفسها. أما 4 751 سجلًا إضافيًا فبقيت في الفهرس بوصفها مؤشرات فقط، أي روابط دون نصوص.

محتوى المدوّنة:

• 11 349 سجلًا (93,4%) في الرياضيات. ثم الفيزياء (339) وعلوم الحاسوب (285) وتعلّم الآلة (70). • أكثر المسائل في نظرية الأعداد (2 867) وفي الهندسة والطوبولوجيا (2 371). • أكبر المصادر: TheoremDB (3 909)، وقوائم المعهد الأمريكي للرياضيات (3 470)، ومشروع Formal Conjectures (459). • 65,9% من السجلات لها رمز وفق تصنيف MSC 2020 المعتمد في الرياضيات. • الصياغة بلغة Lean 4 متوفرة لـ 1 946 سجلًا فقط، أي 16%. وLean لغة تُكتب بها البراهين بحيث يتحقق الحاسوب من كل خطوة فيها.

ولا يجمّل المؤلفون وضع المسائل. فقد وُسم وضع 46% من السجلات بأنه غير محدد، لأن المصدر لا يذكر ببساطة هل المسألة محلولة اليوم أم لا. ولم تُحذف النسخ المكررة كي لا تُعاد كتابة صياغات الآخرين.

كيف صُمم الاختبار ولماذا لا يكفي «تاريخ القطع»

يتألف OpenFrontiers-Bench من جزأين. يضم Rediscovery-110 عدد 110 مسائل كانت مفتوحة قبل عام 2026 ثم وُجد لها حل. وتاريخ جميع أدلة الحلول لاحق لـ 5 يناير 2026. أما Open-90 فيضم 90 مسألة لا تزال دون حل. وتتوفر لـ 85 من المسائل المحلولة براهين موثّقة بلغة Lean أو شهادة نهائية دقيقة، مثل مثال مضاد أُعيد حسابه بحساب دقيق.

ولكل مسألة من المسائل الـ 200 صياغة بلغة Lean 4 (الإصدار 4.33.1، ومكتبة Mathlib). أُخذت 93 صياغة حرفيًا من Formal Conjectures، وعُدّلت 47، وكُتبت 60 من الصفر. وراجع كل صياغة مراجعان: قارنها الأول بالنص الأصلي للمسألة، وحاول الثاني إفساد معناها. والمراجعان كلاهما نموذجان لغويان، وليسا رياضيين بشريين. ولم تبقَ ملاحظات حرجة، وفي 23 مسألة لم تُسفر المراجعتان إلا عن ملاحظات طفيفة.

وظهرت أثناء الإعداد تفصيلة غير مريحة: ففي 55 من أصل 110 حلولًا، ينسب مؤلفو المصادر الرياضيات الأساسية إلى أنظمة ذكاء اصطناعي. وإذا كان نموذج من «السلالة» نفسها قد ولّد الحل، فلا يصح الحديث عن إعادة اكتشاف. لذلك لا يكفي تاريخ القطع وحده: فالبروتوكول يستبعد هذه المسائل لكل نموذج على حدة. وجُعل الوضع الرئيسي closed-book، أي العمل دون الوصول إلى الشبكة.

ماذا أظهر الوكلاء السبعة

شُغّل الوكلاء على HQ-50، وهي 50 مسألة اختيرت بحسب الجودة، منها 40 مسألة محلولة. وكانت الظروف ثلاثة: دون إنترنت، ومع نسخة مجمّدة من البحث، ومع الويب المباشر. ولم يُحتسب إلا البرهان بلغة Lean الذي قبله برنامجا تحقق مستقلان في بيئة معزولة (sandbox).

• دون إنترنت، حلّ الوكلاء من 0 إلى 7 مسائل من أصل 40. وهي في الغالب ثلاث مسائل حلّها البشر ببنية قصيرة. • مع الويب المباشر، كان أفضل نتيجة 27 مسألة. وفي معظم الحالات كان الوكيل يعثر أولًا على حل منشور. • لم يحل أحد أي مسألة مفتوحة حقًا دون العثور على حل جاهز. • كثيرًا ما يستسلم الوكلاء الأقوياء دون أن يستنفدوا ميزانية الوقت إذا كانت المسألة صعبة جدًا.

ماذا يعني ذلك

لم تعد المقاييس من نوع الأولمبيادات والامتحانات ذات الإجابة المعروفة سلفًا تفرّق بين البحث الحقيقي والبحث الجيد في الإنترنت. ويبيّن OpenFrontiers كيف يمكن الفصل بينهما: منع الشبكة، وطرح المسألة بصياغتها الأصلية السابقة للحل، وقبول النتيجة المتحقق منها شكليًا فقط. وهذا مرشّح مفيد للمختبرات والمستثمرين إزاء التصريحات الصاخبة عن «علماء الذكاء الاصطناعي». أما للباحثين فهو خريطة جاهزة لغير المحلول ومجموعة مسائل لا يمكن فيها تفسير النجاح بتسرّب من بيانات التدريب.

وثمة قيود أيضًا. فالاختبار رياضي بالكامل تقريبًا، وصياغات Lean متاحة لجزء صغير من المدوّنة. وتولّت النماذج نفسها التحقق من الصياغات، وإن كان ذلك في مرورين مستقلين. وقد نُشرت البيانات والاختبار على Hugging Face ضمن المجموعة FlippyDora/openfrontiers.