VeriPlan：将正式验证和大语言模型集成到终端用户规划中

研究背景与问题

• 作者发现了哪些问题或挑战？
  自动化规划工具传统上针对专业用户设计，其使用复杂的语言和逻辑方法，限制了普通用户的可用性。此外，即使是先进的大语言模型（LLMs），在复杂规划任务中仍存在可预测性不足、容易出现“幻觉”（生成虚假信息）以及缺乏用户信任的问题。

• 为什么这个问题很重要？
  普通用户在日常生活中有复杂的规划需求，如时间管理、项目协调等。然而，现有工具对普通用户不友好且缺乏可靠性，这限制了技术的潜在应用。此外，在关键领域如医疗或保障任务中，这些漏洞可能带来负面的安全影响。

• 研究动机与相关工作
  作者提出通过结合正式验证方法（如模型检查）和LLMs来增强这些系统的可靠性与可用性。使用模型检查技术为系统提供确定性边界，并在用户与系统的交互中加入更多控制机制，以解决规划中的不一致和约束未能完全遵守的问题。

解决方案

• 作者提出了哪些方法或解决方案？
  作者开发了名为“VeriPlan”的系统，通过结合大语言模型和正式验证方法（模型检查）来解决规划任务中的挑战。VeriPlan包括以下核心特性：规则翻译器（Rule Translator）、灵活性滑块（Flexibility Sliders）以及模型检查器（Model Checker）。

• 该解决方案的创新之处是什么？

  1. 正式验证：首次将模型检查技术应用于普通用户的规划任务，以验证LLMs的输出是否符合用户定义的约束。
  2. 用户参与：通过提供规则翻译器和灵活性滑块，用户能够动态调整规则的严格性和约束优先级，从而增强人机交互的有效性。
  3. 结合LLMs与正式验证：通过将用户输入转化为逻辑约束，并利用外部验证方法推动计划产出优化。

• 实施步骤是什么？使用了哪些关键技术？

  1. LLM规划：接受用户自然语言输入并生成初步规划结果。
  2. 规则翻译器：将用户的输入转化为正式的逻辑表达式（LTL逻辑），并提供用户确认译文的正确性。
  3. 灵活性滑块：允许用户通过调整滑块设置各规则的严格性（软约束/硬约束）。
  4. 模型检查器：利用PRISM工具，验证生成的规划是否符合用户规则，并提供反馈给用户与LLM。
  5. 迭代优化：LLM根据模型检查器反馈反复生成计划，直到满足定义的规则或达到迭代限制。

研究成果

• 取得了哪些具体成果？
  通过用户研究（n=12），验证了VeriPlan的有效性。整体结果显示，集成规则翻译器、灵活性滑块和模型检查器的VeriPlan系统显著提升了LLMs的使用性、输出性能与用户信任度。

• 与现有解决方案相比，它有哪些优势？

  1. 提高了规划任务的可靠性：模型检查器提供外部验证以减少规划输出中的错误。
  2. 增强用户控制：灵活性滑块和规则翻译器允许用户动态调整规则设置，满足个人偏好和实际情境需求。
  3. 提供创新性：将正式验证方法与大语言模型结合，增强了输出的透明性和用户满意度。用户能够主动定义和优化约束。

• 实验或评估结果是什么？
  在多个任务场景中（如病人导航、厨师优化和日程安排），完整的VeriPlan系统（含所有特性）显著超过未包含模型检查器（Condition 4）或单一特性缺失（Condition 2和3）的变体系统。在用户评分中，系统的使用性、满意度及规划性能均显著提升。

• 局限性与未来方向

  1. 约束模板的限制：目前的规则模板仅覆盖有限类型的时间约束，未来研究可扩展更多约束类型并允许用户定义自定义约束。
  2. 模型框架改进：PRISM工具限制了逻辑表达的类型，未来可探索新的验证方法以增强灵活性和表达力。
  3. 任务范围扩展：实验仅限于几个日常规划场景，未来可测试VeriPlan在其他领域（如医疗、制造业）中的表现。
  4. 可扩展性研究：受限于较小样本量，后续可开展更大规模的用户研究以进一步验证结果。

总结

VeriPlan为自动化规划开辟了新的路径，通过引入正式验证技术和用户控制，提升了LLMs的可靠性与使用性。本研究证明了结合模型检查和用户交互可有效解决规划任务中的种种挑战。未来研究可进一步扩展功能、增强灵活性，并深化领域应用，以满足复杂、动态环境中的用户需求。