講演抄録/キーワード |
講演名 |
2020-03-03 11:00
様相μ計算によるRNNのモデル検査 ○青島達大・碓井利宣(NTT) ICSS2019-88 |
抄録 |
(和) |
機械学習モデルは,自動運転やロボティクス,工場の作業自動化など,様々なサイバーフィジカルシステムへ適用されている.しかしながら,発電所などのより重要なシステムへの採用は,安全性に関する保証がないこと
から,困難である.本論文では,機械学習モデル,特に再帰ニューラルネットワークにより制御されるシステムのセキュリティについて考える.提案手法は,与えられた再帰ニューラルネットワークが与えられた仕様を満たすかどうかを検査するもので,モデルを制約zonotope により抽象的に解釈することで実現する.仕様は,時相論理の一種であるLinear Temporal Logic やComputation Tree Logic 等の一般化である様相μ 計算により記述できる. |
(英) |
Machine learning models have been applied to many cyber-physical systems such as self-driving cars, robotics, and factory automation. However, it would be difficult to adapt them to more mission-critical systems, such as energy plants, because there is no safety guarantee. This paper presents the security of systems controlled using machine learning models, especially, Recurrent Neural Networks (RNNs). We propose a novel method for checking whether a given RNN satisfies a given specification, as abstractly interpreting the model with the con-
strained zonotopes. The specification is written in the modal μ-calculus containing many classical temporal logics such as Linear Temporal Logic and Computation Tree Logic. |
キーワード |
(和) |
モデル検査 / 再起ニューラルネットワーク / 様相μ計算 / 制約zonotope / / / / |
(英) |
Model checking / Recurrent Neural Networks / Modal μ-calculus / Constrained zonotopes / / / / |
文献情報 |
信学技報, vol. 119, no. 437, ICSS2019-88, pp. 119-124, 2020年3月. |
資料番号 |
ICSS2019-88 |
発行日 |
2020-02-24 (ICSS) |
ISSN |
Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
ICSS2019-88 |