LAD-VF: LLM-Automatic Differentiation Enables Fine-Tuning-Free Robot Planning from Formal Methods Feedback
LAD-VF leverages formal verification feedback with AutoDiff for prompt optimization, achieving over 90% compliance without model fine-tuning.
Key Findings
Methodology
This paper introduces LAD-VF, a framework combining LLM AutoDiff with formal verification feedback to iteratively refine prompts. It converts generated plans into automata (e.g., NuSMV), verifies them against logical specifications using model checkers, and computes a violation ratio as a loss. This loss propagates as textual gradients through AutoDiff, updating prompts without altering model weights. The system employs multi-round prompt refinement, supporting modular architectures, and enhances interpretability by making prompt adjustments transparent. Experiments in robotic navigation and manipulation tasks demonstrate significant improvements in safety compliance, with success rates rising from 60% to over 90%. The approach is scalable, resource-efficient, and applicable to real-world robotic systems.
Key Results
- In robotic navigation and manipulation tasks, LAD-VF increased specification compliance from 60% to over 90%, outperforming traditional prompt optimization methods. The iterative prompt refinement effectively reduced safety violations, with the safety score improving from 0.6 to 0.92. Compared to fine-tuning approaches like RLVF, LAD-VF achieved similar performance with significantly less computational cost and data. Combining multiple prompt strategies (single, two-, multi-iteration) further enhanced robustness. Real robot deployments validated the method's practicality, maintaining high safety standards in dynamic environments. Ablation studies confirmed the critical role of formal verification feedback and AutoDiff in driving performance gains.
- The results highlight that prompt optimization via formal verification feedback can match or surpass fine-tuning in safety-critical applications. The resource efficiency and interpretability advantages make LAD-VF suitable for scalable deployment. Its ability to generalize across different tasks and specifications demonstrates broad applicability, paving the way for trustworthy autonomous systems. The experiments underscore the importance of multi-round prompt refinement and the integration of formal methods for robust safety guarantees in real-world scenarios.
- Ablation studies showed that removing formal verification feedback reduced compliance by 20%, emphasizing its importance. Multi-iteration prompts consistently outperformed single-step approaches, with safety scores increasing by 15-20%. The framework's modular design allowed adaptation to various task complexities, maintaining high performance. Overall, LAD-VF offers a practical, scalable solution for safe robot planning, with potential extensions into multi-modal feedback and dynamic specification generation, promising further improvements in autonomous system safety and reliability.
Significance
This work addresses a critical challenge in deploying large language models for safety-critical robotic tasks. By eliminating the need for costly fine-tuning, LAD-VF provides a scalable, interpretable, and mathematically grounded approach to ensure behavior compliance. Its integration of formal verification with prompt engineering bridges the gap between AI flexibility and safety guarantees, making autonomous systems more trustworthy. The framework's adaptability to modular architectures and real-world deployment demonstrates its potential to revolutionize autonomous control in industries like autonomous driving, industrial automation, and service robotics. It offers a new paradigm where safety is embedded directly into the prompt design, reducing reliance on extensive data labeling and model retraining, thus accelerating the adoption of AI in safety-sensitive domains.
Technical Contribution
LAD-VF introduces a novel integration of formal verification feedback into the prompt optimization process via LLM AutoDiff. Unlike traditional fine-tuning or preference-based methods, it employs a differentiable prompt refinement mechanism that propagates textual gradients through a complex multi-module system. The core innovation lies in converting generated plans into automata, verifying them with model checkers, and translating verification outcomes into loss signals that guide prompt updates. This approach supports multi-step, sequential decision-making, and modular architectures, enabling scalable, interpretable, and safe AI-driven control. The framework extends AutoDiff to handle cyclic graphs and non-LLM components, opening new avenues for safe AI deployment.
Novelty
This research is the first to embed formal verification feedback directly into the prompt optimization loop of large language models without model fine-tuning. It leverages AutoDiff to propagate verification outcomes as textual gradients, enabling iterative prompt refinement in complex, multi-module systems. Unlike prior work focused on preference learning or static prompt design, LAD-VF dynamically adjusts prompts based on formal safety guarantees, ensuring high compliance rates. Its modular, multi-step architecture and use of automata verification distinguish it from existing methods, providing a scalable, transparent, and theoretically grounded solution for safety-critical applications.
Limitations
- The effectiveness depends on the accuracy and completeness of formal specifications; poorly defined specs may limit safety guarantees.
- Computational overhead from automata conversion and model checking can impact real-time performance, especially in highly dynamic environments.
- While avoiding model fine-tuning, the iterative prompt optimization still requires multiple inference passes, which may be resource-intensive in large-scale systems.
Future Work
Future research will explore integrating multi-modal feedback, such as visual or sensor data, to enrich verification signals. Developing adaptive specification generation methods could enhance system robustness in unknown environments. Additionally, optimizing the AutoDiff process for faster convergence and extending the framework to multi-agent systems are promising directions. These advancements aim to further reduce computational costs, improve real-time performance, and broaden applicability across diverse autonomous platforms.
AI Executive Summary
Deep Dive
Plain Language Accessible to non-experts
想象你在厨房做菜，你有一本食谱，但食谱上的指示不够详细，可能会做出不健康或不合规的菜。于是，你用一台智能检测器检查菜的健康程度，发现哪里不符合标准后，你会调整食谱上的指示，再做一次。你不断重复这个过程，直到菜变得既好吃又健康。这就像LAD-VF用形式验证检查机器人计划，逐步优化提示，让机器人做事更安全、更符合规范。整个过程不用重新训练厨师（模型），只需不断改进菜单（提示），就能做出更好的菜。这种方法简单高效，也更容易理解和控制。
ELI14 Explained like you're 14
想象你在学校写作文，你的老师告诉你写得不够好，要你改一改。每次你写完，老师会检查，指出哪里错，然后你根据建议改。你反复这样做，作文会变得越来越棒。这就像LAD-VF的工作：它让机器人用类似的方法不断改正自己。它先让机器人写一个计划，然后用一个“老师”——一种特别的验证程序——检查这个计划是否符合安全规则。如果不符合，它会告诉机器人哪里错了，然后机器人根据这个反馈调整提示，再写一遍。这样反复多次，机器人就能写出既符合规则又能完成任务的计划。这不用重新训练机器人，只是不断调整它的“提示”，让它变得更聪明、更安全。就像你在学习中不断改正，最后变得更厉害一样。
Abstract
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.