⚛️ الفيزياء الكمومية

Discovering formally verified quantum programs with AI

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

المؤلف الأصلي: Sergey Shirobokov, Ben Jaderberg, Katerina Hristova, George Tsoukalas, Johannes Bausch, Eric Wieser, Francisco J. H. Heras, Nicholas C. Rubin, Guang Hao Low, Sébastien Racanière, Nenad Tomašev, Lei M.

نُشر 2026-11-09

📖 3 دقيقة قراءة🧠 قراءة متعمّقة

CC BY 4.0

المؤلف الأصلي: Sergey Shirobokov, Ben Jaderberg, Katerina Hristova, George Tsoukalas, Johannes Bausch, Eric Wieser, Francisco J. H. Heras, Nicholas C. Rubin, Guang Hao Low, Sébastien Racanière, Nenad Tomašev, Lei M. Zhang, James Watson, Tanuj Khattar, Aws Albarghouthi, Stavan Jain, Harun Khan, Leopoldo Sarra, Andrew W. Senior, Michael Broughton, Hussain Masoom, Sergio Boixo, Ryan Babbush, Swarat Chaudhuri, Pushmeet Kohli

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلف ولم يصادق عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

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

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

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

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

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

ملخص تقني: اكتشاف برامج كمومية مُتحقق منها رسميًا باستخدام الذكاء الاصطناعي

بيان المشكلة

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

المنهجية

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

1. مكتبة التحقق الرسمي

جوهر النظام هو مكتبة تعتمد على منطق هور (Hoare Logic) الكمومي (QHL). وهي تقوم بصياغة ما يلي رسميًا:

الحالات الكلاسيكية-الكمومية: دمج التدفق الكلاسيكي للتحكم مع الحالات الكمومية.
الصحة: يتم التعبير عنها عبر ثلاثيات هور (الشرط المسبق، البرنامج، الشرط اللاحق)، ويتم التحقق منها عبر حساب الشرط المسبق الأضعف.
عدّ الموارد: حدود رسمية للتكاليف المتوقعة والأسوأ في أسوأ الحالات، وتستهدف تحديدًا تكلفة الزمكان ( $Q \cdot T$ )، والتي تُعرف بعدد الكيوبتات المنطقية ( $Q$ ) مضروبًا في عدد بوابات $T$ ( $T$ ). هذا المقياس بالغ الأهمية في البنى التحتية المقاومة للأخطاء حيث تشكل عملية تقطير بوابة $T$ العبء الأكبر.

2. بنية الاكتشاف متعددة الوكلاء

يحدد الباحثون مواصفات المشكلة في Lean، حيث يتم ذكر مبرهنة الصحة المستهدفة وحدود التكلفة مع وضع علامات (sorry) مكان الحل.

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

المساهمات الرئيسية

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

النتائج

طُبق سير العمل على خمس مشكلات متميزة، مما أدى إلى تخفيضات كبيرة في الموارد مقارنة بأقوى النماذج المرجعية المنشورة:

المشكلة	مجال التطبيق	التكلفة المرجعية ( $Q \cdot T$ )	تكلفة هذا العمل ( $Q \cdot T$ )	التحسن
بحث غروفر المتوازي	البحث غير المهيكل	البروتوكولات المنشورة الأقوى	دوائر متحقق منها	ما يصل إلى 1.41× خفض في جولات الأوراكل المتوقعة
أقواس arcsin ذات النقطة الثابتة	تحضير الحالة	$> 1.08 \times 10^8$	$3.70 \times 10^5$	290× خفض
قدرة إيقاف جسيمات ألفا	حصر الاندماج الحراري	$5.42 \times 10^{15}$	$4.98 \times 10^{14}$	10.9× خفض
ديناميكيات غير بورن-أوبنهايمر	الكيمياء الضوئية ( $C_{23}H_{20}N_3O$ )	$4.98 \times 10^{15}$	$6.16 \times 10^{14}$	8.08× خفض
مركب سيتوكروم P450	استقلاب الأدوية	$1.09 \times 10^{12}$	$4.37 \times 10^{11}$	2.49× خفض

تحسينات خوارزمية محددة

arcsin: قام الوكلاء أولًا بالتحسين باستخدام مجموعة بوابات "kickmix" مقيدة (يمكن التحقق منها عبر الفحص العشوائي الكلاسيكي) ثم رفعوا الحل إلى مجموعة Clifford+ $T$ الكاملة باستخدام التحقق الرسمي، حيث اكتشفوا آلية للبحث عن المعاملات قللت من عدد بوابات $T$ بنسبة 33%.
قدرة الإيقاف (Stopping Power): استخدم الحل تمثيل شبكة الفضاء الحقيقي لاستغلال مبدأ استبعاد باولي، مما قلل من معيار $\lambda$ للتركيب الخطي للوحدات (LCU). كما قدم تقنية لإعادة استخدام سجل الزخم الإلكتروني الكلي بين خطوات المشي، مما قلل عدد بوابات $T$ لكل خطوة بنسبة 10%.
ديناميكيات غير بورن-أوبنهايمر: شملت التحسينات إلغاء الحساب القائم على القياس لتحميل الإحداثيات، وتقريب جهود $1/r$ عبر كثيرات حدود برنشتاين (لتجنب الضرب المكلف)، واستخدام المنطق العكسي للشحنات النووية بدلًا من أخذ عينات التزييف (alias sampling).
سيتوكروم P450: استبدل الحل عمليات البحث عن الزوايا الثنائية بسجل "واحد-ساخن" (one-hot) لمتجهات المدارات، مما قلل بشكل كبير من تكلفة بوابات $T$ لتحضير الحالة وتطبيق الدوران.

الأهمية والادعاءات

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

تتجاوز المحاكاة الكلاسيكية: قادرة على معالجة مشكلات تتطلب آلاف الكيوبتات و $10^9$ إلى $10^{15}$ عملية منطقية، وهي مجالات يستحيل فيها الاختبار العددي الكلاسيكي.
متحقق منها بدقة: تأتي كل نتيجة مع برهان آلي الصحة والتكلفة، مما يضمن الموثوقية دون الحاجة إلى أجهزة مقاومة للأخطاء لاختبار الخوارزميات.
تعاونية: يوضح نظام الوكلاء المتعددين أن التعاون بين الفرق (عبر الويكي والمؤتمرات) أمر ضروري، حيث تظهر أفضل الحلول غالبًا من خلال تركيب الأفكار عبر فرق متعددة.

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