Verifiable Robot Planning: Safeguarding Foundation Models via Formal Methods Feedback

Foundation Models (FMs), such as large language and vision models, are revolutionising robot planning by offering unprecedented flexibility for general-purpose reasoning. However, these models inherently lack formal guarantees, creating a significant risk of generating plans that are unsafe, non-compliant with operational and regulatory constraints. This "black box" nature is a critical barrier to deploying autonomous systems to interact with vulnerable individuals (e.g., the elderly, children) or in cluttered, unpredictable domestic settings.

This PhD project aims to solve this challenge by developing a novel framework that integrates formal methods as a continuous feedback loop for FM-driven planning. The central research question is: How can the outputs of formal verification be systematically translated into a corrective signal to guide, optimise, and safeguard an FM's planning process in real-time? The proposed methodology involves three core components. First, a high-level formal language (e.g., a variant of Linear Temporal Logic) will be used to specify both complex temporal-extended tasks and non-negotiable safety/regulatory rules. Second, a formal verifier (e.g., a model checker) will rigorously check the FM-generated plans against the formalised specifications before execution. Third, and most crucially, the verifier's output—such as a counterexample detailing a potential safety violation—will be programmatically converted into a structured feedback signal. This signal will be used to improve the FM's planning, for instance through automated prompt optimisation, guiding it to iteratively refine its plan. This creates a "verify-and-refine" architecture that moves beyond simple plan rejection, enabling the development of assistive robots that are not only intelligent but also provably safe and trustworthy.