論文の概要: Formal Verification of End-to-End Learning in Cyber-Physical Systems:
Progress and Challenges
- arxiv url: http://arxiv.org/abs/2006.09181v1
- Date: Mon, 15 Jun 2020 16:50:47 GMT
- ステータス: 処理完了
- システム内更新日: 2022-11-21 02:22:14.542274
- Title: Formal Verification of End-to-End Learning in Cyber-Physical Systems:
Progress and Challenges
- Title（参考訳）: サイバー物理システムにおけるエンドツーエンド学習の形式的検証:進展と課題
- Authors: Nathan Fulton, Nathan Hunt, Nghia Hoang, Subhro Das
- Abstract要約: コンピュータチェックによる正式な正当性を構築することで、自律システムの安全性を確保することができるかもしれない。
本稿では,既存の形式的検証手法に基づく3つの仮定について述べる。
形式的検証による証拠の強度向上に向けた予備的な研究を要約する。
- 参考スコア（独自算出の注目度）: 7.955313479061443
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Autonomous systems -- such as self-driving cars, autonomous drones, and
automated trains -- must come with strong safety guarantees. Over the past
decade, techniques based on formal methods have enjoyed some success in
providing strong correctness guarantees for large software systems including
operating system kernels, cryptographic protocols, and control software for
drones. These successes suggest it might be possible to ensure the safety of
autonomous systems by constructing formal, computer-checked correctness proofs.
This paper identifies three assumptions underlying existing formal verification
techniques, explains how each of these assumptions limits the applicability of
verification in autonomous systems, and summarizes preliminary work toward
improving the strength of evidence provided by formal verification.
- Abstract（参考訳）: 自動運転車、無人ドローン、自動列車などの自律システムは、強力な安全性を保証する必要がある。
過去10年間で、形式的手法に基づく技術は、オペレーティングシステムカーネル、暗号プロトコル、ドローンの制御ソフトウェアなど、大規模ソフトウェアシステムに対して強力な正確性保証を提供することに成功した。
これらの成功は、正式なコンピュータチェックによる正当性証明を構築することによって、自律システムの安全性を確保することができることを示唆している。
本稿では,既存の形式的検証手法に基づく3つの仮定を特定し,これらの仮定が自律システムにおける検証の適用性をいかに制限しているかを説明し,形式的検証による証拠の強度向上に向けた予備的な取り組みを要約する。
関連論文リスト
- 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) - Towards Formal Fault Injection for Safety Assessment of Automated
Systems [0.0]
本稿では,開発ライフサイクルを通じてこれら2つのテクニックを融合したフォーマルなフォールトインジェクションを紹介する。
我々は,形式的手法と断層注入の相互支援の5つの領域を同定し,より密着的なアプローチを提唱する。
論文 参考訳（メタデータ） (2023-11-16T11:34:18Z) - Testing learning-enabled cyber-physical systems with Large-Language Models: A Formal Approach [32.15663640443728]
機械学習(ML)をサイバー物理システム(CPS)に統合することは大きな利益をもたらす。
既存の検証と検証技術は、しばしばこれらの新しいパラダイムには不十分である。
本稿では, 基礎確率テストからより厳密なアプローチへ移行し, 正式な保証を実現するためのロードマップを提案する。
論文 参考訳（メタデータ） (2023-11-13T14:56:14Z) - Formal Methods for Autonomous Systems [21.989467515686858]
形式的手法は安全クリティカルシステムの正当性を確立する上で重要な役割を果たしてきた。
形式的なメソッドの主なビルディングブロックはモデルと仕様です。
様々な定式化の下で, 正しい構成合成を考察する。
論文 参考訳（メタデータ） (2023-11-02T14:18:43Z) - A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳（メタデータ） (2023-09-12T09:37:26Z) - When Authentication Is Not Enough: On the Security of Behavioral-Based Driver Authentication Systems [53.2306792009435]
我々はランダムフォレストとリカレントニューラルネットワークアーキテクチャに基づく2つの軽量ドライバ認証システムを開発した。
我々は,SMARTCANとGANCANという2つの新しいエスケープアタックを開発することで,これらのシステムに対する攻撃を最初に提案する。
コントリビューションを通じて、これらのシステムを安全に採用する実践者を支援し、車の盗難を軽減し、ドライバーのセキュリティを高める。
論文 参考訳（メタデータ） (2023-06-09T14:33:26Z) - Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
本稿は、正式に認証されたシステムを作成し、実際に使用するためにデプロイした各種のアプリケーション分野のプロジェクトについて検討する。
使用する技術、適用の形式、得られた結果、そしてソフトウェア産業が形式的な検証技術やツールの恩恵を受ける能力について示すべき教訓を考察する。
論文 参考訳（メタデータ） (2023-01-05T18:18:46Z) - Differentiable Control Barrier Functions for Vision-based End-to-End
Autonomous Driving [100.57791628642624]
本稿では,視覚に基づくエンドツーエンド自動運転のための安全保証学習フレームワークを提案する。
我々は、勾配降下によりエンドツーエンドに訓練された微分制御バリア関数(dCBF)を備えた学習システムを設計する。
論文 参考訳（メタデータ） (2022-03-04T16:14:33Z) - A Review of Formal Methods applied to Machine Learning [0.6853165736531939]
機械学習システムの検証の新たな分野に適用される最先端の形式的手法を検討します。
我々はまず,安全クリティカルな分野であるavionic softwareにおいて確立された形式的手法とその現状を思い出す。
次に、機械学習のためにこれまでに開発された形式的手法を包括的かつ詳細にレビューし、その強みと限界を強調します。
論文 参考訳（メタデータ） (2021-04-06T12:48:17Z) - Trustworthy AI [75.99046162669997]
入力データの小さな敵対的変化への脆さ、決定の説明能力、トレーニングデータのバイアスに対処する能力は、最も顕著な制限である。
我々は,AIシステムに対するユーザおよび公的な信頼を高める上での6つの重要な問題に対処するために,信頼に値するAIに関するチュートリアルを提案する。
論文 参考訳（メタデータ） (2020-11-02T20:04:18Z) - Dos and Don'ts of Machine Learning in Computer Security [74.1816306998445]
大きな可能性にもかかわらず、セキュリティにおける機械学習は、パフォーマンスを損なう微妙な落とし穴を引き起こす傾向がある。
我々は,学習ベースのセキュリティシステムの設計,実装,評価において共通の落とし穴を特定する。
我々は,落とし穴の回避や軽減を支援するために,研究者を支援するための実用的な勧告を提案する。
論文 参考訳（メタデータ） (2020-10-19T13:09:31Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。