論文の概要: 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ソルバを用いて正当性を正式に保証する。
我々は,プロトタイプソフトウェアツールを開発し,大規模かつ多様なベンチマークスイート上での制御と証明書合成による検証の有効性を評価する。
関連論文リスト
- 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) - Recursively Feasible Probabilistic Safe Online Learning with Control
Barrier Functions [63.18590014127461]
本稿では,CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
本研究では,ロバストな安全クリティカルコントローラの実現可能性について検討する。
次に、これらの条件を使って、イベントトリガーによるオンラインデータ収集戦略を考案します。
論文 参考訳(メタデータ) (2022-08-23T05:02:09Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。