Astra من OpenAI: كيف حلّ نموذج غير منشور 10 مسائل رياضية مقابل 2,000 دولار

نموذج بلا موعد إطلاق يتفوق للتو على الرياضيين البشر

في 1 أغسطس 2026، أعلنت OpenAI أن نسخة داخلية غير منشورة من نموذجها القادم — الذي يحمل الاسم الرمزي Astra — حلّت 10 مسائل في الرياضيات وعلوم الحاسوب النظرية ظلّت مفتوحة لعقد كامل أو أكثر. وشملت المسائل نظرية المجموعات، وجبريات فون نويمان، والتوافقيات، وتعبئة الكرات في الأبعاد العالية، ونظرية الترميز، وتعقيد الدوائر الحسابية، والتكرار المتوازي الكمومي، والتشفير القائم على الشبكات، وفقًا لملخص SiliconANGLE للإعلان.

الرقم الأبرز صغير لكنه لافت: أنتج Astra البراهين العشرة مقابل نحو 2,000 دولار من الحوسبة بأسعار واجهة برمجة تطبيقات (API) GPT-5.6، بحسب تقرير SiliconANGLE. هذا الرقم مهم لأنه يعيد صياغة الإعلان من «مختبر أمضى أشهرًا في مغامرة محفوفة بالمخاطر» إلى «نموذج أنجز ذلك كمهمة جانبية بتكلفة حاسوب محمول».

لم تكن هذه أول ظهور لـAstra. ذكرت مجلة Forbes أن عائلة النماذج نفسها دحضت في مايو 2026 حدسية المسافة الواحدية لإردوش (Erdős) التي عمرها 80 عامًا — وهي نتيجة وصفها Thomas Bloom، القائم على كتالوج مسائل إردوش، بأنها «خبر كبير» آنذاك. وتحويل إعلان أغسطس عن عشرة براهين دفعة واحدة نتيجة معزولة إلى نمط متكرر.

هذا النمط يحمل تحفظًا يجب ذكره منذ البداية: سبق لـOpenAI أن بالغت في نتائج متعلقة بإردوش. ففي أكتوبر 2025، زعم نائب رئيس OpenAI Kevin Weil أن GPT-5 «وجد حلولًا لعشر (!) مسائل من مسائل إردوش لم تُحل سابقًا»، لكن Bloom — الرياضياتي نفسه الذي أشاد لاحقًا بنتيجة مايو 2026 — نفى علنًا هذا التوصيف، موضحًا أن المسائل الموسومة بـ«مفتوحة» على موقعه تعني فقط أنه شخصيًا لم يكن على علم بحل منشور لها، لا أنه لا يوجد حل من الأساس. فقد عثر GPT-5 على أدبيات موجودة لم يكن Bloom قد فهرسها، ولم يحل حدسيات غير محلولة فعلًا — وهو تمييز أشار إليه علنًا كلٌّ من Yann LeCun من Meta وDemis Hassabis من Google DeepMind في حينه، بحسب تقرير TechCrunch.

المجموعة غير السوفية: سؤال مفتوح منذ 27 عامًا

أبرز نتيجة في هذه المجموعة هي أول بناء صريح لدليل على وجود مجموعة غير سوفية — وهو مفهوم قدّمه عالم الرياضيات Mikhail Gromov عام 1999، وفقًا لـSiliconANGLE، ما يجعل السؤال الأساسي عمره 27 عامًا وقت صدور نتيجة Astra. المجموعات السوفية هي فئة من المجموعات اللانهائية التي يمكن تقريبها ببنى منتهية بمعنى تقني دقيق؛ وقد ظلّ السؤال عمّا إذا كانت كل مجموعة سوفية، أو ما إذا كانت المجموعات غير السوفية موجودة أصلًا، عصيًّا على الحل من قبل الرياضيين البشر لما يقارب ثلاثة عقود.

كما تناولت المجموعة حدسية الصلابة لكون (Connes) في جبريات فون نويمان، ومسائل قصوى في نظرية رامزي ونظرية الرسوم البيانية، ومسألة أقرب متجه في التشفير القائم على الشبكات — وهي افتراضية صعوبة أساسية تقوم عليها عدة مخططات تشفير لما بعد الحوسبة الكمومية. ولم تصل أي من هذه النتائج كتصريح بلغة سردية، بل كبرهان مُنسّق بالكامل بصيغة Lean 4.

صفر «sorry» — ماذا يعني «قابل للتحقق آليًا» فعليًا

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

وفقًا لـSiliconANGLE، عدد كلمات «sorry» عبر البراهين العشرة المُنسّقة هو صفر: لم تُترك أي خطوة، من بين البراهين العشرة، دون إثبات. ونشرت OpenAI ملفات الشهادات على GitHub بترخيص Apache 2.0، ما يعني أن أي باحث — دون حساب في OpenAI، ودون مفتاح API، ودون الحاجة لأي ثقة بادعاءات الشركة — يمكنه تحميل Lean وتشغيل الملفات ومشاهدة المدقق يؤكد كل خطوة بشكل مستقل.

هذه القابلية للتدقيق المستقل هي ما استقطب أقوى تزكية. فقد قال الحائز على ميدالية فيلدز Timothy Gowers إنه سيوصي بأحد البراهين لنشره في مجلة رياضية مرموقة دون تردد، بحسب تقرير Forbes حول الإعلان.

للمتشككين وجهة نظر أيضًا

لم تكن كل ردود الفعل احتفالية. فقد وصف عالم الإدراك وناقد الذكاء الاصطناعي Gary Marcus الإعلان بأنه «مذهل لكنه مبالغ فيه إلى حد كبير»، بحسب Forbes، مجادلًا بأن OpenAI اختارت بنفسها المسائل التي روّجت لها — وهي نجاحات مُنتقاة من مجموعة محاولات أوسع بكثير لم تُنشر — وأن الباحثين الخارجيين لا يمكنهم تشغيل النموذج بشكل مستقل لاختباره على مسائل جديدة من اختيارهم. وكلتا النقطتين تتعلقان ببنية الإعلان لا بالبراهين نفسها: فتحقق Lean يؤكد صحة النتائج العشر، لكنه لا يقول شيئًا عن معدل الفشل في المسائل التي لم تُدرج في الإعلان، ولا عن قدرات Astra خارج نطاق الرياضيات، لأنه لا أحد خارج OpenAI يملك وصولًا عمليًا إليه.

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

ما تكشفه هذه الحادثة عن مسار الذكاء الاصطناعي

الأهمية العملية هنا لا تتعلق كثيرًا بعشر نظريات محددة بقدر ما تتعلق بما تعنيه التكلفة وطريقة التحقق لمستقبل البحث المدعوم بالذكاء الاصطناعي.

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

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

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

ماذا يعني هذا لمؤسسات البحث التي تدرس الاكتشاف المدعوم بالذكاء الاصطناعي

1. اجعل التحقق الشكلي المعيار الجديد للادعاءات العلمية المولّدة بالذكاء الاصطناعي

أي نتيجة مدعومة بالذكاء الاصطناعي لا يمكن التحقق منها بشكل مستقل بأداة حتمية — Lean أو Coq أو Isabelle أو ما يعادلها — ينبغي التعامل معها كفرضية لا كنتيجة ثابتة. إعلان Astra مفيد بالضبط لأنه لم يطلب من أحد الثقة بـOpenAI؛ بل طلب تشغيل مدقق مجاني ومفتوح المصدر. وينبغي للمؤسسات التي تبني مسارات عمل بحثية داخلية قائمة على الذكاء الاصطناعي أن تتبنى الانضباط نفسه: ربط أي برهان أو منتج برمجي أو ادعاء بشأن مجموعة بيانات ناتج عن نموذج لغوي كبير بخطوة تحقق آلية قابلة للتدقيق من طرف ثالث قبل اعتباره أمرًا مسلّمًا به.

2. اعتبر ميزانية حوسبة البحث بالذكاء الاصطناعي بندًا هامشيًا لا مغامرة كبرى

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

3. الاستعداد لفجوة متنامية بين القدرة المتقدمة والوصول العام

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

4. افصل السردية التسويقية عن الادعاء القابل للدحض

نقد Gary Marcus — بشأن الانتقاء المواتي للمسائل واستحالة الاختبار الخارجي — تذكير بضرورة القراءة أبعد من الرقم الأبرز. فعند تقييم ادعاءات بحثية لأي مختبر ذكاء اصطناعي، ينبغي السؤال بدقة: كم عدد المحاولات التي فشلت، وهل النموذج أو نتائجه قابلة للاختبار بشكل مستقل، وهل طريقة التحقق نفسها موثوقة ومفتوحة. تحصل حالة Astra على تقييم جيد في السؤال الأخير وتقييم ضعيف في السؤالين الأولين، وكلا الاستنتاجين صحيح في آن واحد.

النمط الأوسع: أدوات البحث بالذكاء الاصطناعي تسبق الوصول إلى البحث بالذكاء الاصطناعي

تندرج براهين Astra ضمن نمط أوسع في عام 2026: إذ تتمحور إعلانات القدرات المتقدمة للذكاء الاصطناعي بشكل متزايد حول عروض ضيقة وقابلة للتحقق وذات مكانة رفيعة — برهان رياضي، أو معيار برمجي، أو فرضية علمية — بدلًا من إطلاقات منتجات استهلاكية واسعة. ولهذا التحول منطق تجاري: فتزكية حائز ميدالية فيلدز إشارة مصداقية أكثر ديمومة من عرض توضيحي لروبوت محادثة، وتكلفتها جزء يسير من ميزانية تدريب نموذج أساسي كامل. لكن هذا يعني أيضًا أن النقاش العام حول تقدّم الذكاء الاصطناعي يتشكّل بشكل متزايد من نتائج لا يستطيع الجمهور إعادة إنتاجها، وأدوات لا يستطيع استئجارها، ونماذج لا يستطيع استجوابها. ويمثّل تحقق Lean ضمانة حقيقية ودائمة على الادعاءات المحددة التي طُرحت في 1 أغسطس — فالبراهين العشرة صحيحة، هذا كل ما في الأمر. أما ما لا يمكن لهذا التحقق كشفه، فهو كل ما اختار الإعلان عدم عرضه.

الأسئلة الشائعة

المصادر والقراءات الإضافية

• OpenAI’s Astra solves 10 long-open math problems and publishes the proofs — SiliconANGLE
• OpenAI’s Astra Solved 10 Decades-Old Math Problems For $2,000 — Forbes
• OpenAI says it slowed Astra model development over security concerns — TechCrunch
• OpenAI’s embarrassing math (GPT-5 Erdős problems dispute) — TechCrunch