mlsanityData to 14 Oct 2026

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

arXiv 2502.17898 ↗First posted 25 Feb 2025cs.HC cs.AIcited by 20

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. Cited by 20 papers in the map (data through 14 Oct 2026). Builds on 63 of its 125 references that are in the map. First posted on arXiv 25 Feb 2025.

Builds on

63 of 125 references.

References · 63

  1. 2023GPT-4 Technical Reportcited by 18,396
  2. 2020Retrieval-Augmented Generation for Knowledge-Intensive NLP Taskscited by 9,297
  3. 2022ReAct: Synergizing Reasoning and Acting in Language Modelscited by 8,695
  4. 2023Judging LLM-as-a-Judge with MT-Bench and Chatbot Arenacited by 8,626
  5. 2022Survey of Hallucination in Natural Language Generationcited by 2,075
  6. 2023Language Models Don't Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Promptingcited by 1,122
  7. 2023Large Language Models are not Fair Evaluatorscited by 1,085
  8. 2023Teaching Large Language Models to Self-Debugcited by 988
  9. 2020On Faithfulness and Factuality in Abstractive Summarizationcited by 900
  10. 2023CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquingcited by 783
  11. 2023ChatEval: Towards Better LLM-based Evaluators through Multi-Agent Debatecited by 742
  12. 2024MathVerse: Does Your Multi-modal LLM Truly See the Diagrams in Visual Math Problems?cited by 586
38 more
  1. 2022LLM-Planner: Few-Shot Grounded Planning for Embodied Agents with Large Language Modelscited by 462
  2. 2024Understanding the planning of LLM agents: A surveycited by 421
  3. 2023Harnessing the Power of LLMs in Practice: A Survey on ChatGPT and Beyondcited by 411
  4. 2023Describe, Explain, Plan and Select: Interactive Planning with Large Language Models Enables Open-World Multi-Task Agentscited by 398
  5. 2024TravelPlanner: A Benchmark for Real-World Planning with Language Agentscited by 392
  6. 2023A Survey of Hallucination in Large Foundation Modelscited by 368
  7. 2023Explainability for Large Language Models: A Surveycited by 333
  8. 2023On the Planning Abilities of Large Language Models : A Critical Investigationcited by 312
  9. 2023LEVER: Learning to Verify Language-to-Code Generation with Executioncited by 239
  10. 2022Making Large Language Models Better Reasoners with Step-Aware Verifiercited by 233
  11. 2023Large Language Models as General Pattern Machinescited by 197
  12. 2024LLMs Can't Plan, But Can Help Planning in LLM-Modulo Frameworkscited by 179
  13. 2023LLM Lies: Hallucinations are not Bugs, but Features as Adversarial Examplescited by 177
  14. 2023Benchmarking Cognitive Biases in Large Language Models as Evaluatorscited by 150
  15. 2024Who Validates the Validators? Aligning LLM-Assisted Evaluation of LLM Outputs with Human Preferencescited by 144
  16. 2023Generalized Planning in PDDL Domains with Pretrained Large Language Modelscited by 139
  17. 2020Uncertainty as a Form of Transparency: Measuring, Communicating, and Using Uncertaintycited by 129
  18. 2021Reframing Human-AI Collaboration for Generating Free-Text Explanationscited by 125
  19. 2022Explanations from Large Language Models Make Small Reasoners Bettercited by 124
  20. 2024Beyond Functional Correctness: Exploring Hallucinations in LLM-Generated Codecited by 107
  21. 2023Wider and Deeper LLM Networks are Fairer LLM Evaluatorscited by 94
  22. 2024OffsetBias: Leveraging Debiased Data for Tuning Evaluatorscited by 94
  23. 2023Can Large Language Models Explain Themselves? A Study of LLM-Generated Self-Explanationscited by 90
  24. 2023The Metacognitive Demands and Opportunities of Generative AIcited by 87
  25. 2021Few-Shot Self-Rationalization with Natural Language Promptscited by 83
  26. 2024User-LLM: Efficient LLM Contextualization with User Embeddingscited by 76
  27. 2023Bridging the Gulf of Envisioning: Cognitive Design Challenges in LLM Interfacescited by 72
  28. 2023Plug in the Safety Chip: Enforcing Constraints for LLM-driven Robot Agentscited by 69
  29. 2023MathChat: Converse to Tackle Challenging Math Problems with LLM Agentscited by 68
  30. 2024CFBench: A Comprehensive Constraints-Following Benchmark for LLMscited by 67
  31. 2023Graphologue: Exploring Large Language Model Responses with Interactive Diagramscited by 66
  32. 2023The Past, Present and Better Future of Feedback Learning in Large Language Models for Subjective Human Preferences and Valuescited by 54
  33. 2023Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environmentscited by 53
  34. 2023Post Hoc Explanations of Language Models Can Improve Language Modelscited by 50
  35. 2023Sensecape: Enabling Multilevel Exploration and Sensemaking with Large Language Modelscited by 48
  36. 2022Investigating Explainability of Generative AI for Code through Scenario-based Designcited by 47
  37. 2024"We Need Structured Output": Towards User-centered Constraints on Large Language Model Outputcited by 46
  38. 2024On the Prospects of Incorporating Large Language Models (LLMs) in Automated Planning and Scheduling (APS)cited by 40

50 most cited of 63 All 63 (JSON)

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 10; 2026: 10.

20 papers.

Sort:

By area:

  1. 2025ACE: A Security Architecture for LLM-Integrated App Systemscited by 55
  2. 2025LLM-Based Human-Agent Collaboration and Interaction Systems: A Surveycited by 29
  3. 2025AgentGuard: Runtime Verification of AI Agentscited by 17
  4. 2026ToolGate: Contract-Grounded and Verified Tool Execution for LLMscited by 15
  5. 2025VeruSAGE: A Study of Agent-Based Verification for Rust Systemscited by 12
  6. 2025Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verificationcited by 7
  7. 2025RepV: Safety-Separable Latent Spaces for Scalable Neurosymbolic Plan Verificationcited by 2
  8. 2026Toward Safe LLM Agents: A Survey of Specification, Verification, and Enforcementcited by 2
  9. 2025Verifying Memoryless Sequential Decision-making of Large Language Modelscited by 1
  10. 2026GNNVerifier: Graph-based Verifier for LLM Task Planningcited by 1
  11. 2026LitPivot: Developing Well-Situated Research Ideas Through Dynamic Contextualization and Critique within the Literature Landscapecited by 1
  12. 2026Meta-Agent: From Task Descriptions to Verified Multi-Agent Systemscited by 1
8 more
  1. 2025Persuasive or Neutral? A Field Experiment on Generative AI in Online Travel Planningcited by 0
  2. 2025HyPlan: Hybrid Learning-Assisted Planning Under Uncertainty for Safe Autonomous Drivingcited by 0
  3. 2025Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verificationcited by 0
  4. 2026Do You Understand How I Feel?: Towards Verified Empathy in Therapy Chatbotscited by 0
  5. 2026Explorable Proofs: Making Written Proofs Explorable by Grounding Them in Formal Representationscited by 0
  6. 2026U-Define: Designing User Workflows for Hard and Soft Constraints in LLM-Based Planningcited by 0
  7. 2026From Tool to Agent: How Worker Needs Reorganize Across the Agentic Roles of Workplace AIcited by 0
  8. 2026Agentic Cognitive Depth: Operational Criteria for Evaluating LLM Agentscited by 0