面向线性时序逻辑任务的神经符号运动与任务规划

本文提出了一个神经符号框架，用于解决涉及时序目标的移动机器人运动规划问题。时序目标使用诸如线性时序逻辑 (LTL) 等时序逻辑公式来描述，以捕捉复杂的任务。所提出的框架训练基于神经网络 (NN) 的规划器，当应用于未见任务时具有强大的正确性保证，即在 NN 训练期间，确切任务（包括工作空间、LTL 公式和机器人的动态约束）是未知的。我们实现理论保证和计算效率的方法基于两点见解。首先，我们将符号模型纳入 NN 的训练中，使得生成的基于 NN 的规划器继承符号模型的可解释性和正确性保证。此外，符号模型作为离散的“记忆”，这对于满足时序逻辑公式是必要的。其次，我们在离线状态下训练一个神经网络库，并在运行时任务明确时，将训练好的 NN 的一个子集组合成一个单一的基于 NN 的规划器。特别地，我们开发了一种新颖的受约束 NN 训练过程，命名为形式化 NN 训练，以强制库中的每个神经网络代表符号模型中的一个“符号”。因此，我们的神经符号框架享有机器学习的可扩展性和灵活性优势，并继承了来自控制理论和形式化方法技术的可证明保证。我们在仿真和实际机器人车辆上均证明了我们框架的有效性，并展示了我们的框架能够泛化到最先进的元强化学习技术无法胜任的未知任务。