نموذج أسترا يحل عشر مسائل رياضية مفتوحة: ماذا يعني الذكاء الاصطناعي القابل للتحقق لعملك؟

نموذج أسترا من OpenAI يحل عشر مسائل رياضية مفتوحة — والخبر الحقيقي ليس الرياضيات

باختصار: في الأول من أغسطس 2026 أعلنت OpenAI أن نسخة داخلية من نموذجها القادم «أسترا» (Astra) توصلت إلى نتائج جديدة في عشر مسائل مفتوحة في الرياضيات وعلوم الحاسب النظرية، ظلت كل واحدة منها بلا حل عقدا على الأقل. والأهم من الحل نفسه أن كل نتيجة نُشرت مصحوبة بشهادة إثبات قابلة للفحص آليا بلغة Lean 4 على غيت هب، إلى جانب مخطوطة من 249 صفحة، وبتكلفة حوسبية إجمالية قاربت 2000 دولار فقط. الدرس هنا لصاحب العمل ليس في نظرية الزمر ولا في حزم الكرات، بل في مبدأ واحد: الذكاء الاصطناعي الذي يسلمك مخرجا قابلا للتحقق آليا يختلف جوهريا عن الذي يسلمك نصا مقنعا فحسب.

ما الذي أُعلن بالضبط؟

أبرز النتائج المعلنة هي أول بناء صريح لما يسمى «زمرة غير سوفية» (non-sofic group)، وهو سؤال ظل مفتوحا منذ أن طرح ميخائيل غروموف مفهوم السوفية عام 1999. ومعه نتائج أخرى تشمل نقض فرضية الصلابة لكونيس في جبور فون نيومان، وإثبات فرضية إيرهارت للحجوم، وحل ثلاث مسائل من قائمة بول إيردوش — من بينها المسألة 183 المتعلقة بأعداد رامزي متعددة الألوان — إضافة إلى تحسين حد أعلى في كثافة حزم الكرات عالية الأبعاد، وهو تحسين يُقال إنه الأول من نوعه منذ 1978.

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

القيمة ليست في أن النموذج ادعى نتيجة، بل في أنه سلّم معها آلة تتحقق من الادعاء نيابة عنك.

الجانب الآخر: انتقادات جدية لا يصح تجاهلها

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

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

الترجمة العملية لصاحب عمل سعودي

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

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

أكثر مشاريع الذكاء الاصطناعي فشلا في الشركات هي التي تعامل النوع الثاني كما لو كان النوع الأول. والعكس صحيح أيضا: كثير من الفرص الرابحة ضائعة لأن الشركة لم تنتبه أن عملية ما لديها تقبل التحقق الآلي فعلا لو صُممت بشكل صحيح.

كيف تبني «طبقة تحقق» داخل شركتك

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

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

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

ثلاث خلاصات تحملها معك

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

كيف نبنيه في أوريجامي

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

المصادر

• الإعلان الرسمي من OpenAI: openai.com
• تغطية The Next Web للإعلان وتفاصيل الزمر غير السوفية: thenextweb.com
• تغطية SiliconANGLE ونشر البراهين: siliconangle.com
• الهيئة السعودية للبيانات والذكاء الاصطناعي — نظام حماية البيانات الشخصية: sdaia.gov.sa