VeriPlan: Integrating Formal Verification and LLMs into End-User Planning
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909509555847168 |
|---|---|
| author | Lee, Christine Porfirio, David Wang, Xinyu Jessica Zhao, Kevin Mutlu, Bilge |
| author_facet | Lee, Christine Porfirio, David Wang, Xinyu Jessica Zhao, Kevin Mutlu, Bilge |
| contents | Automated planning is traditionally the domain of experts, utilized in fields like manufacturing and healthcare with the aid of expert planning tools. Recent advancements in LLMs have made planning more accessible to everyday users due to their potential to assist users with complex planning tasks. However, LLMs face several application challenges within end-user planning, including consistency, accuracy, and user trust issues. This paper introduces VeriPlan, a system that applies formal verification techniques, specifically model checking, to enhance the reliability and flexibility of LLMs for end-user planning. In addition to the LLM planner, VeriPlan includes three additional core features -- a rule translator, flexibility sliders, and a model checker -- that engage users in the verification process. Through a user study (n=12), we evaluate VeriPlan, demonstrating improvements in the perceived quality, usability, and user satisfaction of LLMs. Our work shows the effective integration of formal verification and user-control features with LLMs for end-user planning tasks. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_17898 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | VeriPlan: Integrating Formal Verification and LLMs into End-User Planning Lee, Christine Porfirio, David Wang, Xinyu Jessica Zhao, Kevin Mutlu, Bilge Human-Computer Interaction Artificial Intelligence I.2.1; I.2.5; I.2.2; I.2.7 Automated planning is traditionally the domain of experts, utilized in fields like manufacturing and healthcare with the aid of expert planning tools. Recent advancements in LLMs have made planning more accessible to everyday users due to their potential to assist users with complex planning tasks. However, LLMs face several application challenges within end-user planning, including consistency, accuracy, and user trust issues. This paper introduces VeriPlan, a system that applies formal verification techniques, specifically model checking, to enhance the reliability and flexibility of LLMs for end-user planning. In addition to the LLM planner, VeriPlan includes three additional core features -- a rule translator, flexibility sliders, and a model checker -- that engage users in the verification process. Through a user study (n=12), we evaluate VeriPlan, demonstrating improvements in the perceived quality, usability, and user satisfaction of LLMs. Our work shows the effective integration of formal verification and user-control features with LLMs for end-user planning tasks. |
| title | VeriPlan: Integrating Formal Verification and LLMs into End-User Planning |
| topic | Human-Computer Interaction Artificial Intelligence I.2.1; I.2.5; I.2.2; I.2.7 |
| url | https://arxiv.org/abs/2502.17898 |