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

• Item type: Journal(1)
• 公開日: 2022-12-15
• タイトル: XGBoost法により学習させたAIモデルの振舞いの形式検証
• タイトル / 言語: en
• タイトル: Formal Verification of AI Model Bahaviors Trained by XGBoost Machine-learning Method
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [一般論文] AIソフトウェアのテスト，機械学習，決定木集合モデル，プログラム検証，充足可能性問題
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• ID登録: 10.20729/00222737
• ID登録 / ID登録タイプ: JaLC
• 著者所属: 株式会社日立製作所研究開発グループ
• 著者所属: 株式会社日立製作所研究開発グループ
• 著者所属: 株式会社日立製作所研究開発グループ
• 著者所属: 株式会社日立製作所研究開発グループ
• 著者所属(英): 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モデルの振舞いの形式検証は，指定した入力データ範囲の中で推論出力データが検証性質を満たすことを網羅的に検証する点で，この課題の解決に有効なアプローチである．その反面，形式検証には多くの計算が必要であり，現実的な計算資源の下では検証結果が得られない場合もある．本稿では，XGBoost法を使って学習させた決定木集合モデルの振舞いの形式検証手法を提案し，検証の計算量と精度を制御するためのモデルの縮約について述べる．米国の住宅価格データベースを学習データとして作成した決定木集合モデルを題材に，ツールを使ったケーススタディを行い，提案手法のフィージビリティを評価した．大規模AIモデルへの適用を通じて手法を洗練することが，今後の課題である．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Machine learning is expected to be a development method of software, which process phenomena that are difficult to describe and analyze logically. Since machine learning generates AI models inductively, their behaviors are unpredictable. An AI model may output data which is obviously inconsistent with human knowledge. Formal verification of AI models solves this problem by checking that the output of the model satisfies the given property for every input specified in the precondition. However, much computing resources are needed for formal verification and frequently verification does not terminate in a practical time. In this paper, we propose a formal verification method for decision tree ensemble models trained using XGBoost machine learning method and describe a model reduction technique for controlling 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. Our feature work is to apply the proposed method to larger models and refine it.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 63, 号 12, p. 1830-1839, 発行日 2022-12-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764
• 公開者 / 言語: ja
• 公開者 / 出版者: 情報処理学会