Researchers use dual-LLM system with formal logic for verified farm robot missions

As robotic systems become more common in agriculture, operators often lack the programming skills needed to configure them precisely. To bridge this gap, researchers introduced a mission planner that uses large language models (LLMs) to convert natural language instructions into executable robot plans. However, natural language is inherently ambiguous, leading to potential mission failures.

In a new paper presented at ICRA 2026, Marcos Abel Zuzuárregui and Stefano Carpin extend this system by adding multiple feedback loops that leverage linear temporal logic (LTL). LTL formally verifies that the generated plan matches the user's intended specifications. To further reduce bias, they split the task between two distinct commercial LLMs: one handles specification generation, the other performs verification. Their experiments show this approach effectively catches errors, though LLMs occasionally produce incorrect LTL formulas. The work highlights a practical path toward making agricultural robots accessible to non-experts while maintaining reliability.