通过 大语言模型 将非结构化需求自动翻译为线性时序逻辑

自动将非结构化自然语言需求转换为形式化规范仍然是需求工程和形式化方法中的一个挑战，特别是对于其验证依赖于数学精确规范的安全和任务关键型系统。本文评估当代现成的 大语言模型 (LLM) 是否可以通过直接从非结构化需求生成线性时序逻辑 (LTL) 公式来帮助弥补这一差距。该研究在 15 个结构不同的要求的异构基准上使用几次提示策略检查了 6 个现代 LLM。每个需求模型对收集了五个独立的代，总共产生了 450 个候选 LTL 公式。通过手动语义评估、在 {1, 3, 5} 中对 k 进行 pass@k 以及在随机试验中捕获句法再现性的自我一致性测量来评估性能。结果表明，当前的通用 LLM 可以在非结构化 NL 到 LTL 任务上实现实际显着的性能，而无需特定于任务的 微调。该研究还通过将生成的公式与模型生成的自然语言解释配对并讨论基于时间线的 LTL 可视化的补充使用来考虑非专家的可理解性。研究结果表明，现代 LLM 正在成为半自动化形式化工作流程的可行前端助手。