Large Language Models (LLMs) such as GPT-4 or LLaMA have recently been applied to robotics, where they can generate task plans directly from natural-language instructions (e.g., “Set the table for dinner”). However, natural-language plans are often ambiguous and unreliable, making it difficult to guarantee safe and correct robot behavior.

This thesis explores an alternative: guiding LLMs to generate plans in the Planning Domain Definition Language (PDDL), a formal representation widely used in AI planning. By converting high-level instructions into PDDL, robot plans can be formally checked for validity, goal satisfaction, and resource constraints before execution. This combination of LLM-based plan generation with formal reliability checks has the potential to significantly improve the safety and robustness of LLM-controlled robots.

While LLMs are powerful at producing structured outputs, generating syntactically and semantically valid PDDL remains a challenge. Moreover, not all valid plans are feasible or safe when applied to robotic tasks. This thesis investigates the following challenges:

• How can LLMs be prompted or fine-tuned to reliably generate syntactically correct PDDL plans?
• How can existing planning tools and validators (e.g., Fast Downward, VAL) be used to automatically check correctness and feasibility of these plans?
• Does integrating formal verification improve the reliability and safety of robot task execution compared to direct natural-language planning?
• (Optional) Can failed verifications be used as structured feedback loops to refine LLM-generated plans?

• Programming skills in Python.
• Familiarity with machine learning and/or AI planning.
• Interest in robotics, formal methods, or LLMs.
• (Preferred) Prior knowledge of PDDL or willingness to learn.
• (Optional) Experience with robotic simulators (e.g., PyBullet, Gazebo, Webots) is a plus.