論文の概要: Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision

• arxiv url: http://arxiv.org/abs/2507.22760v1
• Date: Wed, 30 Jul 2025 15:21:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-31 16:14:18.281708
• Title: Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
• Title（参考訳）: 良き神と悪しき天使: 有限精度で安全な制御を保証
• Authors: Samuel Teuber, Debasmita Lohar, Bernhard Beckert,
• Abstract要約: 本稿では,有限精度摂動に頑健さを取り入れた理論保証と実世界の実装のギャップを埋める。 我々は、音質と効率的な実装を合成するために、最先端の混合精度固定点チューナーを用いて、完全なエンドツーエンドソリューションを提供する。 我々は,自動車・航空分野のケーススタディにアプローチし,厳密な無限時間地平線安全保証を備えた効率的なNN実装を構築した。
• 参考スコア（独自算出の注目度）: 0.716879432974126
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: As neural networks (NNs) become increasingly prevalent in safety-critical neural network-controlled cyber-physical systems (NNCSs), formally guaranteeing their safety becomes crucial. For these systems, safety must be ensured throughout their entire operation, necessitating infinite-time horizon verification. To verify the infinite-time horizon safety of NNCSs, recent approaches leverage Differential Dynamic Logic (dL). However, these dL-based guarantees rely on idealized, real-valued NN semantics and fail to account for roundoff errors introduced by finite-precision implementations. This paper bridges the gap between theoretical guarantees and real-world implementations by incorporating robustness under finite-precision perturbations -- in sensing, actuation, and computation -- into the safety verification. We model the problem as a hybrid game between a good Demon, responsible for control actions, and a bad Angel, introducing perturbations. This formulation enables formal proofs of robustness w.r.t. a given (bounded) perturbation. Leveraging this bound, we employ state-of-the-art mixed-precision fixed-point tuners to synthesize sound and efficient implementations, thus providing a complete end-to-end solution. We evaluate our approach on case studies from the automotive and aeronautics domains, producing efficient NN implementations with rigorous infinite-time horizon safety guarantees.
• Abstract（参考訳）: ニューラルネットワーク(NN)が安全クリティカルなニューラルネットワーク制御サイバー物理システム(NNCS)でますます普及するにつれて、その安全性を正式に保証することが重要である。 これらのシステムでは、安全は操作全体を通して確保され、無限時間地平線検証が必要である。 NNCSの無限時間地平線安全性を検証するため、近年のアプローチでは差動動的論理(dL)を利用する。 しかし、これらのdLベースの保証は、理想化された実数値NNセマンティクスに依存しており、有限精度実装で導入されたラウンドオフエラーを考慮できない。 本稿では, 有限精度摂動下でのロバスト性(センサ, アクティベーション, 計算)を安全性検証に組み込むことにより, 理論的保証と実世界の実装のギャップを埋める。 我々はこの問題を、コントロールアクションに責任を持つ優れたデーモンと、摂動を導入した悪いエンジェルのハイブリッドゲームとしてモデル化する。 この定式化は、与えられた(有界な)摂動に対する堅牢性の形式的証明を可能にする。 このバウンダリを活用することで、最先端の混合精度固定点チューナーを用いて、音質と効率的な実装を合成し、完全なエンドツーエンドソリューションを提供する。 我々は,自動車・航空分野のケーススタディにアプローチし,厳密な無限時間地平線安全保証を備えた効率的なNN実装を構築した。

関連論文リスト

• Reachability Barrier Networks: Learning Hamilton-Jacobi Solutions for Smooth and Flexible Control Barrier Functions [5.846607930201535]
  制御バリア関数(CBF)は、一般的な制御フレームワークに安全保証を付加する一般的な方法である。 物理インフォームドニューラルネットワーク(PINN)を用いて,ハミルトン・ヤコビ最適制御解の計算によりCBFのスムーズな近似を生成する。 我々は、RBNは低次元において非常に正確であり、高次元における標準的な神経CBFアプローチよりも安全であることを示した。
  論文  参考訳（メタデータ） (2025-05-16T23:30:13Z)
• Provably Safe Neural Network Controllers via Differential Dynamic Logic [2.416907802598482]
  NNCS検証のための制御理論の再利用を可能にする最初の一般手法を提案する。 dLの安全な制御エンベロープに基づいて、NN検証によって証明されたNNの仕様を導出する。 本稿では,NNCS の無限時間安全に関する dL 証明によって,仕様に忠実な NNCS の証明が反映されていることを示す。
  論文  参考訳（メタデータ） (2024-02-16T16:15:25Z)
• Scaling #DNN-Verification Tools with Efficient Bound Propagation and Parallel Computing [57.49021927832259]
  ディープニューラルネットワーク(DNN)は多くのシナリオで異常な結果を示した強力なツールです。 しかし、それらの複雑な設計と透明性の欠如は、現実世界のアプリケーションに適用する際の安全性上の懸念を提起する。 DNNの形式的検証(FV)は、安全面の証明可能な保証を提供する貴重なソリューションとして登場した。
  論文  参考訳（メタデータ） (2023-12-10T13:51:25Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。 違反の正確な数を返す新しい手法を提案する。 安全クリティカルなベンチマークのセットに関する実験結果を示す。
  論文  参考訳（メタデータ） (2023-01-17T18:32:01Z)
• Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems [59.57462129637796]
  本稿では,ニューラルネットワークを用いた閉ループシステムの安全性検証のための後方到達性アプローチを提案する。 フィードバックループにおけるNNの存在は、その活性化関数の非線形性や、NNモデルは一般に可逆的ではないため、ユニークな問題セットを示す。 フィードフォワードNNで表される制御ポリシを持つ線形系と非線形系のBP過近似を計算するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2022-09-28T13:17:28Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。 次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。 これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
  論文  参考訳（メタデータ） (2022-08-23T05:02:09Z)
• Log Barriers for Safe Black-box Optimization with Application to Safe Reinforcement Learning [72.97229770329214]
  本稿では,学習時の安全性維持が不可欠である高次元非線形最適化問題に対する一般的なアプローチを提案する。 LBSGDと呼ばれるアプローチは、慎重に選択されたステップサイズで対数障壁近似を適用することに基づいている。 安全強化学習における政策課題の違反を最小限に抑えるためのアプローチの有効性を実証する。
  論文  参考訳（メタデータ） (2022-07-21T11:14:47Z)
• Automated Repair of Neural Networks [0.26651200086513094]
  安全でないNNの安全仕様を修復するためのフレームワークを提案する。 提案手法では,重み値のいくつかを修正して,新しい安全なNN表現を探索することができる。 我々は,提案するフレームワークが安全なNNを実現する能力を示す広範な実験を行った。
  論文  参考訳（メタデータ） (2022-07-17T12:42:24Z)
• Pointwise Feasibility of Gaussian Process-based Safety-Critical Control under Model Uncertainty [77.18483084440182]
  制御バリア関数(CBF)と制御リアプノフ関数(CLF)は、制御システムの安全性と安定性をそれぞれ強化するための一般的なツールである。 本稿では, CBF と CLF を用いた安全クリティカルコントローラにおいて, モデル不確実性に対処するためのガウスプロセス(GP)に基づくアプローチを提案する。
  論文  参考訳（メタデータ） (2021-06-13T23:08:49Z)
• Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning [0.0]
  高品質の安全シールドを合成できる自動検証パイプラインを提案します。 私たちの重要な洞察は、事前に計算された安全シールドを使用して神経コントローラのトレーニングを制限し、神経コントローラから安全検証を分離することを含みます。 実測的な高次元深部RLベンチマークによる実験結果から,本手法の有効性が示された。
  論文  参考訳（メタデータ） (2021-04-20T19:30:29Z)

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

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