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

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 39 references that are in the map.
- First posted on arXiv 17 Mar 2025.

## Builds on (most cited first, 13 of 13)

- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [A Survey of Autonomous Driving: Common Practices and Emerging Technologies](https://mlsanity.com/paper/1906.05113/) (2019)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [IRIS: LLM-Assisted Static Analysis for Detecting Security Vulnerabilities](https://mlsanity.com/paper/2405.17238/) (2024)
- [NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Models](https://mlsanity.com/paper/2305.07766/) (2023)
- [Specification Patterns for Robotic Missions](https://mlsanity.com/paper/1901.02077/) (2019)
- [Python Symbolic Execution with LLM-powered Code Generation](https://mlsanity.com/paper/2409.09271/) (2024)
- [Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation](https://mlsanity.com/paper/2311.10483/) (2023)
- [Physically-Feasible Repair of Reactive, Linear Temporal Logic-based, High-Level Tasks](https://mlsanity.com/paper/2207.02834/) (2022)
- [RABBIT: A Robot-Assisted Bed Bathing System with Multimodal Perception and Integrated Compliance](https://mlsanity.com/paper/2401.15159/) (2024)
- [Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications](https://mlsanity.com/paper/1308.4113/) (2013)
- [Automated Robot Recovery from Assumption Violations of High-Level Specifications](https://mlsanity.com/paper/2407.00562/) (2024)

## Abstract (arXiv)

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.