Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4

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

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

التدقيق الرقمي المزدوج

في هذه الورقة، يأخذ جونيه جي (Jun-ye Ji) من جامعة واشنطن خواروارزمية كانان-باسم — وهي وصفة ذكية لفرز المصفوفات الصحيحة — ويبني برهاناً مدققاً آلياً لها باستخدام أداة تسمى Lean 4. فكر في Lean 4 كأمين مكتبة آلي صارم للغاية، يرفض قبول أي برهان رياضي ما لم تكن كل خطوة فيه سليمة منطقياً. إذا حاولت التسلل بكلمة "ربما" أو "من المحتمل أن يعمل"، سيغلق الروبوت الباب في وجهك. لم يكتفِ "جي" بكتابة الكود فحسب؛ بل أجبر الروبوت على التحقق من أن الكود ينتهي دائماً، ولا يتعطل أبداً، وينتج الإجابة الصحيحة تماماً في كل مرة.

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

رقصة "المحور" وتقليص الأرقام

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

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

حساب التكلفة: "الأثر" (The Trace)

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

لقد أثبتوا أن التكلفة الإجمالية لهذا الإيصال تنمو بمعدل متعدد الحدود (polynomial rate). وباللغة البسيطة، هذا يعني أنه حتى لو أصبحت المصفوفة المدخلة ضخمة جداً، فإن الوقت الذي يستغرقه حلها لن ينفجر إلى اللانهاية؛ بل سينمو بطريقة يمكن التنبؤ بها والسيطرة عليها. حتى أنهم حسبوا "الدرجة" المحددة لهذا النمو. تكشف الورقة أن التكلفة محكومة بمتعدد حدود درجته 2,150,687 (للعمل المنجز) و 98,990 (لحجم المخرجات).

الآن، تبدو تلك الأرقام مرعبة للغاية، لكن المؤلفين حذرون جداً في شرح ما يعنيه ذلك. هذه ليست أسُس "حادة" (مثل القول إنها تستغرق بالضبط $n^2$ من الخطوات)؛ بل هي شهود تحفظية (conservative witnesses). فكر فيها كهامش أمان. إذا كنت تبني جسراً، فقد تحسب أنه يجب أن يتحمل 100 طن، لكنك تصممه ليتحمل 1,000 طن لمجرد الأمان. هذه الأرقام الضخمة هي الـ "1,000 طن" في عالم الرياضيات — ضمانات بأن الخوارزمية آمنة وفعالة، حتى لو كان الأداء في العالم الحقيقي أفضل بكثير.

ما الذي تم استبعاده؟

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

الحكم النهائي

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

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