論文の概要: TNODEV: Toolbox for Neural ODE Verification
- arxiv url: http://arxiv.org/abs/2606.16567v1
- Date: Mon, 15 Jun 2026 11:09:06 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-16 16:21:34.475001
- Title: TNODEV: Toolbox for Neural ODE Verification
- Title（参考訳）: TNODEV: ニューラルネットワーク検証ツールボックス
- Authors: Abdelrahman Sayed Sayed, Pierre-Jean Meyer, Mohamed Ghazel,
- Abstract要約: ニューラル・オードの最初の音響形式検証器であるTNODEVについて述べる。
ニューラル・ニューラル・オード(GNODE)とニューラル・ニューラル・オード(GNODE)によるクローズド・ループ内のニューラル・オードの安全な包摂性検証を支援する。
我々は,TNODEVを,安全な包摂性および分類ロバスト性にまたがる様々なベンチマークで評価した。
- 参考スコア（独自算出の注目度）: 1.7205106391379026
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: Neural ordinary differential equations (neural ODE) have started to appear in safety critical settings such as continuous-time controllers for cyber-physical systems and classifiers integrated into automated decision pipelines, raising the question of whether their behavior can be formally verified. Existing tools dedicated to neural ODE provide only a single reachability call without iterative input set refinement, limiting the precision of their verdicts to whatever one reachability call can deliver. We present TNODEV, the first sound formal verifier for neural ODE that integrates a falsification checker, a fast interval-based reachability backend based on continuous-time mixed monotonicity, a verification and refinement loop with three input-set splitting heuristics, and a parallel scheduler in a single end-to-end pipeline. TNODEV supports safe-set inclusion verification on pure neural ODE, neural ODE in closed loop with a neural network controller and general neural ODE (GNODE), with the safe set specified either as an interval or as the half-space intersection induced by a target classification label. We evaluate TNODEV on a range of benchmarks across safe-set inclusion and classification-robustness properties, including a direct reachability comparison against NNV~2.0 and CORA and a verification comparison against NNV2.0 on MNIST general neural ODE classifiers.
- Abstract（参考訳）: ニューラル常微分方程式(ニューラルODE)は、サイバー物理システムのための連続時間制御器や自動決定パイプラインに統合された分類器などの安全クリティカルセッティングに現れ始めており、それらの挙動を正式に検証できるかどうかという疑問が提起されている。
既存のニューラルODE専用のツールは、反復的な入力セットの洗練なしに単一のリーチビリティコールのみを提供し、検証の精度を1つのリーチビリティコールが提供できるものに制限する。
本稿では,Falsification Checkerと連続時間混合単調性に基づく高速区間ベースリーチビリティバックエンド,3つの入力セット分割ヒューリスティックを持つ検証・改善ループ,単一エンドツーエンドパイプラインにおける並列スケジューラを統合した,最初のニューラルODE用音響形式検証器TNODEVを提案する。
TNODEVは、純粋なニューラルODE、ニューラルネットワークコントローラと一般ニューラルODE(GNODE)によるクローズドループ内のニューラルODEの安全な包含検証をサポートし、安全なセットはインターバルまたはターゲット分類ラベルによって誘導されるハーフスペースの交叉として指定される。
NNV~2.0 と CORA との直接到達性比較,MNIST の一般ニューラル・オード分類器におけるNNV2.0 との比較などを含む,安全な包摂性および分類ロバスト性特性のベンチマークにおける TNODEV の評価を行った。
関連論文リスト
- Fidelity-informed neural pulse compilation of a continuous family of quantum gates with uncertainty-margin analysis [0.0]
我々は,3量子状態核磁気共鳴(NMR)プロセッサ上で,単一量子ゲート群に対するニューラルパルスコンパイルフレームワークを開発した。
対象のユニタリを校正基底ゲート列に分解する代わりに、SU(2)演算において任意のUの軸角パラメータから直接写像を学習する。
一つのモデルが連続的なゲートパラメータにわたって一般化されることを数値的に示し、ベンチトップ3量子NMRデバイス上での代表パルスを実験的に検証する。
論文 参考訳（メタデータ） (2026-04-13T11:17:18Z) - Certified Neural Approximations of Nonlinear Dynamics [51.01318247729693]
安全クリティカルな文脈では、神経近似の使用は、基礎となるシステムとの密接性に公式な境界を必要とする。
本稿では,認証された一階述語モデルに基づく新しい,適応的で並列化可能な検証手法を提案する。
論文 参考訳（メタデータ） (2025-05-21T13:22:20Z) - DeNOTS: Stable Deep Neural ODEs for Time Series [0.99450247450967]
CDEは不規則時系列の時間的進化を処理する方法を提供する。
我々は、NFEの増加とモデルの「深化」のために統合時間地平線を拡大することを提案する。
また、負のフィードバックによって動的を安定化する方法を提案する。
論文 参考訳（メタデータ） (2024-08-15T09:49:37Z) - On Tuning Neural ODE for Stability, Consistency and Faster Convergence [0.0]
本研究では,Nesterov'sAccelerated gradient (NAG) を用いたODE-solverを提案する。
我々は、より速くトレーニングし、より優れた、または同等のパフォーマンスをニューラルダイオードに対して達成し、アプローチの有効性を実証的に実証した。
論文 参考訳（メタデータ） (2023-12-04T06:18:10Z) - From NeurODEs to AutoencODEs: a mean-field control framework for
width-varying Neural Networks [68.8204255655161]
本稿では,動的に駆動する制御フィールドをベースとした,AutoencODEと呼ばれる新しいタイプの連続時間制御システムを提案する。
損失関数が局所凸な領域では,多くのアーキテクチャが復元可能であることを示す。
論文 参考訳（メタデータ） (2023-07-05T13:26:17Z) - Benign Overfitting in Deep Neural Networks under Lazy Training [72.28294823115502]
データ分布が適切に分離された場合、DNNは分類のためのベイズ最適テスト誤差を達成できることを示す。
よりスムーズな関数との補間により、より一般化できることを示す。
論文 参考訳（メタデータ） (2023-05-30T19:37:44Z) - Continuous time recurrent neural networks: overview and application to
forecasting blood glucose in the intensive care unit [56.801856519460465]
連続時間自己回帰リカレントニューラルネットワーク(Continuous Time Autoregressive Recurrent Neural Network, CTRNN)は、不規則な観測を考慮に入れたディープラーニングモデルである。
重篤なケア環境下での血糖値の確率予測へのこれらのモデルの適用を実証する。
論文 参考訳（メタデータ） (2023-04-14T09:39:06Z) - On the Forward Invariance of Neural ODEs [92.07281135902922]
本稿では,ニューラル常微分方程式(ODE)が出力仕様を満たすことを保証するための新しい手法を提案する。
提案手法では,出力仕様を学習システムのパラメータや入力の制約に変換するために,制御障壁関数のクラスを用いる。
論文 参考訳（メタデータ） (2022-10-10T15:18:28Z) - Neural Clamping: Joint Input Perturbation and Temperature Scaling for Neural Network Calibration [62.4971588282174]
我々はニューラルクランプ法と呼ばれる新しい後処理キャリブレーション法を提案する。
実験の結果,Neural Clampingは最先端の処理後のキャリブレーション法よりも優れていた。
論文 参考訳（メタデータ） (2022-09-23T14:18:39Z) - Blind Coherent Preamble Detection via Neural Networks [2.2063018784238984]
ニューラルネットワーク(NN)シークエンス検出器とタイミング先進推定器を提案する。
NNによるプリアンブル検出のプロセス全体を置き換えるものではない。
本稿では,通信路効果を補うために,検出器内の信号を組み合わせたテキストブロードコヒーレントにのみNNを用いることを提案する。
論文 参考訳（メタデータ） (2021-09-30T09:53:49Z) - Provably-Robust Runtime Monitoring of Neuron Activation Patterns [0.0]
ディープニューラルネットワークの入力がトレーニングで使用されるデータと似ている場合、運用時間で監視することが望ましい。
モニタ構築プロセス内に公式な記号的推論を統合することで,この問題に対処する。
証明可能な堅牢性は、単一のニューロンの監視が複数のビット以上を使用する場合にさらに一般化される。
論文 参考訳（メタデータ） (2020-11-24T08:37:18Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。