Can We Formally Verify Neural PDE Surrogates? SMT Compilation of Small Fourier Neural Operators
تُثبت هذه الورقة أنه يمكن التحقق من صحة معاملات فوريه العصبية الصغيرة (Fourier Neural Operators) رسمياً لخصائص فيزيائية مثل الإيجابية وحفظ الكتلة عبر تجميع عمليات تمريرها الأمامية الخطية المجزأة في حلول SMT، مما يكشف عن مقايضة واضحة حيث توفر الترميزات الدقيقة ضمانات سليمة ولكنها تعاني من صعوبة في التوسع، بينما توفر الترميزات التقريبية السرعة على حساب القدرة على التصديق.