Revisiting Incremental Linearization for Nonlinear Integer Arithmetic

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

في معظم الأوقات، تكون هذه الألغاز سهلة لأنها تتضمن فقط خطوطاً مستقيمة وعمليات جمع بسيطة (مثل $x + y = 5$). الحواسيب مذهلة في هذه الأمور. لكن الحياة تصبح فوضوية عندما تقدم الحسابات غير الخطية — قواعد حيث تُضرب الأشياء في بعضها أو تُرفع لقوى (مثل $x \times y$ أو $x^3$). فجأة، تصبح القواعد منحنية وملتوية، وتصبح الرياضيات صعبة الحل بشكل هائل. في الواقع، بالنسبة للأعداد الصحيحة، من المستح المستحيل رياضياً ابتكار طريقة كاملة بنسبة 100% تحل كل هذه الألغاز. ولهذا السبب، يبني علماء الحاسوب "محققين جيدين بما يكفي" يستخدمون طرقاً مختصرة ذكية لإيجاد الإجابات، حتى لو لم يتمكنوا من الوعد بحل كل حالة مستحيلة.

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

الطريقة القديمة: التخمين باستخدام الدوال غير المفسرة

لفهم الترقية، دعنا نرى كيف كان يعمل المحققون السابقون. تخيل أن لديك صندوقاً غامضاً يحمل ملصق $f(x, y)$. أنت لا تعرف ما بداخله، لكنك تعلم أنك إذا وضعت نفس الأرقام، فستحصل على نفس الرقم في الخارج. الطريقة القديمة كانت تعامل كل عملية ضرب، مثل $x \times y$، كأنها هذا الصندوق الغامض. كان الحاسوب يخمن قيمة للصندوق، ويتحقق مما إذا كانت منطقية، وإذا لم تكن كذلك، فإنه يضيف قاعدة لتصحيح التخمين.

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

الحيلة الجديدة: إحكام الشبكة باستخدام القواطع (Secants)

قرر مؤلفو هذه الورقة التوقف عن معاملة هذه القوى كصناديق غامضة ومعاملتها بدلاً من ذلك كـ ثوابت جديدة — مجرد أرقام بسيطة تمثل نتيجة القوة. لكن السحر الحقيقي يكمن في القواعد الجديدة التي أضافوها للتحقق من هذه الأرقام.

لقد اكتشفوا أنه لأي عدد صحيح، وليكن $v$، فإن الدالة $x^k$ (مثل $x^3$) تسلك سلوكاً يمكن التنبؤ به جداً بين $v$ و $v+1$. لقد أنشأوا مجموعة جديدة من القواعد تعتمد على خطوط القاطع (secant lines). تخيل منحنى على رسم بياني. خط القاطع هو خط مستقيم يصل بين نقطتين على هذا المنحنى. أدرك المؤلفون أنه إذا رسمت خطاً مستقيماً بين النقطة $(v, v^k)$ والنقطة الصحيحة التالية، فإن هذا الخط سيخلق "سياجاً" ضيقاً جداً حول المنحنى.

إليك التشبيه:

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

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

تحدي "مجموع ثلاثة مكعبات"

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

على سبيل المثال، قد يكون اللغز: $x^3 + y^3 + z^3 = 79$.

هذا الكابوس بالنسبة للمحللات القياسية. يمكن أن تكون الأرقام ضخمة، والعلاقات معقدة. اختبر المؤلفون محللهم الجديد، qfn2l، مقابل أفضل المحللات الموجودة (مثل Z3 و cvc5 و MathSAT).

• حاولت المحللات الأخرى حل لغز $x^3 + y^3 + z^3 = 79$ لكنها استسلمت بعد 3 دقائق (انتهى الوقت المخصص لها).
• وجد المحلل الجديد، qfn2l، الإجابة — $x = -19, y = 35, z = -33$ — في غض[ن] 20 ثانية فقط.

النتائج: منافس جديد قوي

قام الباحثون بتشغيل محللهم على مجموعة ضخمة مكونة من 25,444 لغزاً من مكتبة قياسية تسمى SMT-LIB. إليكم ما وجدوه:

1. الأداء العام: المحلل الجديد ينافس أفضل الأدوات الموجودة. لقد حل حوالي 14,000 لغز في المجمل، وهو رقم قريب من الأداء العالي، رغم أنه لم يتفوق على الأفضل على الإطلاق (مثل Z3) في كل نوع من أنواع الألغاز.
2. نقطة القوة: يتألق المحلل الجديد بوضوح في الألغاز التي تهيمن عليها القوى والمنتجات المختلطة. في عائلة "MathProblems" (التي تتضمن مجموع المكعبات)، حل حوالي 53% من الحالات (585 إلى 587 من أصل 1,100). عانت المحللات الأخرى بشكل كبير مع هذه الأنواع المحددة من المشكلات.
3. المقايضة: اختبر المؤلفون نسخة من محللهم تحاول أن تكون حذرة للغاية بشأن التحقق مما إذا كانت الأجزاء المختلفة من اللغز متسقة (ما يسمى "بديهيات التطابق" أو congruence axioms). وجدوا أن هذا التحقق الإضافي أبطأ المحلل في الألغاز العامة، حيث حل حوالي 1,600 حالة أقل في المجمل. وهذا يشير إلى أنه بالنسبة لمعظم المشكلات، فإن الأسوار الضيقة (حدود القاطع) كافية، ولا تحتاج إلى العمل الشاق الإضافي للتحقق من كل قاعدة اتساق فردية.

لماذا هذا مهم؟

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

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

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