面向学习型自主系统验证的假设生成
人工智能
2023-05-31 v1 机器学习
摘要
为自主系统提供安全保证十分困难，因为这些系统在复杂环境中运行，需要使用学习型组件，如用于视觉感知的深度神经网络（DNN）。DNN因其规模（可有数千或数百万参数）、缺乏形式化规范（DNN通常从标记数据中学习，无任何形式需求）以及对环境微小变化的敏感性而难以分析。我们提出一种假设-保证风格的组合方法，用于对此类自主系统系统级安全属性进行形式化验证。我们的洞见是：通过自动合成关于DNN行为的假设（保证所需安全属性满足），可在无DNN感知组件情况下分析系统。所合成假设在某种意义下最弱——它们刻画了所有可行DNN的输出序列，这些DNN接入自主系统后可保证所需安全属性。该假设可用作部署DNN上的运行时监视器以保证整体系统安全；也可被挖掘以提取局部规范用于DNN训练与测试。我们在来自自主飞机领域、使用复杂DNN进行感知的案例研究中说明了本方法。
引用
@article{arxiv.2305.18372,
title = {Assumption Generation for the Verification of Learning-Enabled Autonomous Systems},
author = {Corina Pasareanu and Ravi Mangal and Divya Gopinath and Huafeng Yu},
journal= {arXiv preprint arXiv:2305.18372},
year = {2023}
}