PSI: نموذج غير منشور من أنثروبيك يبرهن حدسية كمّية عمرها 18 عاماً

الملخص

• تقول شركة PSI إن نظامها البحثي، بنموذج غير منشور من أنثروبيك، برهن حدسية آرونسون-أمبينيس في الحوسبة الكمّية.
• البرهان اكتمل في اليوم الثالث من التشغيل، وقبله مدقّق البراهين الآلي Lean قبل تحسينه مرتين.
• الذكاء الاصطناعي ينتقل من المساعدة في الرياضيات إلى برهان كامل يُفحص آلياً، ومطابقة الصياغة تنتظر مراجعة بشرية.

خبر

وجد نظام بحثي داخلي لدى شركة فيزيكال سوبرإنتليجنس، بحسب إعلانها، برهاناً لحدسية آرونسون-أمبينيس المفتوحة منذ 2008، مستخدماً نسخاً من نموذج غير منشور من أنثروبيك. اكتمل البرهان في اليوم الثالث من التشغيل وقبله مدقّق البراهين Lean. ثم حسّن النظام النتيجة مرتين، ونشرت الشركة الصياغة الرسمية والشيفرة علناً لمن يريد إعادة الفحص.

تفصيل

• الإعلان: أعلنت الشركة، المعروفة اختصاراً بـPSI، النتيجة في 6 نوفمبر 2026، ونشرت صفحة بحث وورقة ومستودعاً على غيت هاب برخصة Apache 2.0. ولم تسمِّ النموذج الذي شغّله نظامها، واكتفت بوصفه نموذجاً غير منشور من أنثروبيك يعمل بنسخ متعددة على بنيتها.
• الحدسية: وضع سكوت آرونسون وأندريس أمبينيس الحدسية في 2008، وهي تتصل بسؤال: هل يتفوق الحاسوب الكمّي تفوقاً أُسّياً على مدخلات عشوائية بلا بنية؟ وأثبت الباحثان أن صحة عبارة عن كثيرات الحدود منخفضة الدرجة تعني أن الجواب لا، فبقيت العبارة مفتوحة 18 عاماً.
• المسار: أنتج النظام برهاناً كاملاً في اليوم الثالث من التشغيل على بنية الشركة، وقبله Lean. ثم كلّفته الشركة بمسائل مفتوحة مرتبطة بالنتيجة، فحسّنها مرتين قبل أن يقبل Lean النسخة النهائية. ولم تعلن الشركة المدة الكلية للتشغيل ولا كلفته ولا حجم التوجيه البشري.
• التحقق الآلي: الصياغة بلغة Lean 4 منشورة بإصدار 4.33.0 مع مكتبة Mathlib، ولم يجد تدقيق مسجّل فيها مواضع برهان مؤجلة ولا مسلّمات مضافة، إذ تعتمد النظريات النهائية الأربع ثلاث مسلّمات قياسية فقط. وأُعيد تشغيل التعريفات عبر نواة Lean وعبر lean4lean، وهو مدقّق أنواع مستقل.
• اختبار المدقّق: في تشغيل معزول قبلت أداة مقارنة تستخدم نواتين مختلفتين، هما nanoda ونواة Lean، النظريات النهائية الأربع. وعلى جهاز ثانٍ اختُبرت الأداة نفسها بحلول معروفة النتيجة، فقبلت حلاً صغيراً صحيحاً ورفضت أربعة حلول خاطئة وُضعت عمداً.
• ما بقي بشرياً: الورقة نفسها غير مدقّقة آلياً، ومطابقة الصياغة الرسمية للحدسية كما طُبعت في الأصل تحتاج قراءة بشرية. فبرهان Lean يثبت ما تقوله صياغته الرسمية فقط، وأي فرق دقيق بينها وبين نص الحدسية يجعله جواباً عن سؤال آخر.
• الفريق: طوّر ديفيد تورتوريان من فريق PSI النظام وشغّله وحدد المسألة ووجّه النموذج وراجع المسودة الأولى، وهو المسؤول عن صحة الورقة. ودقّق جيم هالفرسون البرهان، وعلّقت فيالا شاناهان على الصياغة الرسمية. ويتبع البرهان خطة وضعها شاشار لوفيت وجيابنغ تشانغ، مستبدلاً متباينة افترضاها بمتباينة جديدة مبرهنة.
• تقييم ستانفورد: يقرأ أربعة باحثين من ستانفورد، قدّموا في أغسطس 2026 ورقة عن أثر الحدسية في المحاكاة الكلاسيكية للخوارزميات الكمّية المتوازية، البرهان الكامل ويعدّون عرضاً أقصر له. وقالوا في تقييم نشرته الشركة: "هذه نتيجة ضخمة، إنها تحسم حدسية عمرها عقود".
• سجل سابق: ليست هذه أول نتيجة تعلنها الشركة بهذا الأسلوب، ففي 23 أكتوبر 2026 نشرت نتائج في خمس مسائل مفتوحة في نظرية المعلومات الكمّية، أرفقت بكل منها ورقة وصياغة Lean وشيفرة تحقق، وقالت إن باحثيها وجّهوا العمل المدعوم بالذكاء الاصطناعي وراجعوه.

المصدر: فيزيكال سوبرإنتليجنس