論文の概要: Scalable Formal Verification via Autoencoder Latent Space Abstraction

• arxiv url: http://arxiv.org/abs/2512.13593v2
• Date: Tue, 16 Dec 2025 16:58:02 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-17 14:48:05.993833
• Title: Scalable Formal Verification via Autoencoder Latent Space Abstraction
• Title（参考訳）: オートエンコーダ遅延空間抽象化によるスケーラブルな形式検証
• Authors: Robert Reed, Luca Laurenti, Morteza Lahijanian,
• Abstract要約: コンベックスオートエンコーダを用いてシステムの次元を小さくし,カーネルベースの手法で潜伏空間の力学を学習する形式的手法を提案する。 潜伏空間における検証結果を元のシステムにマッピングできることが示される。
• 参考スコア（独自算出の注目度）: 13.740416712776456
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Finite Abstraction methods provide a powerful formal framework for proving that systems satisfy their specifications. However, these techniques face scalability challenges for high-dimensional systems, as they rely on state-space discretization which grows exponentially with dimension. Learning-based approaches to dimensionality reduction, utilizing neural networks and autoencoders, have shown great potential to alleviate this problem. However, ensuring the correctness of the resulting verification results remains an open question. In this work, we provide a formal approach to reduce the dimensionality of systems via convex autoencoders and learn the dynamics in the latent space through a kernel-based method. We then construct a finite abstraction from the learned model in the latent space and guarantee that the abstraction contains the true behaviors of the original system. We show that the verification results in the latent space can be mapped back to the original system. Finally, we demonstrate the effectiveness of our approach on multiple systems, including a 26D system controlled by a neural network, showing significant scalability improvements without loss of rigor.
• Abstract（参考訳）: 有限抽象法は、システムが仕様を満たすことを証明するための強力な形式的なフレームワークを提供する。 しかし、これらの手法は、次元とともに指数関数的に成長する状態空間の離散化に依存するため、高次元システムに対するスケーラビリティの課題に直面している。 ニューラルネットワークとオートエンコーダを利用した,次元削減のための学習ベースのアプローチは,この問題を軽減する大きな可能性を示している。 しかし、結果の正当性を保証することは未解決の問題である。 本研究では,凸オートエンコーダを用いたシステム次元の削減と,カーネルベースの手法による潜伏空間のダイナミクスの学習を行うための公式なアプローチを提案する。 次に、学習したモデルから潜在空間に有限の抽象化を構築し、その抽象化が元のシステムの真の振る舞いを含むことを保証する。 潜伏空間における検証結果を元のシステムにマッピングできることが示される。 最後に、ニューラルネットワークによって制御される26Dシステムを含む複数のシステムに対するアプローチの有効性を示す。

関連論文リスト

• Certified Neural Approximations of Nonlinear Dynamics [51.01318247729693]
  安全クリティカルな文脈では、神経近似の使用は、基礎となるシステムとの密接性に公式な境界を必要とする。 本稿では,認証された一階述語モデルに基づく新しい,適応的で並列化可能な検証手法を提案する。
  論文  参考訳（メタデータ） (2025-05-21T13:22:20Z)
• Physics-Informed Latent Neural Operator for Real-time Predictions of time-dependent parametric PDEs [0.0]
  ディープ・オペレーター・ネットワーク(DeepONet)は、偏微分方程式(PDE)によって支配される系の代理モデルとして約束されている。 本研究では,物理を直接学習プロセスに統合する物理インフォームトニューラルネットワークフレームワークPI-Latent-NOを提案する。
  論文  参考訳（メタデータ） (2025-01-14T20:38:30Z)
• Input-to-State Stable Coupled Oscillator Networks for Closed-form Model-based Control in Latent Space [2.527926867319859]
  我々は、制御理論の文献から強力でよく理解された閉形式戦略を活用することが有望な道であると論じる。 既存の潜在空間モデルにおける3つの根本的な欠点は、これまでこの強力な組み合わせを妨げてきた。 これらすべての問題に同時に取り組む新しい結合ネットワーク(CON)モデルを提案する。
  論文  参考訳（メタデータ） (2024-09-13T00:11:09Z)
• Latent Dynamics Networks (LDNets): learning the intrinsic dynamics of spatio-temporal processes [2.3694122563610924]
  ラテント・ダイナミクス・ネットワーク(LDNet)は、非マルコフ力学系の低次元固有力学を発見できる。 LDNetは軽量で訓練が容易で、時間外挿方式でも精度と一般化性に優れている。
  論文  参考訳（メタデータ） (2023-04-28T21:11:13Z)
• On Optimizing Back-Substitution Methods for Neural Network Verification [1.4394939014120451]
  本稿では, 後方置換がより厳密な境界を生じさせるアプローチを提案する。 我々の技術は、多くの既存のシンボル境界伝搬技術に統合できるという意味で、一般的なものである。
  論文  参考訳（メタデータ） (2022-08-16T11:16:44Z)
• Self-Supervised Training with Autoencoders for Visual Anomaly Detection [61.62861063776813]
  我々は, 正規サンプルの分布を低次元多様体で支持する異常検出において, 特定のユースケースに焦点を当てた。 我々は、訓練中に識別情報を活用する自己指導型学習体制に適応するが、通常の例のサブ多様体に焦点をあてる。 製造領域における視覚異常検出のための挑戦的なベンチマークであるMVTec ADデータセットで、最先端の新たな結果を達成する。
  論文  参考訳（メタデータ） (2022-06-23T14:16:30Z)
• Pure Exploration in Kernel and Neural Bandits [90.23165420559664]
  我々は、特徴表現の次元が腕の数よりもはるかに大きい帯域における純粋な探索について研究する。 そこで本研究では,各アームの特徴表現を低次元空間に適応的に埋め込む手法を提案する。
  論文  参考訳（メタデータ） (2021-06-22T19:51:59Z)
• Explicitly Encouraging Low Fractional Dimensional Trajectories Via Reinforcement Learning [6.548580592686076]
  モデル自由強化学習エージェントによって誘導される軌道の次元性は,エージェント報酬信号にポストプロセッシング関数を追加することで影響できることを示す。 システムに付加されるノイズに対して寸法の低減が堅牢であることを検証するとともに, 改良されたエージェントは, 一般に, 騒音や押圧障害に対してより現実的に堅牢であることを示す。
  論文  参考訳（メタデータ） (2020-12-21T20:09:17Z)
• MetaSDF: Meta-learning Signed Distance Functions [85.81290552559817]
  ニューラルな暗示表現で形状を一般化することは、各関数空間上の学習先行値に比例する。 形状空間の学習をメタラーニング問題として定式化し、勾配に基づくメタラーニングアルゴリズムを利用してこの課題を解決する。
  論文  参考訳（メタデータ） (2020-06-17T05:14:53Z)

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

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