Verified Pauli-Product Measurement Compilation for Fault-Tolerant Quantum Computation

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

تعتمد الطريقة القياسية للعديد من هذه الآلات المستقبلية على تقنية تسمى "جراحة الشبكة" (lattice surgery). تخيل قطعة كبيرة من القماش تمثل ذاكرة الحاسوب. لتنفيذ عملية حسابية، لا تكتفي بمجرد قلب مفتاح، بل تقوم بخياطة قطع من هذا القماش معاً وفصلها بنماط دقيقة. هذه الغرز ليست خيوطاً مادية، بل هي قياسات مشتركة لمجموعات من الجسيمات. يقوم الحاسوب بقياس كيفية ارتباط هذه المجموعات ببعضها البعض، ويسجل النتيجة كبت بسيط من البيانات، ثم يستخدم تلك البيانات لتقرير ما يجب فعله بعد ذلك. هذه العملية، المعروفة باسم "قياس ناتج باولي" (Pauli-product measurement)، هي اللغة الأساسية لهذه الآلات المستقبلية. تكمن المشكلة في أن أدوات البرمجيات المستخدمة لترجمة الخوارزميات المصممة بشرياً إلى هذه اللغة لم يتم التحقق منها. فإذا ارتكب المترجم (compiler) خطأً أثناء الترجمة، فقد تفشل العملية الحسابية بأكملها، ونظراً لتعقيد العملية، يصعب معرفة مكان وقوع الخطأ.

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

ركز الباحثون على مهمتين رئيسيتين: "التنزيل" (lowering) و"التحسين" (optimization). التنزيل هو عملية أخذ بوابة كمومية قياسية، مثل عملية دوران أو بوابة منطقية، وتفكيكها إلى تسلسل من القياسات والتصحيحات المطلوبة من عتاد جراحة الشبكة. أما التحسين فيتضمن إعادة ترتيب هذه القياسات لجعل العملية أسرع وأكثر كفاءة. وفي عملهم، أثبتوا أن المترجم الخاص بهم يمكنه أخذ دائرة، وترجمتها إلى تعليمات قياس، ثم تطبيق قواعد لدمج وإعادة ترتيب تلك التعليمات دون تغيير النتيجة النهائية. كما تحققوا من أن المترجم يتعامل بشكل صحيح مع "الحالات السحرية" (magic states)، وهي موارد خاصة مطلوبة لأداء أنواع معينة من الحسابات، وأنه يبقي نتائج القياس الخاصة مخفية عن العالم الخارجي بينما يضمن بقاء النتائج العامة متاحة.

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

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

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