基于大语言模型将非结构化需求自动翻译为线性时序逻辑
Automatic Translation of Unstructured Requirements into Linear Temporal Logic through Large Language Models
浏览论文内容
中文总结 AI 辅助
本文评估6种大语言模型，通过少样本提示策略在含15个需求的基准上生成线性时序逻辑公式，验证通用LLMs无需微调即可完成非结构化自然语言转LTL任务，可作为半自动化形式化工作流的前端助手。
中文摘要 AI 辅助
将非结构化自然语言需求自动转换为形式化规范，在需求工程和形式化方法领域仍是一项挑战，对于安全关键和任务关键系统而言尤为突出，这类系统的验证依赖于数学上精确的规范。本文评估了当前现成的大语言模型（LLMs）是否可通过直接从非结构化需求生成线性时序逻辑（LTL）公式来弥合这一差距。研究采用少样本提示策略，在包含15个结构各异需求的异构基准上检验了6种现代LLMs；针对每个需求-模型对收集5次独立生成结果，总计得到450个候选LTL公式。性能通过手动语义评估、k∈{1,3,5}时的pass@k指标，以及衡量随机试验间语法可复现性的自一致性指标进行评估。结果表明，当前通用LLMs无需针对该任务进行微调，即可在非结构化自然语言转LTL任务上实现具有实际意义的性能。研究还考虑了非专家的可理解性，将生成的公式与模型生成的自然语言解释配对，并探讨了基于时间线的LTL可视化的互补使用。研究结果表明，现代LLMs正成为半自动化形式化工作流的可行前端助手。
英文摘要
Automatically translating unstructured natural language requirements into formal specifications remains a challenge in requirements engineering and formal methods, particularly for safety- and mission-critical systems whose verification depends on mathematically precise specifications. 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. The study examines six modern LLMs using a few-shot prompting strategy on a heterogeneous benchmark of 15 structurally varied requirements. Five independent generations were collected for each requirement-model pair, yielding 450 candidate LTL formulas in total. Performance was assessed through manual semantic evaluation, pass@k for k in {1, 3, 5}, and a self-consistency measure capturing syntactic reproducibility across stochastic trials. The results indicate that current general-purpose LLMs can achieve practically significant performance on the unstructured NL-to-LTL task without task-specific fine-tuning. The study also considers understandability for non-experts by pairing generated formulas with model-produced natural language explanations and discussing the complementary use of timeline-based LTL visualization. The findings suggest that modern LLMs are becoming viable front-end assistants for semi-automated formalization workflows.
