INPROVF: Leveraging Large Language Models to Repair High-level Robot Controllers from Assumption Violations
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866909541324554240 |
|---|---|
| author | Meng, Qian Zhou, Jin Peng Weinberger, Kilian Q. Kress-Gazit, Hadas |
| author_facet | Meng, Qian Zhou, Jin Peng Weinberger, Kilian Q. Kress-Gazit, Hadas |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_13660 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | INPROVF: Leveraging Large Language Models to Repair High-level Robot Controllers from Assumption Violations Meng, Qian Zhou, Jin Peng Weinberger, Kilian Q. Kress-Gazit, Hadas Robotics Artificial Intelligence Formal Languages and Automata Theory Systems and Control 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. |
| title | INPROVF: Leveraging Large Language Models to Repair High-level Robot Controllers from Assumption Violations |
| topic | Robotics Artificial Intelligence Formal Languages and Automata Theory Systems and Control |
| url | https://arxiv.org/abs/2503.13660 |