Program Synthesis for Non-Linear Real Arithmetic: Going Beyond Realizability

ملخص تقني: تخليق البرامج للحساب الحقيقي غير الخطي: ما وراء القابلية للتحقق

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

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

الصعوبة النظرية والقيود
وضع المؤلفون حدوداً نظرية هامة لهذه المشكلة:

1. التبادلية مع مسألة هيلبرت العاشرة: أثبتوا أن RPSQ قابلة للتبادل مع مسألة هيلبرت العاشرة على الأعداد النسبية ($HTP_{\mathbb{Q}}$). وبما أن $HT_Q$ هي مسألة مفتوحة منذ زمن طويل في نظرية الأعداد، فإن هذا يعني أن وجود خوارزمية تخليق عامة وصحيحة وكاملة لـ RPSQ أمر غير مرجح.
2. استحالة التخليق الخالي من الحلقات: تُظهر الورقة أن RPSQ لا يمكن حلها باستخدام برامج خالية من الحلقات فقط. فلو وُجد حل خالٍ من الحلقات، لكان ذلك يعني أن نظرية الحساب النسبي تقبل حذف المكممات، وهي نتيجة معروفة بأنها غير قابلة للتقرير (Robinson, 1959).

المنهجية والخوارزميات
نظراً لعدم القابلية للتقرير العامة، يقترح المؤلفون نهجاً متعدد المستويات:

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

2. خوارزمية صحيحة وكاملة للمخرج الواحد ($|Y|=1$): للمواصفات ذات متغير مخرج واحد، يقدم المؤلفون خوارزمية صحيحة وكاملة (Algorithm 1). يفصل هذا النهج المشكلة إلى حالتين:

   • المتباينات الصارمة: تستخدم عزل الجذور الحقيقية (RRI) لإيجاد الفترات التي يكون فيها إشارة كثيرات الحدود ثابتة. ومن خلال أخذ عينات من النقاط النسبية داخل هذه الفترات (استغلال كثافة الأعداد النسبية في الأعداد الحقيقية)، تجد الحلول للقيود الصارمة.
   • المتباينات غير الصارمة: بالنسبة للحلول الواقعة على الحدود (حيث تصبح المتباينات غير الصارمة مساواة)، تستخدم الخوارزمية نظرية الجذور النسبية (RRT). يسمح هذا بحصر مجموعة منتهية من الجذور النسبية المرشحة لمعادلات كثيرات الحدود المشتقة من شروط الحدود.
     تجمع الخوارزمية بين هذه الطرق وحذف المكممات (باستخدام QEPCAD) لتحديد أضعف الشروط المسبقة لوجود الحلول.

3. خوارزمية صحيحة ولكن غير كاملة للحالة العامة ($|Y|>1$): للمخرجات المتعددة، يقترح المؤلفون Algorithm 2 (المطبقة في الأداة NQSynth)، وهي إجراء صحيح ولكنه غير كامل يقوم بتفكيك مشكلة المخرجات المتعددة تكرارياً إلى مشكلات مخرج واحد:

   • تستعلم من أوراكل (Oracle) الخاص بـ NRA (وهو Z3) لإيجاد تعيين مرضٍ نسبي (Model).
   • تقوم بتثبيت جميع متغيرات المخرجات باستثناء واحد بناءً على هذا النموذج، مما يحول المشكلة إلى حالة تخليق مخرج واحد قابلة للحل بواسطة الخوارزمية الكاملة الموصوفة أعلاه.
   • تقوم ببناء قائمة قرار (سلسلة من فروع if-then-else) حيث يمثل كل فرع شرطاً مسبقاً مستخرجاً عبر حذف المكممات.
   • تتكرر العملية، مع تنقيح المواصفة عن طريق نفي الشروط المسبقة للحلول الموجودة، حتى تصبح المواصفة غير قابلة للتحقق أو يصل الوقت المحدد.

التنفيذ والنتائج التجريبية
قام المؤلفون بتنفيذ نهجهم في أداة نموذجية تسمى NQSynth. وقاموا بتقييمها مقابل نهجين منافسين:

• QEPCAD+CVC5: خط معالجة SyGuS معدل يقوم أولاً بحساب أضعف شرط مسبق على الأعداد الحقيقية ثم يخلق برنامجاً.
• ModEnum: نهج يعتمد على تعداد النماذج مستوحى من أعمال Monniaux حول الحساب الخطي.

استخدم التقييم مجموعتين من المعايير:

1. معايير NRA: 83 معياراً تم تكييفها من مستودع SMT-LIB 2024 (عائلات meti-tarski/Arthan, asin, zankl).
2. المعايير الهندسية: 51 مواصفة تمثل علاقات هندسية ثنائية وثلاثية الأبعاد (دوائر، مناطق حلقية، قطع زائد).

النتائج الرئيسية:

• حلت NQSynth 59 من أصل 83 من معايير NRA و33 من أصل 51 من المعايير الهندسية خلال مهلة 120 ثانية.
• في المقابل، حلت QEPCAD+CVC5 26 من معايير NRA و16 من المعايير الهندسية، بينما حلت ModEnum 23 من معايير NRA و11 من المعايير الهندسية.
• بشكل ملحوظ، نجحت NQSynth في تخليق برامج للعديد من المواصفات التي كانت غير قابلة للتحقق (أو حيث كان من الصعب حساب أضعف شرط مسبق)، وهو سيناريو تفشل فيه أدوات SyGuS تماماً.
• سلطت التجارب الضوء على أن العائق الأساسي لـ NQSynth كان خطوة حذف المكممات (QEPCAD)، خاصة للمدخلات الكبيرة، وليس منطق التخليق نفسه.

الأهمية والادعاءات
تدعي الورقة أنها تضيف تقنية جديدة إلى مجموعة تقنيات تخليق البرامج من مواصفات NRA. تكمن أهميتها الأساسية في:

1. التعامل مع عدم القابلية للتحقق: توفر طريقة عملية لتخليق برامج تتعامل بسلاسة مع المدخلات التي لا يوجد لها حل، وهي قدرة تفتقر إليها أدوات SyGuS الحديثة.
2. الدقة النسبية: من خلال استهداف المدخلات والمخرجات النسبية، تتجنب أخطاء التقريب المرتبطة بحسابات الفاصلة العائمة، مما يضمن الصحة الرياضية للتطبيقات التي تتطلب دقة عالية.
3. ما وراء SyGuS: يحل النهج مشكلات تتجاوز نطاق أدوات SyGuS الحالية، حتى بالنسبة للمواصفات القابلة للتحقق، وذلك من خلال الاستفادة من الخصائص نظرية الأعداد (RRT و RRI) بدلاً من الاعتماد فقط على البحث النحوي أو حذف المكممات القياسي.

يخلص المؤلفون إلى أنه بينما من غير المرجح نظرياً وجود حل كامل عام بسبب صعوبة $HTP_{\mathbb{Q}}$، فإن إجراءهم الصحي وغير الكامل يقدم حلاً عملياً قوياً يتفوق بشكل كبير على الأساليب الحالية في مجموعة واسعة من المعايير. ويُقترح كعمل مستقبلي استقصاء الظروف التي تكون فيها البرامج الخالية من الحلقات كافية وتقليل الاعتماد على محركات حذف المكممات الثقيلة.