論文の概要: Can We Formally Verify Neural PDE Surrogates? SMT Compilation of Small Fourier Neural Operators

• arxiv url: http://arxiv.org/abs/2605.08938v1
• Date: Sat, 09 May 2026 13:16:24 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-12 23:28:49.980299
• Title: Can We Formally Verify Neural PDE Surrogates? SMT Compilation of Small Fourier Neural Operators
• Title（参考訳）: ニューラルPDEサロゲートを形式的に検証できるか? : 小型フーリエニューラル演算子のSMTコンパイル
• Abstract要約: トレーニングされた重みと格子が固定されると、FNOのスペクトル畳み込みは線形写像であることを示す。 その結果、音質-可聴性トレードオフを明確化し、生産規模のニューラル演算子の形式的検証に必要なものを指し示している。
• 参考スコア（独自算出の注目度）: 5.274108539480755
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Fourier Neural Operators (FNOs) can greatly accelerate PDE simulation, but they are often used without formal guarantees that they preserve basic physical structure. We show that, once the trained weights and grid are fixed, the spectral convolution in an FNO is a linear map. As a result, the full forward pass is piecewise-linear and can be represented exactly in Z3's linear real arithmetic. We study two encodings. The exact encoding compiles the spectral convolution into a dense matrix multiplication, which is sound for both proofs and counterexamples. The lighter frozen encoding replaces the spectral path with a constant, making it faster but approximate. On 10 small FNO surrogates for 1D advection-diffusion-reaction (85 to 117 parameters, grids 8 to 32), the exact encoding gives 2 sound positivity proofs on linear (ReLU-free) models, 5 sound positivity counterexamples, and 10 sound mass-violation counterexamples; the remaining 3 positivity queries on ReLU models time out. For mass non-increase, Z3 finds worse counterexamples than both gradient-based falsification and Monte Carlo on 7 of 10 models. The frozen encoding scales to grid size 64 with sub-second positivity checks, but it no longer provides certificates for the original FNO. Overall, the results make the soundness--scalability tradeoff explicit and point to what is needed for formal verification of production-scale neural operators.
• Abstract（参考訳）: フーリエニューラル演算子(FNO)はPDEシミュレーションを大幅に高速化するが、基本的な物理構造を保存するという正式な保証なしにしばしば使用される。 トレーニングされた重みと格子が固定されると、FNOのスペクトル畳み込みは線形写像であることを示す。 その結果、フルフォワードパスは断片的に線形であり、Z3の線形実算術で正確に表現できる。 私たちは2つのエンコーディングを研究します。 正確な符号化はスペクトルの畳み込みを密度の高い行列乗法にコンパイルする。 より軽量な凍結符号化はスペクトルパスを一定に置き換え、高速だが近似する。 1次元の対流拡散反応のための10個の小さなFNOサロゲート(85から117個のパラメータ、格子8から32)では、正確な符号化は線形(ReLUのない)モデルに2つの正の証明を与える。 質量非増加の場合、Z3は10モデル中7モデルで勾配ベースのファルシフィケーションとモンテカルロよりも悪い反例を見出す。 凍結符号化は、サブ秒の陽性チェックでグリッドサイズ64までスケールするが、元のFNOの証明書は提供されない。 全体として、結果は音質-スケーリング可能性トレードオフを明確にし、プロダクションスケールのニューラル演算子の形式的検証に必要なものを指し示している。

関連論文リスト

• A Constitutive Markov Physics-Informed Neural Operator (MPNO) for Autoregressive Stability in Transient Dynamics [14.04953000698584]
  本稿では,一段階進化を伝搬演算子としてモデル化したマルコフ物理インフォームドニューラル演算子(MPNO)を提案する。 MPNOは100/135/165 m/sで全ての試験種子の有界誤差で安定にロールアウトし、単一ステップの相対的なL2誤差は0.7304 +/- 0.0008であり、FNOのパラメータの約4分の1でFNOに匹敵する。 約20Kパラメータで、MPNOはLS-DYNA上で約105倍の推論速度を提供する。
  論文  参考訳（メタデータ） (2026-08-26T12:54:37Z)
• MiNO: Cotangent-bundle propagator learning for PDEs [3.1861308132183375]
  第3のターゲットとして,位相空間における位相,振幅,プロパゲータ自体について検討する。 輸送された不連続性は空間と時間において非滑らかであるため、進化をもたらす物体はそれが生成する場よりもはるかに滑らかである。 ニューラルタングエントブランチ損失バランスを持つ物理インフォームニューラルネットワークは、初期エラーの近くに留まる。
  論文  参考訳（メタデータ） (2026-08-15T12:02:03Z)
• An end-to-end quantum algorithm for weakly nonlinear plasma physics with superquadratic speedup [0.0]
  運動プラズマシミュレーションは高次元で古典的に要求される。 量子アルゴリズムは、非線形力学を線形計算に埋め込んだり、高密度な場-相互作用データをロードしたり、情報を効率的に抽出したりするなど、さまざまなボトルネックに直面している。 弱非線形な非線形プラズマモデルに対して,厳密な収束を保証するエンドツーエンドの量子アルゴリズムを提案する。
  論文  参考訳（メタデータ） (2026-07-15T19:14:21Z)
• What Does a Discrete Diffusion Model Learn? [71.03603607324338]
  離散拡散モデルは、デノイザ、スコア比、ブリッジプラグイン予測器などを学ぶ。 まず, 連続時間マルコフ連鎖 (CTMC) ELBO の任意のノイズ発生過程に対する厳密な導出から始める。 すべてのアイデンティティは、正確に解けるモデル上で近似なしで数値的に検証される。
  論文  参考訳（メタデータ） (2026-07-06T17:56:11Z)
• Scale-Invariant Neural Network Optimization: Norm Geometry and Heavy-Tailed Noise [12.977441534320041]
  スペクトルノルムを持つスケール不変の1次法は$(minm, n-frac3p-2p-1)の呼び出しを必要とすることを示す。 我々は、標準がスペクトルであり、ヘシアンがリプシッツであるとき、バッチ法が$(minm, n-frac5p2p-2p-2)$のマッチング境界を達成することを証明した。
  論文  参考訳（メタデータ） (2026-05-18T15:13:18Z)
• FUTON: Fourier Tensor Network for Implicit Neural Representations [56.48739018255443]
  入射神経表現(INR)はシグナルを符号化する強力なツールとして現れてきたが、支配的な設計はしばしば収束が遅く、ノイズに過度に適応し、外挿が不十分である。 低ランクテンソル分解により係数がパラメータ化される一般化フーリエ級数として信号をモデル化するFUTONを導入する。
  論文  参考訳（メタデータ） (2026-02-13T19:31:44Z)
• Differentiable Logic Synthesis: Spectral Coefficient Selection via Sinkhorn-Constrained Composition [0.0]
  凍結フーリエ基底からスペクトル係数を選択する微分可能なアーキテクチャである階層スペクトル合成を導入する。 我々はこのフレームワークを論理合成に適用し、ブール否定を可能にするカラムサイン変調を追加する。
  論文  参考訳（メタデータ） (2026-01-20T13:26:52Z)
• A Lindblad-Pauli Framework for Coarse-Grained Chaotic Binary-State Dynamics [0.0]
  我々は、駆動ダッフィング発振器の粗粒度左/右の統計情報を2時間2$密度行列表現に埋め込む2状態フレームワークを開発した。 対角状態の場合、GKSL力学は古典的な二状態方程式に還元される。 我々は閉形式解、明示的なクラウス表現、時間的一階マルコフ仮定の実用的な診断を導出する。
  論文  参考訳（メタデータ） (2025-12-19T03:27:05Z)
• Rao-Blackwell Gradient Estimators for Equivariant Denoising Diffusion [55.95767828747407]
  分子やタンパク質の生成のようなドメインでは、物理系はモデルにとって重要な固有の対称性を示す。 学習のばらつきを低減し、確率的に低い分散勾配推定器を提供するフレームワークを提案する。 また,軌道拡散法(Orbit Diffusion)と呼ばれる手法を用いて,損失とサンプリングの手順を取り入れた推定器の実用的実装を提案する。
  論文  参考訳（メタデータ） (2025-02-14T03:26:57Z)
• Topological quantum compilation of metaplectic anyons based on the genetic optimized algorithms [0.0]
  我々は、textitF-matrices, textitR-symbols, and fusion rules of metaplectic anyonを用いて、合計6つのエノンモデルを得る。 1ビットの場合、古典的 textitH- と textitT-gate は遺伝的アルゴリズムを改良した Solovay-Kitaev アルゴリズムを用いてうまく構築できる。
  論文  参考訳（メタデータ） (2025-01-03T10:18:16Z)
• Learning with Norm Constrained, Over-parameterized, Two-layer Neural Networks [54.177130905659155]
  近年の研究では、再生カーネルヒルベルト空間(RKHS)がニューラルネットワークによる関数のモデル化に適した空間ではないことが示されている。 本稿では,有界ノルムを持つオーバーパラメータ化された2層ニューラルネットワークに適した関数空間について検討する。
  論文  参考訳（メタデータ） (2024-04-29T15:04:07Z)
• SKI to go Faster: Accelerating Toeplitz Neural Networks via Asymmetric Kernels [69.47358238222586]
  Toeplitz Neural Networks (TNN) は、印象的な結果を持つ最近のシーケンスモデルである。 我々は, O(n) 計算複雑性と O(n) 相対位置エンコーダ (RPE) 多層パーセプトロン (MLP) と減衰バイアスコールの低減を目指す。 双方向モデルの場合、これはスパースと低ランクのToeplitz行列分解を動機付ける。
  論文  参考訳（メタデータ） (2023-05-15T21:25:35Z)
• SiMaN: Sign-to-Magnitude Network Binarization [165.5630656849309]
  重みバイナライゼーションは、高倍率重みを+1s、0sに符号化することで分析ソリューションを提供する。 二元化ネットワークの学習重みは、エントロピーを許さないラプラシアン分布に概ね従うことが証明される。 CIFAR-10 と ImageNet を用いて,シマナライゼーション (SiMaN) と呼ばれる手法の評価を行った。
  論文  参考訳（メタデータ） (2021-02-16T07:03:51Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。