Can We Formally Verify Neural PDE Surrogates? SMT Compilation of Small Fourier Neural Operators

ملخص تقني: تجميع مشغلات نيورونية فورية (FNO) صغيرة باستخدام SMT

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

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

تتضمن المنهجية استراتيجيتين رئيسيتين للترميز:

1. الترميز الدقيق (Exact Encoding): يتم تجميع الالتفاف الطيفي إلى مصفوفة كثيفة صريحة ($W^{spec}$) عن طريق تطبيق العملية على متجهات الأساس القياسية. ويتم تمثيل المسار الأمامي الكامل كتركيب من الخرائط الأفينية ودوال ReLU لكل إحداثي. هذا الترميز سليم (sound)، مما يعني أن نتيجة "UNSAT" تثبت صحة الخاصية لجميع المدخلات المقبولة، بينما توفر نتيجة "SAT" مثالاً مضاداً صالحاً. ومع ذلك، يتوسع التعقيد بمعدل $O(N^2H^2L)$، مما يحد من استخدامه في أحجام الشبكات الصغيرة ($N \le 32$).
2. الترميز المجمد (Frozen Encoding): لزيتماد النطاق إلى شبكات أكبر ($N \le 64$)، يتم استبدال المسار الطيفي بثابت مشتق من مدخل مرجعي. يقلل هذا من التعقيد إلى $O(NH^2L)$ ويسمح بعمليات تحقق في أقل من ثانية. ومع ذلك، يعد هذا تقريباً؛ حيث إن نتائج "UNSAT" تشهد فقط للنموذج البديل المجمد، وليس لـ FNO الأصلي، كما تتطلب نتائج "SAT" إعادة التحقق على النموذج الأصلي.

تركز التجارب على معادلات (ADR) أحادية البعد (الانتشار-الحمل-التفاعل) مع شروط حدودية دورية. وتتحقق الدراسة من خاصيتين:

• عدم زيادة الكتلة: التحقق مما إذا كانت الكتلة المنفصلة للمخرجات تتجاوز كتلة المدخلات بهامش سماح $\epsilon = 0.05$.
• الإيجابية: التحقق مما إذا كانت المدخلات غير السالبة تنتج مخرجات غير سالبة عند جميع نقاط الشبكة.

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

• التجميع الدقيق: يقدم البحث أول تجميع دقيق لمشغلات FNO ذات الشبكة الثابتة في حسابات الأعداد الحقيقية الخطية لـ Z3 من خلال بناء مصفوفات طيفية صريحة.
• أول البراهين الرسمية: يقدم البحث أول براهين رسمية سليمة لمشغل معادلة تفاضلية جزئية نيوروني، وتحديداً توليد شهادات الإيجابية لـ FNO الخطية (الخالية من ReLU) لأحجام شبكات تصل إلى 16.
• التحليل المقارن: يقارن العمل بين Z3 والتكذيب القائم على التدرج واختبار مونت كارلو عبر 10 نماذج صغيرة (85-117 بارامتراً).
• حد المتانة-القابلية للتوسع: يحدد المؤلفون المقايضة بين التحقق الدقيق والقابلية للتوسع، موضحين أن الترميزات الدقيقة تدعم البراهين للنماذج الخطية الصغيرة، بينما تدعم الأمثلة المضادة للنماذج المتوسطة التي تحتوي على ReLU، في حين أن الترميزات التقريبية تتوسع بشكل أكبر ولكنها تفقد المتانة الرسمية للنموذج الأصلي.

النتائج

• عدم زيادة الكتلة: باستخدام الترميز الدقيق، وجد Z3 أمثلة مضادة سليمة لانتهاك الكتلة لجميع النماذج العشرة. وفي 7 من أصل 10 نماذج، اكتشف Z3 انتهاكات أكثر حدة من كل من التكذيب القائم على التدرج واختبار مونت كارلو. بالنسبة للنماذج الخطية، قام Z3 بالتحسين عالمياً لإيجاد انتهاكات أعمق؛ أما بالنسبة لنماذج ReLU، فقد ظل البحث عن التدرج تنافسياً.
• الإيجابية:
  • النماذج الخطية (L=1): أنتج Z3 برهانين سليمين للإيجابية (لحجم شبكة $N=8$ و $N=16$) ووجد 4 أمثلة مضادة سليمة في النماذج الخطية الأخرى.
  • نماذج ReLU (L=2): وجد Z3 مثالاً مضاداً سليماً واحداً، لكنه استغرق وقتاً طويلاً (timeout) في طلبات الإيجبية الثلاثة المتبقية بسبب الانفجار التوليفي لأنماط التنشيط ($2^{NH}$). نجح التكذيب القائم على التدرج في إيجاد انتهاكات في جميع نماذج ReLU الأربعة، وغالباً بحدة أكبر من Z3.
• الترميز المجمد: نجح هذا النهج في التحقق من الإيجابية في 8 نماذج أكبر ($N=32$ إلى $64$) ووجد أمثلة مضادة للكتلة في 4 منها. ومع ذلك، فإن هذه النتائج تقريبية؛ إذ تنطبق براهين الإيجابية فقط على البديل المجمد، وتطلبت الأمثلة المضادة للكتلة إعادة التحقق على النموذج الأصلي (تم تأكيد 3 حالات، ولم يتم تأكيد حالة واحدة).

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

تكمن الأهمية في إثبات ما يلي:

1. يمكن تجميع FNOs بدقة في أشكال خطية مجزأة، مما يسمح باستخدام برامج حل SMT للخصائص المستوحاة من الفيزياء.
2. التحقق الرسمي ممكن للنماذج النيورونية التشغيلية الخطية الصغيرة، مما يوفر أول الشهادات السليمة لمثل هذه الأنظمة.
3. هناك حد واضح: البراهين الدقيقة عملية حالياً فقط للنماذج الخطية الصغيرة، بينما تمتد الأمثلة المضادة الدقيقة إلى نماذج ReLU المتوسطة. ستتطلب المشغلات الأكبر إما ترميزات تقريبية أو دمجاً مع برامج تحقق نيورونية متخصصة وقابلة للتوسع (مثل $\alpha$-$\beta$-CROWN) بدلاً من برامج حل SMT العامة.

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