用形式化方法提升自动驾驶强化学习的可靠性与效率
Model Checking for Reinforcement Learning in Autonomous Driving: One Can Do More Than You Think!
- 通过模型检测预分析传感器精度与学习步长缺陷
- 奖励自动机显著提升多目标学习性能
- 适合关注自动驾驶RL可靠性的研究者
多数强化学习平台使用高级编程语言（如OpenAI Gymnasium的Python），虽提供丰富API和基准测试，但侧重算法设计与训练表现，忽视模型与奖励函数的正确性，而这对自动驾驶（AD）等实际应用至关重要。本文提出采用形式化方法建模AD系统，并展示模型检测（MC）在自动驾驶强化学习中的多重作用。以往研究多聚焦安全防护（如安全盾牌），本文揭示了新应用场景：首先，基于MC的模型预分析可发现传感器精度与学习步长相关的缺陷，为强化学习提供准备，若存在缺陷可节省时间并加深对系统的理解；其次，奖励自动机有助于优化奖励函数设计，在多目标学习中显著提升学习性能。所有结论均经实验验证。
原文摘要 · Abstract (English)
Most reinforcement learning (RL) platforms use high-level programming languages, such as OpenAI Gymnasium using Python. These frameworks provide various API and benchmarks for testing RL algorithms in different domains, such as autonomous driving (AD) and robotics. These platforms often emphasise the design of RL algorithms and the training performance but neglect the correctness of models and reward functions, which can be crucial for the successful application of RL. This paper proposes using formal methods to model AD systems and demonstrates how model checking (MC) can be used in RL for AD. Most studies combining MC and RL focus on safety, such as safety shields. However, this paper shows different facets where MC can strengthen RL. First, an MC-based model pre-analysis can reveal bugs with respect to sensor accuracy and learning step size. This step serves as a preparation of RL, which saves time if bugs exist and deepens users' understanding of the target system. Second, reward automata can benefit the design of reward functions and greatly improve learning performance especially when the learning objectives are multiple. All these findings are supported by experiments.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。