Automated Generation of MDPs Using Logic Programming and LLMs for Robotic Applications

📄 arXiv: 2511.23143v1 📥 PDF

作者: Enrico Saccon, Davide De Martini, Matteo Saveriano, Edoardo Lamon, Luigi Palopoli, Marco Roveri

分类: cs.RO, cs.AI

发布日期: 2025-11-28

备注: 9 pages, 11 figures, 2 tables, 2 algorithms, accepted for publication in IEEE Robotics and Automation Letters

期刊: IEEE Robotics and Automation Letters, vol. 11, no. 2, pp. 1770-1777, Feb. 2026

DOI: 10.1109/LRA.2025.3643276

💡 一句话要点

提出一种结合LLM与形式化验证的MDP自动生成框架，用于机器人应用。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 马尔可夫决策过程 自动规划 形式化验证 机器人 人机交互 Prolog

📋 核心要点

  1. 现有机器人概率规划方法需要大量人工干预，限制了其可扩展性和易用性。
  2. 利用LLM从自然语言描述中提取知识，自动构建MDP，并结合形式化验证方法合成最优策略。
  3. 在人机交互场景中验证了框架的有效性，证明了其能够以最少的人工干预生成可执行策略。

📝 摘要（中文）

本文提出了一种新颖的框架，该框架将大型语言模型（LLM）与自动规划和形式化验证相结合，以简化马尔可夫决策过程（MDP）的创建和使用。我们的系统利用LLM从自然语言（NL）描述中提取结构化知识，并将其表示为Prolog知识库。然后，通过可达性分析自动构建MDP，并使用Storm模型检测器合成最优策略。生成的策略被导出为状态-动作表以供执行。我们在三个人机交互场景中验证了该框架，证明了其能够以最少的人工干预生成可执行策略。这项工作突出了将语言模型与形式化方法相结合的潜力，从而在机器人技术中实现更易于访问和可扩展的概率规划。

🔬 方法详解

问题定义：论文旨在解决机器人应用中马尔可夫决策过程（MDP）的手动构建问题。现有方法需要人工定义状态空间、动作空间、转移概率和奖励函数，过程繁琐且容易出错，限制了MDP在复杂机器人任务中的应用。因此，如何自动化生成MDP，降低人工成本，提高效率是本文要解决的核心问题。

核心思路：论文的核心思路是利用大型语言模型（LLM）理解自然语言描述的机器人任务，并从中提取结构化知识，然后将这些知识转化为MDP的各个组成部分。通过结合形式化验证方法，可以保证生成的MDP的正确性和最优性。这种方法将自然语言理解、知识表示和形式化验证相结合，实现了MDP的自动化生成。

技术框架：该框架包含以下几个主要模块：1) 自然语言理解模块：使用LLM解析自然语言描述的机器人任务，提取关键信息，例如状态、动作、目标等。2) 知识表示模块：将提取的信息表示为Prolog知识库，方便后续推理和计算。3) MDP构建模块：基于Prolog知识库，通过可达性分析自动构建MDP的状态空间、动作空间、转移概率和奖励函数。4) 策略合成模块：使用Storm模型检测器对MDP进行分析，合成最优策略。5) 策略执行模块：将合成的策略导出为状态-动作表，供机器人执行。

关键创新：该论文的关键创新在于将LLM与形式化验证相结合，实现了MDP的自动化生成。与传统方法相比，该方法无需人工定义MDP的各个组成部分，大大降低了人工成本，提高了效率。此外，通过形式化验证，可以保证生成的MDP的正确性和最优性。

关键设计：论文中LLM的选择和Prolog知识库的构建是关键设计。LLM需要具备强大的自然语言理解能力，能够准确提取任务描述中的关键信息。Prolog知识库需要能够清晰地表示状态、动作、转移概率和奖励函数等信息，方便后续推理和计算。此外，Storm模型检测器的参数设置也会影响策略合成的效率和质量。具体参数设置在论文中未详细说明，属于未知信息。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

论文在三个人机交互场景中验证了该框架的有效性。实验结果表明，该框架能够以最少的人工干预生成可执行策略，证明了其在实际应用中的潜力。具体的性能数据和对比基线在论文中未详细说明，属于未知信息。

🎯 应用场景

该研究成果可应用于各种机器人应用场景，例如人机交互、自主导航、任务规划等。通过自动化生成MDP，可以降低机器人应用开发的门槛，提高开发效率。未来，该方法可以扩展到更复杂的机器人任务中，例如多机器人协作、动态环境下的任务规划等，具有广阔的应用前景。

📄 摘要（原文）

We present a novel framework that integrates Large Language Models (LLMs) with automated planning and formal verification to streamline the creation and use of Markov Decision Processes (MDP). Our system leverages LLMs to extract structured knowledge in the form of a Prolog knowledge base from natural language (NL) descriptions. It then automatically constructs an MDP through reachability analysis, and synthesises optimal policies using the Storm model checker. The resulting policy is exported as a state-action table for execution. We validate the framework in three human-robot interaction scenarios, demonstrating its ability to produce executable policies with minimal manual effort. This work highlights the potential of combining language models with formal methods to enable more accessible and scalable probabilistic planning in robotics.