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

要旨

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.

著者
Christine P.. Lee
University of Wisconsin-Madison, Madison, Wisconsin, United States
David Porfirio
U.S. Naval Research Laboratory, Washington, District of Columbia, United States
Xinyu Jessica. Wang
University of Wisconsin - Madison, Madison, Wisconsin, United States
Kevin Chenkai. Zhao
University of Wisconsin-Madison, Madison, Wisconsin, United States
Bilge Mutlu
University of Wisconsin-Madison, Madison, Wisconsin, United States
DOI

10.1145/3706598.3714113

論文URL

https://dl.acm.org/doi/10.1145/3706598.3714113

動画

会議: CHI 2025

The ACM CHI Conference on Human Factors in Computing Systems (https://chi2025.acm.org/)

セッション: DeIving into LLMs

G303
7 件の発表
2025-04-29 20:10:00
2025-04-29 21:40:00
日本語まとめ
読み込み中…