反馈使完美：NL 到 STL 翻译的闭环框架

信号时态逻辑 (STL) 可以对网络物理系统进行严格的验证和控制，但编写正确的规范需要大多数需求负责人所缺乏的专业知识。大语言模型可以将自然语言 (NL) 要求翻译成 STL，但仅靠更强大的翻译器就可以达到准确性上限。我们认为，这个上限源于任务的提出方式：一次性、开环翻译有点不明确。自然语言是模棱两可的，更根本的是，一个人所写的内容可能并不总是他们想要的，因此目标规范并不完全包含在输入文本中。因此，我们将 NL 到 STL 的翻译重新表述为闭环反馈过程。每个生成的公式都会被翻译回自然语言供用户检查，自然语言更正会推动修订，直到用户接受规范。用户从不阅读或编写正式语法。该框架基于反馈控制理论中常见的不对称性。从模棱两可的语言到形式逻辑的前进道路是艰难且容易出错的。从结构化 STL 到语言的反馈路径可以变得高度精确，并且精确的反馈路径可以让不精确的前向路径实现精确的闭环行为。对 500 个专家撰写的要求和 7 个LLM的实验支持了这一观点。回译解释在 99.5% 的情况下与专家判断一致。闭环细化将强模型的开环精度从约 89\% 提高到 98.0--99.2\%，并为较弱的模型带来超过 30 个百分点的收益（例如，17.6\%$\rightarrow$48.0\%）。消融表明这些收益来自反馈的语义内容，而不是重复的尝试。专家审核和 280 次用户研究进一步证实了循环的可靠性。我们还确定了一个能力阈值，超过该阈值反馈就不再有帮助。