論文の概要: ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
- arxiv url: http://arxiv.org/abs/2511.02164v1
- Date: Tue, 04 Nov 2025 01:09:08 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-11-05 18:47:05.767056
- Title: ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
- Title（参考訳）: ScenicProver:学習可能システムの構成確率的検証のためのフレームワーク
- Authors: Eric Vin, Kyle A. Miller, Inigo Incer, Sanjit A. Seshia, Daniel J. Fremont,
- Abstract要約: 本稿では,学習可能なサイバー物理システムのための検証フレームワークであるScenicProverを紹介する。
解釈可能なコードからブラックボックスまで、明確なコンポーネントインターフェースを備えた構成システム記述をサポートする。
センサフュージョンを用いた自律走行車両の緊急制動システムのケーススタディにより,この枠組みの有効性を実証する。
- 参考スコア（独自算出の注目度）: 3.4880795442123733
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Full verification of learning-enabled cyber-physical systems (CPS) has long been intractable due to challenges including black-box components and complex real-world environments. Existing tools either provide formal guarantees for limited types of systems or test the system as a monolith, but no general framework exists for compositional analysis of learning-enabled CPS using varied verification techniques over complex real-world environments. This paper introduces ScenicProver, a verification framework that aims to fill this gap. Built upon the Scenic probabilistic programming language, the framework supports: (1) compositional system description with clear component interfaces, ranging from interpretable code to black boxes; (2) assume-guarantee contracts over those components using an extension of Linear Temporal Logic containing arbitrary Scenic expressions; (3) evidence generation through testing, formal proofs via Lean 4 integration, and importing external assumptions; (4) systematic combination of generated evidence using contract operators; and (5) automatic generation of assurance cases tracking the provenance of system-level guarantees. We demonstrate the framework's effectiveness through a case study on an autonomous vehicle's automatic emergency braking system with sensor fusion. By leveraging manufacturer guarantees for radar and laser sensors and focusing testing efforts on uncertain conditions, our approach enables stronger probabilistic guarantees than monolithic testing with the same computational budget.
- Abstract（参考訳）: 学習可能なサイバー物理システム(CPS)の完全な検証は、ブラックボックスコンポーネントや複雑な現実世界環境などの課題により、長年にわたって難航してきた。
既存のツールは、限られた種類のシステムに対して正式な保証を提供するか、モノリスとしてシステムをテストするかのいずれかを提供するが、複雑な実環境上で様々な検証技術を用いて学習可能なCPSを構成するための一般的なフレームワークは存在しない。
本稿では,このギャップを埋めるための検証フレームワークであるScenicProverを紹介する。
本フレームワークは,(1)解釈可能なコードからブラックボックスまで,明確なコンポーネントインターフェースによる構成システム記述,(2)任意のシナリオ表現を含む線形時間論理の拡張を用いた仮定保証契約,(3)テストによるエビデンス生成,Lean 4統合による形式的証明,および外部仮定のインポート,(4)契約演算子を用いた生成エビデンスの体系的組み合わせ,(5)システムレベルの保証の証明を追跡する保証ケースの自動生成をサポートする。
センサフュージョンを用いた自律走行車両の自動緊急ブレーキシステムのケーススタディにより, 本フレームワークの有効性を実証した。
レーダとレーザーセンサのメーカー保証を活用し,不確実な条件に焦点を合わせることで,同じ計算予算によるモノリシックテストよりも高い確率保証を実現する。
関連論文リスト
- Composable Attestation: A Generalized Framework for Continuous and Incremental Trust in AI-Driven Distributed Systems [4.2822349607372265]
本稿では,分散システムにおける連続的・漸進的信頼のための汎用的な暗号フレームワークとして,コンポーザブル証明を提案する。
このような証明システムのコア特性を定義する厳密な数学的基盤を確立する。
このフレームワークのユーティリティは、セキュアなAIモデルの完全性検証、フェデレーション学習、ランタイム信頼保証といったアプリケーションにまで拡張されている。
論文 参考訳（メタデータ） (2026-03-02T22:45:26Z) - LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems [0.8574682463936006]
従来の形式的検証ツールは、不透明なブラックボックスAIコンポーネントと複雑なダイナミクスの両方を組み込んだシステムに直面したときに不足する。
我々は,ブラックボックス埋め込み動的システムの安全性を証明するための検証エンジンであるLUCIDを紹介する。
LUCIDは、このようなシステムの安全性を定量化する最初のツールである。
論文 参考訳（メタデータ） (2025-12-12T17:46:50Z) - Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis [49.31947916567367]
Hamilton-Jacobi (J) リーチビリティ解析は、最悪の不確実性の下で最適なリーチビリティを計算できる一般的な非線形システムに対する一般的な形式的検証ツールである。
この作業は、HJローバーを介してRobust Verification Controllersのための、HJベースのリーチビリティベースのシステム検証フレームワークである。
本稿では,Ro-CoReの安全性検証とコントローラ設計のための新しい手法を提案する。
論文 参考訳（メタデータ） (2025-11-18T18:55:20Z) - BarrierBench : Evaluating Large Language Models for Safety Verification in Dynamical Systems [4.530582224312311]
バリア証明書合成のための LLM ベースのエージェントフレームワークを提案する。
このフレームワークは自然言語推論を使用して、候補証明書を提案し、洗練し、検証する。
BarrierBenchは、線形、非線形、離散時間、連続時間設定にまたがる100の動的システムのベンチマークである。
論文 参考訳（メタデータ） (2025-11-12T14:23:49Z) - DSperse: A Framework for Targeted Verification in Zero-Knowledge Machine Learning [0.0]
DSperseは、暗号検証による分散機械学習推論のためのフレームワークである。
複数の証明システムを用いてDSperseを評価し,メモリ使用量,実行時間,回路動作に関する実験結果を報告する。
論文 参考訳（メタデータ） (2025-08-09T12:38:18Z) - BlueGlass: A Framework for Composite AI Safety [0.2999888908665658]
本稿では,統合されたインフラストラクチャを提供することで,AIの安全性を促進するためのフレームワークであるBlueGlassを紹介する。
本フレームワークの有用性を実証するために,視覚言語評価における安全性指向の3つの分析法を提案する。
より広い範囲で、この研究は、より堅牢で信頼性の高いAIシステムを構築するためのインフラストラクチャと発見に貢献している。
論文 参考訳（メタデータ） (2025-07-14T09:45:34Z) - Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。
実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文 参考訳（メタデータ） (2025-05-28T17:57:47Z) - A Hybrid Framework for Statistical Feature Selection and Image-Based Noise-Defect Detection [55.2480439325792]
本稿では,統計的特徴選択と分類技術を統合し,欠陥検出精度を向上させるハイブリッドフレームワークを提案する。
工業画像から抽出した55個の特徴を統計的手法を用いて解析した。
これらの手法をフレキシブルな機械学習アプリケーションに統合することにより、検出精度を改善し、偽陽性や誤分類を減らす。
論文 参考訳（メタデータ） (2024-12-11T22:12:21Z) - A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳（メタデータ） (2023-09-12T09:37:26Z) - Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。
これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
論文 参考訳（メタデータ） (2022-08-23T05:02:09Z) - A Verification Framework for Certifying Learning-Based Safety-Critical
Aviation Systems [6.168537302126847]
本稿では,航空システムにおける学習ベースコンポーネントの設計時および実行時保証のための安全性検証フレームワークを提案する。
設計時保証の観点から,シミュレーション環境における異なるレベルの粒度からの知識を組み込んだオフライン混合忠実度検証ツールを提案する。
実行時保証の観点から,学習に基づく意思決定モデルのための到達可能性および統計に基づくオンラインモニタリングと安全ガードを提案する。
論文 参考訳（メタデータ） (2022-05-09T22:56:00Z) - Learning Hybrid Control Barrier Functions from Data [66.37785052099423]
ハイブリッドシステムの安全な制御法則を得るための体系的なツールが欠如していることから,データから確実に安全な制御法則を学習するための最適化ベースのフレームワークを提案する。
特に、システムダイナミクスが知られており、安全なシステム動作を示すデータが利用可能であるような設定を仮定する。
論文 参考訳（メタデータ） (2020-11-08T23:55:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。