論文の概要: Parallel and Multi-Objective Falsification with Scenic and VerifAI

• arxiv url: http://arxiv.org/abs/2107.04164v1
• Date: Fri, 9 Jul 2021 01:08:49 GMT
• ステータス: 処理完了
• システム内更新日: 2021-07-13 02:27:45.297011
• Title: Parallel and Multi-Objective Falsification with Scenic and VerifAI
• Title（参考訳）: シナリオとVerifAIによる並列・多目的ファルシフィケーション
• Authors: Kesav Viswanadha, Edward Kim, Francis Indaheng, Daniel J. Fremont, Sanjit A. Seshia
• Abstract要約: シナリオ仕様言語とVerifAIツールキットの拡張について述べる。 まず,Scanicのシミュレーションとサンプリング機能の両方にインタフェースを組み込んだ並列化フレームワークを提案する。 次に、サンプリング中の多目的最適化をサポートするために、VerifAIのファルシフィケーションアルゴリズムの拡張を示す。
• 参考スコア（独自算出の注目度）: 11.152087017964584
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Falsification has emerged as an important tool for simulation-based verification of autonomous systems. In this paper, we present extensions to the Scenic scenario specification language and VerifAI toolkit that improve the scalability of sampling-based falsification methods by using parallelism and extend falsification to multi-objective specifications. We first present a parallelized framework that is interfaced with both the simulation and sampling capabilities of Scenic and the falsification capabilities of VerifAI, reducing the execution time bottleneck inherently present in simulation-based testing. We then present an extension of VerifAI's falsification algorithms to support multi-objective optimization during sampling, using the concept of rulebooks to specify a preference ordering over multiple metrics that can be used to guide the counterexample search process. Lastly, we evaluate the benefits of these extensions with a comprehensive set of benchmarks written in the Scenic language.
• Abstract（参考訳）: Falsificationは、自律システムのシミュレーションベースの検証のための重要なツールとして登場した。 本稿では,並列性を活用し,多目的仕様までファルシフィケーションを拡張することで,サンプリングベースファルシフィケーション法のスケーラビリティを向上するシナリオ仕様言語とVerifAIツールキットの拡張について述べる。 まず,Scanic のシミュレーションとサンプリング機能と VerifAI のファルシフィケーション機能の両方にインターフェースされた並列化フレームワークを提案する。 次に,本アルゴリズムを拡張して,サンプリング中の多目的最適化を支援する。ルールブックの概念を用いて,逆例探索プロセスの導出に使用できる複数のメトリクスに対する優先順序を指定する。 最後に、これらの拡張の利点を、シークエンス言語で書かれた包括的なベンチマークセットで評価する。

関連論文リスト

• Amortizing intractable inference in large language models [59.77924190534093]
  難治性後部分布のサンプルとして, 償却ベイズ推定を用いる。 我々は,LLMファインチューニングの分散マッチングパラダイムが,最大習熟の代替となることを実証的に実証した。 重要な応用として、チェーン・オブ・ソート推論を潜在変数モデリング問題として解釈する。
  論文  参考訳（メタデータ） (2023-10-06T16:36:08Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。 本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。 我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
  論文  参考訳（メタデータ） (2023-05-26T14:55:35Z)
• DeforestVis: Behavior Analysis of Machine Learning Models with Surrogate Decision Stumps [49.97564931094598]
  複雑なMLモデルの振る舞いをユーザフレンドリに要約するビジュアル分析ツールであるDeforestVisを提案する。 DeforestVisは、より多くの切り株をインクリメンタルに生成することで、複雑さとフィデリティのトレードオフを探索するのに役立つ。 DeforestVisの適用性と有用性について,2つのユースケースと,データアナリストとモデル開発者とのエキスパートインタビューで紹介する。
  論文  参考訳（メタデータ） (2023-03-31T21:17:15Z)
• Near-optimal Policy Identification in Active Reinforcement Learning [84.27592560211909]
  AE-LSVI はカーネル化された最小二乗値 RL (LSVI) アルゴリズムの新しい変種であり、楽観主義と悲観主義を組み合わせて活発な探索を行う。 AE-LSVIは初期状態に対するロバスト性が必要な場合、様々な環境で他のアルゴリズムよりも優れていることを示す。
  論文  参考訳（メタデータ） (2022-12-19T14:46:57Z)
• Efficiently Controlling Multiple Risks with Pareto Testing [34.83506056862348]
  本稿では,多目的最適化と複数仮説テストを組み合わせた2段階プロセスを提案する。 自然言語処理(NLP)アプリケーションにおいて,大規模トランスフォーマーモデルの実行を確実に高速化する手法の有効性を実証する。
  論文  参考訳（メタデータ） (2022-10-14T15:54:39Z)
• Falsification of Cyber-Physical Systems using Bayesian Optimization [0.5407319151576264]
  シミュレーションに基づくCPSのファルシフィケーションは、システムの正確性に対する信頼性を高めるための実用的なテスト手法である。 各シミュレーションは典型的に計算集約的であるため、仕様をファルシフィケーションするために必要なシミュレーションの数を減らすことが重要なステップである。 本研究では,入力信号のパラメトリゼーションと仕様評価の関係を記述したサロゲートモデルを,サンプル効率で学習するベイズ最適化(BO)について検討する。
  論文  参考訳（メタデータ） (2022-09-14T15:52:19Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Efficient Neural Network Analysis with Sum-of-Infeasibilities [64.31536828511021]
  凸最適化における総和係数法に着想を得て,広範な分岐関数を持つネットワーク上での検証クエリを解析するための新しい手法を提案する。 標準ケース分析に基づく完全探索手順の拡張は、各検索状態で実行される凸手順をDeepSoIに置き換えることによって達成できる。
  論文  参考訳（メタデータ） (2022-03-19T15:05:09Z)
• Parallel Predictive Entropy Search for Multi-objective Bayesian Optimization with Constraints [0.0]
  実世界の問題は、しばしば複数の制約の下で複数の目的を最適化する。 本稿では,ブラックボックス関数の同時最適化のための情報ベースバッチ手法であるPESMOCを紹介する。 繰り返して、PESMOCはブラックボックスを評価するための入力場所のバッチを選択する。
  論文  参考訳（メタデータ） (2020-04-01T17:37:58Z)
• Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
  本稿では,リアプノフ関数の自動合成法を提案する。 我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワークを構築する,反例誘導方式を採用する。 提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。
  論文  参考訳（メタデータ） (2020-03-19T17:21:02Z)

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

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