Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866912726835527680 |
|---|---|
| author | Ramani, Keshav Tawosi, Vali Alamir, Salwa Borrajo, Daniel |
| author_facet | Ramani, Keshav Tawosi, Vali Alamir, Salwa Borrajo, Daniel |
| contents | We introduce a novel framework for evaluating the alignment between natural language plans and their expected behavior by converting them into Kripke structures and Linear Temporal Logic (LTL) using Large Language Models (LLMs) and performing model checking. We systematically evaluate this framework on a simplified version of the PlanBench plan verification dataset and report on metrics like Accuracy, Precision, Recall and F1 scores. Our experiments demonstrate that GPT-5 achieves excellent classification performance (F1 score of 96.3%) while almost always producing syntactically perfect formal representations that can act as guarantees. However, the synthesis of semantically perfect formal models remains an area for future exploration. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_03469 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification Ramani, Keshav Tawosi, Vali Alamir, Salwa Borrajo, Daniel Artificial Intelligence Logic in Computer Science We introduce a novel framework for evaluating the alignment between natural language plans and their expected behavior by converting them into Kripke structures and Linear Temporal Logic (LTL) using Large Language Models (LLMs) and performing model checking. We systematically evaluate this framework on a simplified version of the PlanBench plan verification dataset and report on metrics like Accuracy, Precision, Recall and F1 scores. Our experiments demonstrate that GPT-5 achieves excellent classification performance (F1 score of 96.3%) while almost always producing syntactically perfect formal representations that can act as guarantees. However, the synthesis of semantically perfect formal models remains an area for future exploration. |
| title | Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification |
| topic | Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2510.03469 |