論文の概要: Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles
- arxiv url: http://arxiv.org/abs/2105.02595v1
- Date: Thu, 6 May 2021 11:50:22 GMT
- ステータス: 処理完了
- システム内更新日: 2021-05-07 19:34:24.601542
- Title: Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles
- Title（参考訳）: ツリーアンサンブルのためのメモリ効率のよい形式検証ツールのスケールアップ
- Authors: John T\"ornblom and Simin Nadjm-Tehrani
- Abstract要約: ツール記述として提示されたVoTEアルゴリズムを形式化し拡張する。
コア検証エンジンからプロパティチェックを分離することで、汎用性のある要件の検証が可能となります。
数値認識と航空機衝突回避という2つのケーススタディで、このツールの適用を実証します。
- 参考スコア（独自算出の注目度）: 2.588973722689844
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: To guarantee that machine learning models yield outputs that are not only
accurate, but also robust, recent works propose formally verifying robustness
properties of machine learning models. To be applicable to realistic
safety-critical systems, the used verification algorithms need to manage the
combinatorial explosion resulting from vast variations in the input domain, and
be able to verify correctness properties derived from versatile and
domain-specific requirements.
In this paper, we formalise the VoTE algorithm presented earlier as a tool
description, and extend the tool set with mechanisms for systematic scalability
studies. In particular, we show a) how the separation of property checking from
the core verification engine enables verification of versatile requirements, b)
the scalability of the tool, both in terms of time taken for verification and
use of memory, and c) that the algorithm has attractive properties that lend
themselves well for massive parallelisation.
We demonstrate the application of the tool in two case studies, namely digit
recognition and aircraft collision avoidance, where the first case study serves
to assess the resource utilisation of the tool, and the second to assess the
ability to verify versatile correctness properties.
- Abstract（参考訳）: 機械学習モデルが正確であるだけでなく、堅牢である出力を出力することを保証するため、最近の研究では、機械学習モデルの堅牢性特性を正式に検証することを提案する。
実際の安全クリティカルシステムに適用するには,入力領域のばらつきによる組合せ爆発を管理し,汎用性やドメイン固有の要件から導かれる正確性特性を検証することが必要である。
本稿では,前述した投票アルゴリズムをツール記述として定式化し,そのツールセットを体系的スケーラビリティ研究のメカニズムで拡張する。
特に,a) コア検証エンジンからプロパティチェックを分離することで,多様な要件の検証が可能になること,b) 検証に要する時間とメモリ使用の両面でツールのスケーラビリティ,c) アルゴリズムが大規模並列化に適した魅力的な特性を持っていること,などが示されている。
本研究は,2つのケーススタディ,すなわち,デジタル認識と航空機衝突回避の2つのケーススタディにおいて,ツールの資源利用性を評価するための第1ケーススタディと,汎用的正当性検証能力を評価するための第2ケーススタディである。
関連論文リスト
- Quantitative Assurance and Synthesis of Controllers from Activity
Diagrams [4.419843514606336]
確率的モデル検査は、定性的および定量的な性質を自動検証するために広く用いられている形式的検証手法である。
これにより、必要な知識を持っていない研究者やエンジニアにはアクセスできない。
本稿では,確率時間の新しいプロファイル,品質アノテーション,3つのマルコフモデルにおけるADの意味論的解釈,アクティビティ図からPRISM言語への変換ルールのセットなど,ADの総合的な検証フレームワークを提案する。
最も重要なことは、モデルをベースとした手法を用いて、完全自動検証のための変換アルゴリズムを開発し、QASCADと呼ばれるツールで実装したことです。
論文 参考訳（メタデータ） (2024-02-29T22:40:39Z) - Fine-Tuning Enhances Existing Mechanisms: A Case Study on Entity
Tracking [53.66999416757543]
本研究では,微調整が言語モデルに実装された内部メカニズムに与える影響について検討する。
微調整はモデルの機械的操作を変えるのではなく、強化する。
論文 参考訳（メタデータ） (2024-02-22T18:59:24Z) - Improving Adaptive Conformal Prediction Using Self-Supervised Learning [72.2614468437919]
我々は、既存の予測モデルの上に自己教師付きプレテキストタスクを持つ補助モデルを訓練し、自己教師付きエラーを付加的な特徴として用いて、非整合性スコアを推定する。
合成データと実データの両方を用いて、効率(幅)、欠陥、共形予測間隔の超過といった付加情報の利点を実証的に実証する。
論文 参考訳（メタデータ） (2023-02-23T18:57:14Z) - A Correct-and-Certify Approach to Self-Supervise Object Pose Estimators
via Ensemble Self-Training [26.47895284071508]
現実世界のロボティクスアプリケーションは、さまざまなシナリオで確実に動作するオブジェクトのポーズ推定方法を要求する。
最初のコントリビューションは、深度情報を用いたポーズ推定を補正する堅牢な修正モジュールの開発です。
第2の貢献は、複数のポーズ推定器を自己教師型で同時に訓練するアンサンブル自己学習アプローチである。
論文 参考訳（メタデータ） (2023-02-12T23:02:03Z) - Specifying and Testing $k$-Safety Properties for Machine-Learning Models [20.24045879238586]
フォーマルなメソッドで使われる仕様からインスピレーションを得て、$k$の異なる実行、いわゆる$k$-safetyプロパティを表現します。
ここでは、機械学習モデルに対する$k$-safetyプロパティの幅広い適用性を示し、それらを表現するための最初の仕様言語を示す。
我々のフレームワークは、プロパティ違反を特定するのに有効であり、検出されたバグはより良いモデルのトレーニングに使用できる。
論文 参考訳（メタデータ） (2022-06-13T11:35:55Z) - Information-Theoretic Odometry Learning [83.36195426897768]
生体計測推定を目的とした学習動機付け手法のための統合情報理論フレームワークを提案する。
提案フレームワークは情報理論言語の性能評価と理解のためのエレガントなツールを提供する。
論文 参考訳（メタデータ） (2022-03-11T02:37:35Z) - Fantastic Features and Where to Find Them: Detecting Cognitive
Impairment with a Subsequence Classification Guided Approach [6.063165888023164]
本稿では、逐次機械学習モデルとドメイン知識を活用して、パフォーマンス向上に役立つ機能を予測する機能エンジニアリングの新しいアプローチについて説明する。
本手法により得られた特徴を用いた場合,CI分類精度が強いベースラインよりも2.3%向上することが実証された。
論文 参考訳（メタデータ） (2020-10-13T17:57:18Z) - Verification of ML Systems via Reparameterization [6.482926592121413]
確率的プログラムを定理証明器で自動的に表現する方法を示す。
また、ベイズ仮説テストで用いられるヌルモデルは、人口統計学的パリティ(英語版)と呼ばれる公平性基準を満たすことを証明した。
論文 参考訳（メタデータ） (2020-07-14T02:19:25Z) - A Trainable Optimal Transport Embedding for Feature Aggregation and its
Relationship to Attention [96.77554122595578]
固定サイズのパラメータ化表現を導入し、与えられた入力セットから、そのセットとトレーニング可能な参照の間の最適な輸送計画に従って要素を埋め込み、集約する。
我々のアプローチは大規模なデータセットにスケールし、参照のエンドツーエンドのトレーニングを可能にすると同時に、計算コストの少ない単純な教師なし学習メカニズムも提供する。
論文 参考訳（メタデータ） (2020-06-22T08:35:58Z) - Generating Fact Checking Explanations [52.879658637466605]
まだ欠けているパズルの重要なピースは、プロセスの最も精巧な部分を自動化する方法を理解することです。
本稿では、これらの説明を利用可能なクレームコンテキストに基づいて自動生成する方法について、最初の研究を行う。
この結果から,個別に学習するのではなく,両目標を同時に最適化することで,事実確認システムの性能が向上することが示唆された。
論文 参考訳（メタデータ） (2020-04-13T05:23:25Z) - Adaptive Object Detection with Dual Multi-Label Prediction [78.69064917947624]
本稿では,適応オブジェクト検出のための新しいエンド・ツー・エンドの非教師付き深部ドメイン適応モデルを提案する。
モデルはマルチラベル予測を利用して、各画像内の対象カテゴリ情報を明らかにする。
本稿では,オブジェクト検出を支援するための予測整合正則化機構を提案する。
論文 参考訳（メタデータ） (2020-03-29T04:23:22Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。