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

技術的サマリー：小型フーリエニューラルオペレータの SMT コンパイル

問題定義
フーリエニューラルオペレータ（FNO）は、偏微分方程式（PDE）シミュレーションに対して大幅な高速化をもたらしますが、質量保存や濃度の非負性といった物理的制約に関する形式的保証を欠くことが多々あります。標準的な検証はモンテカルロ（MC）テストや勾配ベースの反証に依存しますが、これらの手法は特定の入力をサンプリングするに留まり、連続的な入力領域全体にわたる網羅的な保証を提供することはできません。既存のニューラルネットワーク検証ツールは主に分類器や制御方針向けに設計されており、スペクトル畳み込み、関数空間入力、または保存則といった PDE 固有の性質をネイティブに扱えません。

手法
著者は、訓練済みの FNO を形式的検証を可能にする Satisfiability Modulo Theories（SMT）ソルバ、特に Z3 へコンパイルすることを提案します。核心的な洞察は、固定グリッドと固定訓練重みにおいて、FNO 内のスペクトル畳み込みが線形写像であるという点です。したがって、ReLU 非線形性を持つ FNO は、前方伝播を近似することなく Z3 の線形実数算術で正確に表現可能な、区分的線形写像となります。

手法は 2 つの主要なエンコーディング戦略を含みます：

1. 正確なエンコーディング：スペクトル畳み込みを、標準基底ベクトルに演算を適用することで明示的な密行列（$W^{spec}$）としてコンパイルします。完全な前方伝播は、アフィン写像と成分ごとの ReLU 関数の合成として表現されます。このエンコーディングは健全（sound）であり、「UNSAT」の結果は許容されるすべての入力に対して性質が成り立つことを証明し、「SAT」の結果は有効な反例を提供します。ただし、計算複雑性は $O(N^2H^2L)$ となり、小さなグリッドサイズ（$N \le 32$）に制限されます。
2. 凍結エンコーディング：より大きなグリッド（$N \le 64$）へスケーリングするため、スペクトル経路を参照入力から導出された定数に置き換えます。これにより複雑性は $O(NH^2L)$ に減少し、1 秒未満のチェックが可能になります。ただし、これは近似であり、「UNSAT」の結果は元の FNO ではなく凍結された代理モデルのみを証明し、「SAT」の結果は元のモデルでの検証を必要とします。

実験は、周期的境界条件を持つ 1 次元移流 - 拡散 - 反応（ADR）方程式に焦点を当てています。本研究は以下の 2 つの性質を検証します：

• 質量非増加：出力の離散質量が許容誤差 $\epsilon = 0.05$ 以内で入力質量を超えないか確認します。
• 非負性：非負の入力がすべてのグリッド点において非負の出力を生むか確認します。

主な貢献

• 正確なコンパイル：明示的なスペクトル行列を構築することにより、固定グリッド FNO を Z3 の線形実数算術へ正確にコンパイルする初の試みを提示しました。
• 初の形式的証明：ニューラル PDE オペレータに対する最初の健全な形式的証明を提供し、特にグリッドサイズ 16 までの線形（ReLU 非使用）FNO に対して非負性の証明書を生成しました。
• 比較分析：10 個の小型モデル（パラメータ数 85〜117）において、勾配ベースの反証やモンテカルロテストと比較して Z3 を評価しました。
• 健全性 - スケーラビリティの境界：正確な検証とスケーラビリティのトレードオフを特徴付け、正確なエンコーディングは小型線形モデルの証明と中規模 ReLU モデルの反例をサポートする一方、近似エンコーディングはさらにスケーリング可能ですが、元のモデルに対する形式的健全性を失うことを実証しました。

結果

• 質量非増加：正確なエンコーディングを使用し、Z3 は 10 個のモデルすべてに対して健全な質量違反の反例を発見しました。10 個のモデルのうち 7 つにおいて、Z3 は勾配ベースの反証および MC テストの両方よりも深刻な違反を発見しました。線形モデルでは、Z3 はより深い違反を見つけるために大域的に最適化しました。ReLU モデルでは、勾配探索が競争力がありました。
• 非負性：
  • 線形モデル（L=1）：Z3 は 2 つの健全な非負性証明（グリッドサイズ $N=8$ および $N=16$ 用）を生成し、他の線形モデルで 4 つの健全な反例を発見しました。
  • ReLU モデル（L=2）：Z3 は 1 つの健全な反例を発見しましたが、活性化パターンの組み合わせ爆発（$2^{NH}$）により、残りの 3 つの非負性クエリでタイムアウトしました。勾配反証は、Z3 よりも頻繁に深刻度が高い違反を含め、すべての 4 つの ReLU モデルで違反を成功裏に見つけました。
• 凍結エンコーディング：このアプローチは、8 つの大型モデル（$N=32$ から $64$）において非負性の検証に成功し、そのうち 4 つで質量の反例を発見しました。ただし、これらの結果は近似です。非負性の証明は凍結された代理モデルにのみ適用され、質量の反例は元のモデルでの再検証を必要としました（3 つは確認済み、1 つは未確認）。

意義と主張
本論文は、生産規模の検証に対する解決策というよりも、概念実証として位置づけられています。著者は明示的に、その結果がスケーラブルな FNO 検証を解決するものではないと述べており、テストされたモデルは「玩具サイズ」であり、凍結された隠れ層と限られたパラメータを持つものです。

意義は以下の点にあります：

1. FNO を区分的線形形式へ正確にコンパイルでき、物理に動機づけられた性質に対する SMT ソルバの使用を可能にすること。
2. 小規模な線形ニューラルオペレータに対する形式的検証が実現可能であり、そのようなシステムに対する初の健全な証明書を生成できること。
3. 明確な境界が存在すること：正確な証明は現在、小規模な線形モデルに対してのみ実用的であり、正確な反例は中規模の ReLU モデルまで拡張可能であること。より大規模なオペレータには、汎用 SMT ソルバではなく、近似エンコーディングまたは $\alpha$-$\beta$-CROWN などの専門的なスケーラブルなニューラルネットワーク検証器との統合が必要となります。

著者は、この研究が形式的検証コミュニティに対してニューラル PDE 代理モデルへの関与を促し、オペレータ学習コミュニティが検証可能性を設計基準として扱うべきであることを示唆すると結論付けています。