論文の概要: 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)システムレベルの保証の証明を追跡する保証ケースの自動生成をサポートする。 センサフュージョンを用いた自律走行車両の自動緊急ブレーキシステムのケーススタディにより, 本フレームワークの有効性を実証した。 レーダとレーザーセンサのメーカー保証を活用し,不確実な条件に焦点を合わせることで,同じ計算予算によるモノリシックテストよりも高い確率保証を実現する。

関連論文リスト

• 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 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)

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

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