XGBoost法により学習させたAIモデルのふるまいの形式検証

• Item type: Symposium(1)
• 公開日: 2021-08-30
• タイトル: XGBoost法により学習させたAIモデルのふるまいの形式検証
• タイトル / 言語: en
• タイトル: Formal Verification of Properties of AI Models Trained by XGBoost Machine-Learning Method
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 形式手法
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: 株式会社日立製作所
• 著者所属: 株式会社日立製作所
• 著者所属: 株式会社日立製作所
• 著者所属: 株式会社日立製作所
• 著者所属(英): en
• 著者所属(英): Research and Development Group, Hitachi, Ltd.
• 著者所属(英): en
• 著者所属(英): Research and Development Group, Hitachi, Ltd.
• 著者所属(英): en
• 著者所属(英): Research and Development Group, Hitachi, Ltd.
• 著者所属(英): en
• 著者所属(英): Research and Development Group, Hitachi, Ltd.
• 著者名: 來間, 啓伸; 明神, 智之; 佐藤, 直人; 小川, 秀人
• 著者名(英): Hironobu, Kuruma; Tomoyuki, Myojin; Naoto, Sato; Hideto, Ogawa
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 論理的に記述し分析することが困難な事象を処理するソフトウェアを構成する方法として，機械学習への期待が高まっている．一方，機械学習によって作成された AI モデルのふるまいを予測することは困難であり，仕様の充足性を確認することを目的とした従来のテスト手法は適用できない．AI モデルのふるまいの形式検証は，指定した入力データ範囲の中で AI モデルの出力データが検証性質を満たすことを網羅的に検証し，不適切なデータが出力されないことを確認できる点で，この課題の解決に有効である [4]．その反面，一般に形式検証には多くの計算が必要であり，検証が現実的な時間内に終了しない場合がある．本稿では XGBoost 法を使って学習させた決定木集合モデルの形式検証について述べるとともに，検証時間と検証精度を制御する手段として近似閾値を用いたモデルの縮約を提案する．米国の住宅価格データベース [7] を学習データとして作成した決定木集合モデルを題材にツールを使ったケーススタディを行い，形式検証のフィージビリティを評価した．検証ノウハウの蓄積とツールの洗練が，今後の課題である．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Machine learning is expected to be a development method of software which process phenomena that are difficult to analyze and describe logically. Since machine learning develops AI models inductively, traditional deductive techniques are not applicable for testing them. Consequently, the behavior of AI models may be inconsistent with the software design. Formal verification of AI models solves this problem by checking that the output data of the model satisfies the given property for every input data specified in the precondition [4]. However, much computing resources are needed for formal verification and frequently verification does not terminate in a practical time. In this paper, we describe a formal verification method for decision tree ensemble models trained using XGBoost machine learning method and propose a model reduction technique which uses approximation threshold to control both verification time and verification accuracy. We evaluated the feasibility of our method through a verification case study of house price prediction model trained on a house sales dataset [7]. Our feature work is to extend the case study to larger models and refine our verification tool.
• 書誌情報: ソフトウェアエンジニアリングシンポジウム2021論文集; 巻 2021, p. 137-142, 発行日 2021-08-30
• 出版者 / 言語: ja
• 出版者: 情報処理学会