Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification

• URL: http://arxiv.org/abs/2510.03469v1
• Date: Fri, 03 Oct 2025 19:46:55 GMT
• Title: Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification
• Abstract summary: We introduce a novel framework for evaluating the alignment between natural language plans and their expected behavior by converting them into Kripke structures and Linear Temporal Logic (LTL)<n>We systematically evaluate this framework on a simplified version of the PlanBench plan verification dataset and report on metrics like Accuracy, Precision, Recall and F1 scores.
• Score: 5.177308274872149
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce a novel framework for evaluating the alignment between natural language plans and their expected behavior by converting them into Kripke structures and Linear Temporal Logic (LTL) using Large Language Models (LLMs) and performing model checking. We systematically evaluate this framework on a simplified version of the PlanBench plan verification dataset and report on metrics like Accuracy, Precision, Recall and F1 scores. Our experiments demonstrate that GPT-5 achieves excellent classification performance (F1 score of 96.3%) while almost always producing syntactically perfect formal representations that can act as guarantees. However, the synthesis of semantically perfect formal models remains an area for future exploration.

Related papers

• Automatic Translation of Unstructured Requirements into Linear Temporal Logic through Large Language Models [46.28810845443601]
  This paper evaluates whether contemporary off-the-shelf Large Language Models (LLMs) can help bridge this gap by generating Linear Temporal Logic (LTL) formulas directly from unstructured requirements.<n>The study examines six modern LLMs using a few-shot prompting strategy on a heterogeneous benchmark of 15 structurally varied requirements.<n>The results indicate that current general-purpose LLMs can achieve practically significant performance on the unstructured NLto-LTL task without task-specific fine-tuning.
  arXiv  Detail & Related papers  (2026-08-06T17:13:07Z)
• Early-Stage Product Line Validation Using LLMs: A Study on Semi-Formal Blueprint Analysis [41.966962052550656]
  We study whether Large Language Models (LLMs) can perform feature model analysis operations (AOs) directly on semi-formal textual blueprints.<n>Using 12 state-of-the-art LLMs and 16 standard AOs, we compare their outputs against the solver-based oracle FLAMA.<n>Results show that reasoning-optimized models (e.g., Grok 4 Fast Reasoning, Gemini 2.5 Pro) achieve 88-89% average accuracy across all evaluated blueprints and operations.
  arXiv  Detail & Related papers  (2026-04-22T13:01:38Z)
• From Scoring to Explanations: Evaluating SHAP and LLM Rationales for Rubric-based Teaching Quality Assessment [12.134587575174633]
  We propose a general framework for sentence-level interpretability of rubric-based scoring.<n>We show that SHAP provides more faithful and transferable explanations for rubric-based scoring.
  arXiv  Detail & Related papers  (2026-04-18T14:27:51Z)
• Claim Automation using Large Language Model [0.0]
  Large Language Models (LLMs) have achieved strong performance on general-purpose language tasks, but their deployment in regulated and data-sensitive domains, including insurance, remains limited.<n>We propose a locally deployed governance-aware language modeling component that generates structured corrective-action recommendations from unstructured claim narratives.<n>We fine-tune pretrained LLMs using Low-Rank Adaptation (LoRA), scoping the model to an initial decision module within the claim processing pipeline to speed up claim adjusters' decisions.
  arXiv  Detail & Related papers  (2026-02-18T20:01:12Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements.<n>Existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency.<n>We propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process.
  arXiv  Detail & Related papers  (2025-10-08T10:25:12Z)
• Estimating Time Series Foundation Model Transferability via In-Context Learning [74.65355820906355]
  Time series foundation models (TSFMs) offer strong zero-shot forecasting via large-scale pre-training.<n>Fine-tuning remains critical for boosting performance in domains with limited public data.<n>We introduce TimeTic, a transferability estimation framework that recasts model selection as an in-context-learning problem.
  arXiv  Detail & Related papers  (2025-09-28T07:07:13Z)
• Can LLM-Reasoning Models Replace Classical Planning? A Benchmark Study [0.0]
  Large Language Models have sparked interest in their potential for robotic task planning.<n>While these models demonstrate strong generative capabilities, their effectiveness in producing structured and executable plans remains uncertain.<n>This paper presents a systematic evaluation of a broad spectrum of current state of the art language models.
  arXiv  Detail & Related papers  (2025-07-31T14:25:54Z)
• Towards Locally Deployable Fine-Tuned Causal Large Language Models for Mode Choice Behaviour [4.378407481656902]
  This study investigates the adoption of open-access, locally deployable causal large language models (LLMs) for travel mode choice prediction.<n>We benchmark eleven LLMs across three stated and revealed preference datasets, testing 396 configurations and generating over 79,000 synthetic commuter predictions.<n>LiTransMC, fine-tuned using parameter efficient and loss masking strategy, achieved a weighted F1 score of 0.6845 and a Jensen-Shannon Divergence of 0.000245.
  arXiv  Detail & Related papers  (2025-07-29T02:03:37Z)
• Large Language Models for Planning: A Comprehensive and Systematic Survey [29.168219253281453]
  Large Language Models (LLMs) have demonstrated remarkable performance on certain planning tasks.<n>This paper presents a comprehensive review of LLM-based planning.
  arXiv  Detail & Related papers  (2025-05-26T08:44:53Z)
• Reliable Decision Support with LLMs: A Framework for Evaluating Consistency in Binary Text Classification Applications [0.7124971549479361]
  This study introduces a framework for evaluating consistency in large language model (LLM) binary text classification.<n>We determine sample size requirements, develop metrics for invalid responses, and evaluate intra- and inter-rater reliability.
  arXiv  Detail & Related papers  (2025-05-20T21:12:58Z)
• SCORE: Systematic COnsistency and Robustness Evaluation for Large Language Models [4.875712300661656]
  We present SCORE ($mathbfS$ystematic $mathbfCO$nsistency and $mathbfR$obustness $mathbfE$valuation), a comprehensive framework for non-adversarial evaluation of Large Language Models.<n>The SCORE framework evaluates models by repeatedly testing them on the same benchmarks in various setups to give a realistic estimate of their accuracy and consistency.
  arXiv  Detail & Related papers  (2025-02-28T19:27:29Z)
• Exploring and Benchmarking the Planning Capabilities of Large Language Models [57.23454975238014]
  This work lays the foundations for improving planning capabilities of large language models (LLMs) We construct a comprehensive benchmark suite encompassing both classical planning benchmarks and natural language scenarios. We investigate the use of many-shot in-context learning to enhance LLM planning, exploring the relationship between increased context length and improved planning performance.
  arXiv  Detail & Related papers  (2024-06-18T22:57:06Z)
• Latent Semantic Consensus For Deterministic Geometric Model Fitting [109.44565542031384]
  We propose an effective method called Latent Semantic Consensus (LSC) LSC formulates the model fitting problem into two latent semantic spaces based on data points and model hypotheses. LSC is able to provide consistent and reliable solutions within only a few milliseconds for general multi-structural model fitting.
  arXiv  Detail & Related papers  (2024-03-11T05:35:38Z)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  Causal explanations of predictions of NLP systems are essential to ensure safety and establish trust. Existing methods often fall short of explaining model predictions effectively or efficiently. We propose two approaches for counterfactual (CF) approximation.
  arXiv  Detail & Related papers  (2023-10-01T07:31:04Z)
• Evaluating and Explaining Large Language Models for Code Using Syntactic Structures [74.93762031957883]
  This paper introduces ASTxplainer, an explainability method specific to Large Language Models for code. At its core, ASTxplainer provides an automated method for aligning token predictions with AST nodes. We perform an empirical evaluation on 12 popular LLMs for code using a curated dataset of the most popular GitHub projects.
  arXiv  Detail & Related papers  (2023-08-07T18:50:57Z)
• Discover, Explanation, Improvement: An Automatic Slice Detection Framework for Natural Language Processing [72.14557106085284]
  slice detection models (SDM) automatically identify underperforming groups of datapoints. This paper proposes a benchmark named "Discover, Explain, improve (DEIM)" for classification NLP tasks. Our evaluation shows that Edisa can accurately select error-prone datapoints with informative semantic features.
  arXiv  Detail & Related papers  (2022-11-08T19:00:00Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.