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的机器人规划方法，在实际应用中面临安全性和合规性挑战。现有方法要么依赖大量人工标注数据进行微调，成本高昂；要么虽然引入了形式化验证反馈，但仍然需要耗费大量计算资源进行微调，难以快速适应新的约束条件。

核心思路：LAD-VF的核心在于利用形式化验证的结果，自动优化LLM的提示（Prompt），而非直接微调LLM的参数。通过这种方式，可以避免微调带来的计算开销和潜在的过拟合风险，同时保持LLM的通用性和灵活性。形式化验证提供了一种明确的反馈信号，指导提示的改进方向，从而提高规划结果的安全性与合规性。

技术框架：LAD-VF框架主要包含以下几个模块：1) LLM规划器：接收自然语言指令，生成初步的机器人行动计划；2) 形式化验证器：对行动计划进行验证，判断其是否满足预设的安全和合规约束；3) LLM自动微分模块（LLM-AutoDiff）：根据形式化验证的结果，计算提示的梯度；4) 提示优化器：根据梯度信息，迭代更新提示，直到满足约束条件或达到最大迭代次数。整个流程是一个闭环反馈系统，通过不断优化提示，提高LLM规划器的性能。

关键创新：LAD-VF最重要的创新在于将形式化验证反馈与LLM自动微分相结合，实现免微调的提示优化。与传统的微调方法相比，LAD-VF无需更新模型参数，降低了计算成本和数据需求。此外，通过优化提示而非模型本身，可以更容易地理解和解释LLM的行为，提高了系统的可信度。

关键设计：LAD-VF的关键设计包括：1) 形式化验证信息文本损失：该损失函数用于衡量当前提示生成的计划与约束条件之间的差距，指导提示的优化方向；2) LLM-AutoDiff：利用LLM的自动微分能力，计算损失函数关于提示的梯度；3) 提示的表示方式：提示的设计需要能够被LLM理解和执行，同时也要方便进行梯度计算和优化。具体的提示结构和优化算法的选择，需要根据具体的应用场景进行调整。

📊 实验亮点

实验结果表明，LAD-VF在机器人导航和操作任务中显著提高了规范依从性，将成功率从60%提高到90%以上。与需要微调的方法相比，LAD-VF在保证性能的同时，大大降低了计算成本和数据需求，展现了其在实际应用中的潜力。

🎯 应用场景

LAD-VF具有广泛的应用前景，可应用于机器人导航、自动驾驶、智能制造等领域。它能够帮助LLM驱动的控制系统更好地满足安全和合规约束，提高系统的可靠性和可信度。未来，该方法有望推广到其他需要形式化验证的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.