验证 LLM-基于 LLM 的机器人预执行任务计划验证-计算机科学-大语言模型-机器人.pdfVIP

验证LLM：基于LLM的机器人预执行任务计划验证

DanilS.Grigorev,AlexeyK.Kovalev,andAleksandrI.Panov

Abstract—在机器人学领域，研究人员面临确保可靠和高

效任务规划的关键挑战。在执行前验证高层次的任务计划显著

减少了错误并提高了这些系统的整体性能。本文提出了一种架

构，用于自动验证仿真或现实世界环境中的高层任务计划。利用

大型语言模型（LLMs），我们的方法包括两个关键步骤：首先，

将自然语言指令转换为线性时态逻辑（LTL），然后对动作序

列进行综合分析。该模块使用LLM的推理能力来评估逻辑连

本贯性并识别计划中的潜在空白。在复杂程度不同的数据集上进

行的严格测试证明了该模块在家用任务上的广泛适用性。我们

译致力于提高任务规划的可靠性和效率，并解决自主系统中执行

中前验证的关键需求。代码可在https://verifyllm.github.io

获取。

1

v

8I.介绍

1

1在执行前验证机器人行动计划仍然是机器人学中的

5一个挑战性任务[1],[2]。现代规划系统生成的行动序列Fig.1.验证LLM工作流以制定验证任务计划。系统将生成的动作

0.乍看之下似乎是正确的，但其中包含只有在执行过程中计划作为输入，并在其上下文窗口内进行分析。每个窗口都由LLM处

7理，以识别位置错误、缺少的先决条件和冗余动作。根据此分析，系统

0才显现出来的隐藏错误。例如，机器人可能会尝试将水提出改进措施，包括重新排序、添加必要步骤和删除重复项。输出是一

5倒入倒置的玻璃或封闭容器中。这些错误并非源于机器个经过优化的动作计划，保持逻辑一致性和完整性。示例演示了茶准备

2

:人的物理限制，而是由于行动计划未能结合人类自然考计划的验证过程，在该过程中，系统识别并纠正了操作顺序问题和缺少

v的先决条件。

i虑到的常识和基本物理约束。

x

r传统的基于PDDL[3]的规划系统在处理需要常识推

a个将LTL与大语言模型（LLMs）结合的新框架，如图1

理的任务时遇到困难，常常忽视了必要的前提条件（例

所示。我们的系统首先将行动计划翻译成LTL公式，提

如，在填充容器之前检查它是否为空[4]），并且未能考虑

供一种正式表示形式以捕捉时间依赖性和逻辑约束。然

行动的结果（例如，在与冰箱互动后检查其是否关闭）。

后大语言模型分析相应的动作序列。这种组合利用了大

最近的方法已经从传统的规划方法演变为基于学习的技

语言模型的上下文理解和常识推理能力[16]来在执行前

术[5]，这些技术更好地处理了不确定性和复杂环境。基

检测潜在错误。为了严格评估我们的框架，我们引入了

于大型语言模型(LLM)的框架在机器人任务规划中展示

两个带有LTL规格注释的专业数据集：ALFRED-LTL、

了有希望的结果[6]–[10]。然而，大多数研究主要集中在

VirtualHome-LTL。ALFRED-LTL源自ALFRED数据

生成计划而不是验证它们[6],[8],[11]，或者提