文章基本信息

标题：New threat on formal verification for neural networks: example and fault tolerance
本地全文：下载
作者：Augustin Viot ; Benjamin Lussier ; Walter Schön 等
期刊名称：IFAC PapersOnLine
印刷版ISSN：2405-8963
出版年度：2022
卷号：55
期号：6
页码：623-630
DOI：10.1016/j.ifacol.2022.07.197
语种：English
出版社：Elsevier
摘要：AbstractThis article details a new threat to NN formal verification that is well known in the formal verification of classical systems: errors in the learned model of a NN could cause the NN to pass formal verification on a property while violating the same property in real life. The solution to this threat for classical systems (which is expert reviews) is inadequate for NN due to their lack of explainability. Here, we propose a detection and recovery mechanism to tolerate it. This mechanism is based on a mathematical diversification of the system's model and the online verification of the formal safety properties. It was successfully implemented and validated on an application example, which, to our knowledge, is one of the most concrete NN formal verification in the literature: the Adaptive Cruise Control function of an autonomous car.
关键词：KeywordsDependabilityNeural approximations for optimal controlestimationApplications and fault tolerant controlfault tolerant controlreconfigurable control