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

arXiv: https://arxiv.org/abs/2509.18384 · HTML: https://mlsanity.com/paper/2509.18384/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Sep 2025.

## Built on by (most cited first, 4 of 4)

- [VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents](https://mlsanity.com/paper/2606.05395/) (2026)
- [Safe Embodied AI for Long-horizon Tasks: A Cross-layer Analysis of Robotic Manipulation](https://mlsanity.com/paper/2606.05660/) (2026)
- [HPFA: Hypergraph-Based Paired Failure Attribution for LLM Reasoning](https://mlsanity.com/paper/2608.02026/) (2026)
- [Security and Privacy in Large-Model-Driven Embodied Agents: Attacks, Defenses, and Future Directions](https://mlsanity.com/paper/2609.27847/) (2026)

## Abstract (arXiv)

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.