用形式化验证提升大模型在普通人规划中的可靠性与可控性
VeriPlan: Integrating Formal Verification and LLMs into End-User Planning
- 结合模型检测技术验证大模型生成的计划正确性
- 用户研究显示感知质量、易用性和满意度显著提升
- 适合希望掌控大模型规划结果的普通用户
自动化规划传统上由专家使用专业工具完成，应用于制造、医疗等领域。近年来大语言模型（LLMs）的发展使普通人也能参与复杂规划任务。然而，大模型在终端用户规划中面临一致性、准确性及用户信任等问题。本文提出VeriPlan系统，将形式化验证技术（特别是模型检查）引入大模型规划，增强其可靠性与灵活性。该系统包含规则转换器、灵活性滑块和模型检查器三个核心组件，使用户能参与验证过程。通过12名用户的实验评估，结果表明系统显著提升了用户对大模型生成计划的质量感知、可用性及满意度。本工作展示了形式化验证与用户控制功能与大模型在终端用户规划任务中的有效融合。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。