用大模型将自然语言计划转为逻辑公式，验证其行为是否正确。
Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification
- 用大模型把自然语言计划转为时序逻辑和状态机。
- GPT-5在验证任务中达到96.3%的F1分数，语法完全正确。
- 适合研究大模型与形式化方法结合的学者或工程师。
我们提出一种新框架，通过大型语言模型（LLMs）将自然语言计划转换为克里普克结构和线性时序逻辑（LTL），并进行模型检验，以评估自然语言计划与其预期行为的一致性。我们在简化版PlanBench计划验证数据集上系统评估该框架，报告了准确率、精确率、召回率和F1分数等指标。实验表明，GPT-5在分类任务中表现优异，F1得分为96.3%，且几乎总是生成语法正确的形式化表示，可作为行为保证。但语义完全正确的形式化建模仍需未来探索。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。