时序逻辑约束下 POMDP 中基于 RNN 策略的可验证方法
人工智能
2020-02-14 v1
摘要
循环神经网络（RNNs）已成为序贯决策问题中控制策略的有效表示。然而，基于 RNN 的策略应用的一个主要缺点在于难以对行为规范（例如安全性和/或可到达性）的满足提供形式化保证。通过整合形式化方法与机器学习技术，我们提出一种从 RNN 自动提取有限状态控制器（FSC）的方法，该控制器在与有限状态系统模型组合后，可适用于现有的形式化验证工具。具体而言，我们引入对所谓量化瓶颈插入技术的迭代修改，以创建作为带记忆的随机策略的 FSC。对于所得 FSC 不满足规范的情况，验证生成诊断信息。我们利用该信息来调整所提取 FSC 中的记忆量或执行 RNN 的聚焦重训练。虽然普遍适用，我们在部分可观测马尔可夫决策过程（POMDPs）的策略综合背景下详述了所得迭代过程，该问题以极其困难而著称。数值实验表明，所提方法在最优基准值的 2% 范围内，比传统 POMDP 综合方法快 3 个数量级。
引用
@article{arxiv.2002.05615,
title = {Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints},
author = {Steven Carr and Nils Jansen and Ufuk Topcu},
journal= {arXiv preprint arXiv:2002.05615},
year = {2020}
}
备注
8 pages, 5 figures, 1 table