VeriPlan: Integrating Formal Verification and LLMs into End-User Planning

TL;DR

VeriPlan enhances end-user planning with LLMs by integrating formal verification, rule translation, and user controls, improving reliability, usability, and user trust through a novel system evaluated in user studies.

Contribution

The paper introduces VeriPlan, a system combining formal verification with LLMs for end-user planning, including new features like rule translation and user-controlled verification.

Findings

Improved perceived quality and usability of LLM-based planning.

Enhanced user trust through formal verification features.

Positive user satisfaction outcomes in a user study.

Abstract

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.