AD-VF: LLM-Automatic Differentiation Enables Fine-Tuning-Free Robot Planning from Formal Methods Feedback

📄 arXiv: 2509.18384v1 📥 PDF

作者: Yunhao Yang, Junyuan Hong, Gabriel Jacob Perin, Zhiwen Fan, Li Yin, Zhangyang Wang, Ufuk Topcu

分类: cs.RO, cs.FL

发布日期: 2025-09-22

💡 一句话要点

AD-VF：基于LLM自动微分与形式化反馈的免微调机器人规划

🎯 匹配领域: 支柱一：机器人控制 (Robot Control) 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 机器人规划 形式化验证 自动微分 免微调 提示工程 规范依从性

📋 核心要点

  1. 现有LLM在机器人规划中难以满足安全和监管约束，且依赖人工标注或资源密集型微调。
  2. LAD-VF利用形式化验证反馈，通过LLM自动微分迭代优化提示，无需微调模型参数。
  3. 实验表明，LAD-VF显著提升了机器人导航和操作任务的规范依从性，成功率从60%提升至90%以上。

📝 摘要（中文）

大型语言模型（LLM）可以将自然语言指令转化为机器人、自动驾驶等领域的可执行行动计划。然而，在物理世界中部署LLM驱动的规划需要严格遵守安全和监管约束，但当前模型由于幻觉或弱对齐，经常违反这些约束。传统的数据驱动对齐方法（如直接偏好优化DPO）需要昂贵的人工标注，而最近的形式化反馈方法仍然依赖于资源密集型的微调。本文提出LAD-VF，一个免微调框架，利用形式化验证反馈进行自动提示工程。通过引入一个形式化验证信息文本损失，并将其与LLM-AutoDiff集成，LAD-VF迭代地优化提示而不是模型参数。这带来了三个关键优势：（i）无需微调的可扩展适应性；（ii）与模块化LLM架构的兼容性；（iii）通过可审计提示实现可解释的优化。在机器人导航和操作任务中的实验表明，LAD-VF显著提高了规范依从性，将成功率从60%提高到90%以上。因此，我们的方法为实现可信赖、经过形式化验证的LLM驱动控制系统提供了一条可扩展且可解释的途径。

🔬 方法详解

问题定义：论文旨在解决LLM在机器人规划中，难以满足安全和监管约束的问题。现有方法，如DPO，需要大量人工标注，成本高昂；而基于形式化反馈的方法通常需要对LLM进行微调，计算资源消耗大，且可能影响模型的通用性。

核心思路：论文的核心思路是利用形式化验证提供的反馈信号，通过自动提示工程来引导LLM生成符合规范的行动计划，而无需对LLM本身进行微调。这种方法旨在降低成本、提高效率，并保持LLM的通用性。

技术框架：LAD-VF框架主要包含以下几个模块：1) LLM：负责生成初始的行动计划；2) 形式化验证器：对行动计划进行验证，判断其是否满足给定的安全和监管规范，并提供反馈信号；3) LLM-AutoDiff：利用LLM的自动微分能力，计算提示词的梯度，并根据形式化验证的反馈信号，迭代优化提示词；4) 提示词更新模块：根据计算得到的梯度，更新提示词，引导LLM生成更符合规范的行动计划。整个流程是一个迭代的过程，直到生成的行动计划满足规范要求或达到最大迭代次数。

关键创新：该论文的关键创新在于将形式化验证的反馈与LLM的自动微分能力相结合，实现了一种免微调的提示工程方法。与传统的微调方法相比，该方法不需要对LLM的参数进行更新，从而降低了计算成本，并保持了LLM的通用性。此外，通过优化提示词，可以更容易地理解和解释LLM的行为，提高了系统的可解释性。

关键设计：LAD-VF的关键设计包括：1) 形式化验证信息文本损失：该损失函数用于衡量生成的行动计划与规范之间的差距，并指导提示词的优化方向；2) LLM-AutoDiff：利用LLM的自动微分能力，计算提示词的梯度，并根据损失函数的值，更新提示词；3) 提示词的表示方式：提示词被表示为可优化的向量，以便利用梯度下降等优化算法进行更新。

🖼️ 关键图片

img_0

📊 实验亮点

实验结果表明，LAD-VF在机器人导航和操作任务中显著提高了规范依从性，将成功率从60%提高到90%以上。与需要微调的方法相比，LAD-VF在保证性能的同时，降低了计算成本，并提高了系统的可解释性。这些结果表明，LAD-VF是一种有效的、可扩展的、可解释的LLM驱动控制系统。

🎯 应用场景

该研究成果可广泛应用于机器人、自动驾驶等领域，尤其是在对安全性和可靠性要求较高的场景中。例如，在医疗机器人手术规划、自动驾驶车辆的路径规划等应用中，可以利用该方法确保生成的行动计划符合安全规范，从而降低事故发生的风险。此外，该方法的可解释性也使其在需要人工干预的场景中具有优势。

📄 摘要（原文）

Large language models (LLMs) can translate natural language instructions into executable action plans for robotics, autonomous driving, and other domains. Yet, deploying LLM-driven planning in the physical world demands strict adherence to safety and regulatory constraints, which current models often violate due to hallucination or weak alignment. Traditional data-driven alignment methods, such as Direct Preference Optimization (DPO), require costly human labeling, while recent formal-feedback approaches still depend on resource-intensive fine-tuning. In this paper, we propose LAD-VF, a fine-tuning-free framework that leverages formal verification feedback for automated prompt engineering. By introducing a formal-verification-informed text loss integrated with LLM-AutoDiff, LAD-VF iteratively refines prompts rather than model parameters. This yields three key benefits: (i) scalable adaptation without fine-tuning; (ii) compatibility with modular LLM architectures; and (iii) interpretable refinement via auditable prompts. Experiments in robot navigation and manipulation tasks demonstrate that LAD-VF substantially enhances specification compliance, improving success rates from 60% to over 90%. Our method thus presents a scalable and interpretable pathway toward trustworthy, formally-verified LLM-driven control systems.