«أسترا» من OpenAI في مواجهة الرياضيات: 10 مسائل، وبراهين قابلة للتحقق آليًا

ما المسائل التي تناولها «أسترا»؟

تمتد النتائج عبر الهندسة عالية الأبعاد، ونظرية الترميز، وتعقيد الدوائر الحسابية، ونظرية الزمر، وجبر المؤثرات، والتعقيد الكمي، وتشفير الشبكات، والتوافقيات القصوى . وتشمل المسائل المعلنة:

1. تعبئة الكرات في الأبعاد العالية: الحصول على حدود علوية جديدة لكثافة تعبئة الكرات، وصولًا إلى حد كوهِن–إلكيس .
2. الرموز الثنائية والكروية: تحسين أُسّي للحدود الخاصة بأقصى حجم للرمز عند تحديد الحد الأدنى للمسافة .
3. الزمر غير السوفية: بناء صريح يثبت وجود زمر غير سوفيّة، وهي مسألة محورية مفتوحة في نظرية الزمر .
4. حدسية كونّ للصلابة: تقديم نقض لحدسية قديمة تتعلق بجبر فون نيومان .
5. تعقيد الدوائر الحسابية: إيجاد حدود دنيا جديدة لحساب المحدد الدائم، من بينها حد أدنى لصيغة حسابية من رتبة تقارب (n^4/\log n) .
6. التكرار المتوازي الكمي: إثبات مبرهنة للتكرار المتوازي الأُسّي في الألعاب الكمية العامة بين لاعبين .
7. مسألة أقرب متجه: إثبات صعوبة التقريب بعامل كثير الحدود، وهي نتيجة ذات صلة بأسس التشفير لما بعد عصر الحوسبة الكمية .
8. حدسية إيرهارت للحجم: تحديد أكبر حجم ممكن لجسم محدب يكون مركز ثقله نقطة الشبكة الداخلية الوحيدة فيه .
9. أعداد رامزي متعددة الألوان: اشتقاق حد أدنى فائق الأُسّ، بما يحسم مسألة إردوش رقم 183 .
10. حدسيات الأعداد القصوى: نتائج بشأن حدسيتي الانضغاط والانحلال، بما يحسم مسألتي إردوش رقمي 146 و180 .

لماذا يُعدّ التحقق عبر Lean مهمًا؟

لم تُصدر OpenAI نموذج «أسترا» نفسه، لكنها نشرت مخطوطًا من 249 صفحة وشهادات براهين Lean 4 على GitHub بموجب ترخيص Apache 2.0 . وتشير الشركة إلى أن المستودع لا يحتوي على أي استخدام لعبارة sorry، وهي عبارة تُستعمل في Lean لترك جزء من البرهان غير مكتمل؛ ووفق هذا الوصف، فإن الخطوات المضمّنة في البراهين العشرة مكتملة وقابلة للتحقق آليًا .

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

إشادة واسعة… وتحفظات جدية

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

ليست مسائل جائزة الألفية

أشار متابعون إلى أن المسائل العشر ليست من مسائل جائزة الألفية الشهيرة، مثل فرضية ريمان أو سؤال «هل P تساوي NP؟» . وهذا لا يجعلها مسائل هامشية؛ فبعضها ظل مفتوحًا لعقود، ومن بينها سؤال وجود الزمر غير السوفية، الذي يعود إلى طرح ميخائيل غروموف لمفهوم «السوفية» عام 1999 . لكن غياب مسائل جائزة الألفية يحد من بعض العناوين الإعلامية التي توحي بأن النموذج حل أصعب ألغاز الرياضيات المعروفة.

غياب التحكيم العلمي المسبق

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

هل تنتقل هذه القدرة إلى العلوم الأوسع؟

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

صعوبة إعادة التجربة

بما أن «أسترا» غير متاح للعامة، ولأن المنهج التفصيلي لصياغة الأوامر لم يُكشف بالكامل، لا يستطيع باحثون مستقلون إعادة تجربة مرحلة توليد الحلول نفسها . ويمكن فحص البراهين المنشورة، لكن لا يمكن حتى الآن تكرار المسار الذي قاد النموذج إلى تلك البراهين من دون الوصول إلى النموذج وإعداداته ومنهجيته.

توقيت الإعلان

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

ماذا يعني ذلك فعليًا؟

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

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

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