INPROVF: Leveraging Large Language Models to Repair High-level Robot Controllers from Assumption Violations

TL;DR

This paper tackles the challenge of repairing high-level robot controllers at runtime when environment assumptions are violated and state spaces are too large for purely formal methods. It introduces INPROVF, a hybrid framework that leverages large language models to generate repair candidates and uses formal verification to ensure correctness, with an explicit Informalization step that translates abstractions into natural language to improve prompting. The approach includes iterative Repair and Feedback stages, where formal analyses provide targeted guidance to the LLM, and verification checks ensure the updated specification is realizable. Empirical results across 12 violations in diverse workspaces show that INPROVF significantly improves scalability over a purely formal-baseline, with ablation studies confirming the value of informalization and feedback in achieving higher success rates.

Abstract

This paper presents INPROVF, an automatic framework that combines large language models (LLMs) and formal methods to speed up the repair process of high-level robot controllers. Previous approaches based solely on formal methods are computationally expensive and cannot scale to large state spaces. In contrast, INPROVF uses LLMs to generate repair candidates, and formal methods to verify their correctness. To improve the quality of these candidates, our framework first translates the symbolic representations of the environment and controllers into natural language descriptions. If a candidate fails the verification, INPROVF provides feedback on potential unsafe behaviors or unsatisfied tasks, and iteratively prompts LLMs to generate improved solutions. We demonstrate the effectiveness of INPROVF through 12 violations with various workspaces, tasks, and state space sizes.

Figures (7)

• Figure 1: INPROVF overview. Given a discrete abstraction, a specification, and an assumption violation we use LLMs and formal methods to repair the behaviors of high-level robot controllers under assumption violations.
• Figure 2: Example \ref{['example:1']} from Sec. VC of meng2024automated. Under an unexpected cup status change, the robot creates a new skill (blue arrow) to handle the violation.
• Figure 3: INPROVF system details. Our system consists of four steps: Informalization translates formal abstraction and strategy into natural language descriptions; Repair leverages to generate new skill candidates; Verification ensures the correctness of the candidates through syntax and realizability checking; Feedback leverages formal analyses to provide concise feedback to assist for iterative prompting.
• Figure 4: Case study for Example \ref{['example:1']}. (A)-(D) describe the prompts and LLM responses from informalization. (E)-(G) present the repair prompt and two sets of new skill candidates from , along with the feedback from formal analyses. We use p_object_region to represent the input $\pi_{{\textrm{object}}}^{{\textrm{region}}}$ and prime (') for the next operator ($\bigcirc$), following the syntax of formulas in Slugs ehlers2016slugs.
• Figure 5: Example workspace. Left: An apartment-like workspace where a mobile manipulator performs laundry tasks. Right: An emergency room-like workspace where a robot swarm performs patrolling tasks.