一句话：提出 ARTEMIS，用 LLM 将自然语言需求经结构化中间表示译为时序逻辑，并用低复杂度区分迹把人工验证开销对数级削减。
安全攸关系统的验证依赖把自然语言需求翻译为形式规约，但人工翻译易错且耗时；直接用 LLM 翻译则常输出错误结果，需要大量人工校验。本文提出 ARTEMIS 框架，将非结构化自然语言需求翻译为时序逻辑（TL）规约，并通过三项协同的自动化技术降低验证成本：（i）先用 LLM 将非结构化需求转为与 TL 存在无歧义映射的结构化自然语言，作为减少翻译错误的中间表示；（ii）针对 LLM 翻译得到的候选规约片段生成低复杂度执行迹（即系统行为），由用户逐一接受或拒绝；（iii）采用均衡区分迹生成策略剪枝候选规约空间，使每条被接受或拒绝的迹都能以对数速度消除候选，从而最小化用户需检查的迹数量。作者在五个真实安全攸关需求数据集上评估 ARTEMIS，结果表明其翻译准确率比当前最佳基线高 1.57 倍，同时将人工验证工作量最多降低 10.83 倍。
Translating natural language (NL) requirements into formal specifications is critical for verifying safety-critical systems, but it is error-prone and time-consuming when done manually. While Large Language Models (LLMs) can automate this translation, they often produce incorrect outputs that require extensive validation. In this paper, we propose ARTEMIS, an LLM-based framework that translates unstructured NL requirements into formal temporal logic (TL) specifications. Our framework reduces validation effort through three synergistic, automated techniques: (i) LLM Translation to Structured NL: We use LLMs to translate unstructured NL requirements into structured NL, which has an unambiguous mapping to TL. This intermediate representation reduces translation errors. (ii) Sub-Specification Generation: We generate low-complexity execution traces (i.e., system behaviors) that correspond to candidate specification fragments from the LLM translations. Users inspect these and accept or reject them. (iii) Balanced Distinguishing Trace Generation: We minimize the number of traces users need to inspect by pruning the candidate specification space. Each accepted or rejected trace eliminates candidates logarithmically. We evaluate ARTEMIS on five real-world safety-critical requirements datasets. The results show that it achieves 1.57X higher translation accuracy while reducing manual validation effort by up to 10.83X compared to state-of-the-art baselines.
DOI 原文 ·
@inproceedings{paperbot11550,
title = {Automating Requirements Formalization: Using LLMs and Low-Complexity Distinguishing Traces for Semantic Validation},
author = {Daniel Mendoza and Anastasia Mavridou and Andreas Katis and Caroline Trippel},
booktitle = {ICSE},
year = {2026},
doi = {10.1145/3744916.3787815}
}