論文の概要: A General Verification Framework for Dynamical and Control Models via Certificate Synthesis

• arxiv url: http://arxiv.org/abs/2309.06090v1
• Date: Tue, 12 Sep 2023 09:37:26 GMT
• ステータス: 処理完了
• システム内更新日: 2023-09-13 13:41:16.973599
• Title: A General Verification Framework for Dynamical and Control Models via Certificate Synthesis
• Title（参考訳）: 証明書合成による動的・制御モデルの一般的な検証フレームワーク
• Authors: Alec Edwards, Andrea Peruffo, Alessandro Abate
• Abstract要約: システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
• 参考スコア（独自算出の注目度）: 60.03938402120854
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: An emerging branch of control theory specialises in certificate learning, concerning the specification of a desired (possibly complex) system behaviour for an autonomous or control model, which is then analytically verified by means of a function-based proof. However, the synthesis of controllers abiding by these complex requirements is in general a non-trivial task and may elude the most expert control engineers. This results in a need for automatic techniques that are able to design controllers and to analyse a wide range of elaborate specifications. In this paper, we provide a general framework to encode system specifications and define corresponding certificates, and we present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks to provide candidate control and certificate functions, whilst using SMT-solvers to offer a formal guarantee of correctness. We test our framework by developing a prototype software tool, and assess its efficacy at verification via control and certificate synthesis over a large and varied suite of benchmarks.
• Abstract（参考訳）: 制御理論の新しい分野は、自律的または制御モデルに対する所望の(おそらく複雑な)システム動作の仕様に関する証明書学習を専門とし、関数ベースの証明によって分析的に検証される。 しかし、これらの複雑な要件を満たしたコントローラの合成は、一般的には非自明なタスクであり、最も熟練した制御エンジニアから遠ざかる可能性がある。 これにより、コントローラを設計し、広範囲の精巧な仕様を分析できる自動技術が必要である。 本稿では,システム仕様をエンコードし,対応する証明書を定義するための汎用フレームワークを提供し,コントローラと証明書を形式的に合成する自動アプローチを提案する。 提案手法は安全学習の幅広い分野に寄与し、ニューラルネットワークの柔軟性を活用して候補制御と証明機能を提供し、SMTソルバを用いて正当性を正式に保証する。 我々は,プロトタイプソフトウェアツールを開発し,大規模かつ多様なベンチマークスイート上での制御と証明書合成による検証の有効性を評価する。

関連論文リスト

• Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems [0.5249805590164903]
  KI-LOKプロジェクトは、AIコンポーネントを自律列車に安全に統合するための新しい方法を模索している。 我々は,(1)B法を用いた形式解析によるステアリングシステムの安全性確保,(2)ランタイム証明書チェッカーによる認識システムの信頼性向上という2層的なアプローチを追求する。 この作業は、実際のAI出力と実際の証明書チェッカーによって制御されるフォーマルモデル上でシミュレーションを実行するデモレータ内の両方の戦略をリンクする。
  論文  参考訳（メタデータ） (2024-11-21T18:09:04Z)
• Transfer of Safety Controllers Through Learning Deep Inverse Dynamics Model [4.7962647777554634]
  制御障壁証明書は、制御システムの安全性を正式に保証する上で有効であることが証明されている。 制御障壁証明書の設計は、時間がかかり、計算に費用がかかる作業である。 本稿では,制御器の正当性を保証する妥当性条件を提案する。
  論文  参考訳（メタデータ） (2024-05-22T15:28:43Z)
• Fine-Tuning Language Models Using Formal Methods Feedback [53.24085794087253]
  我々は、自律システムにおけるアプリケーションのための、微調整済み言語モデルに対して、完全に自動化されたアプローチを提案する。 本手法は,自然言語タスク記述による事前学習モデルから自動制御器を合成する。 その結果、コントローラが満たした仕様の割合が60%から90%に改善したことが示唆された。
  論文  参考訳（メタデータ） (2023-10-27T16:24:24Z)
• Value Functions are Control Barrier Functions: Verification of Safe Policies using Control Theory [46.85103495283037]
  本稿では,制御理論から学習値関数への検証手法の適用方法を提案する。 我々は値関数と制御障壁関数の間の関係を確立する原定理を定式化する。 我々の研究は、RLベースの制御システムの汎用的でスケーラブルで検証可能な設計のための公式なフレームワークに向けた重要な一歩である。
  論文  参考訳（メタデータ） (2023-06-06T21:41:31Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)
• Sparsity in Partially Controllable Linear Systems [56.142264865866636]
  本研究では, 部分制御可能な線形力学系について, 基礎となる空間パターンを用いて検討する。 最適制御には無関係な状態変数を特徴付ける。
  論文  参考訳（メタデータ） (2021-10-12T16:41:47Z)
• Safety Verification of Model Based Reinforcement Learning Controllers [7.407039316561176]
  本稿では,モデルベースRLコントローラのリーチブル・セット解析を用いた新しい安全性検証フレームワークを提案する。 提案したフレームワークは、ニューラルネットワークを用いて表現されるモデルとコントローラを効率的に扱うことができる。
  論文  参考訳（メタデータ） (2020-10-21T03:35:28Z)
• Learning Stability Certificates from Data [19.381365606166725]
  我々は,軌道データのみから認証関数を学習するアルゴリズムを開発した。 このような一般化誤差境界を大域的安定性保証に変換する。 複雑な力学の証明を効率的に学習できることを実証的に実証する。
  論文  参考訳（メタデータ） (2020-08-13T14:58:42Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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