基于抽象的端到端控制与 LLM 增强的自然语言到 LTL 翻译

基于抽象的控制器设计（ABCD）为复杂信息物理系统（CPSs）的安全控制提供了有原则的框架，但将现实世界需求与其形式化综合机制对接仍然是一个主要瓶颈：这些需求最自然地以自然语言（NL）表达，而 ABCD 需要线性时序逻辑（LTL）等形式化规范。大语言模型通过将自然语言需求翻译为形式化规范，为弥合这一差距提供了一种有前景的方法。本文做出了三项贡献。首先，我们形式化了一个用于 ABCD 的 LLM 增强流水线，其中自然语言需求被翻译为 LTL 并用于形式化综合工作流中。其次，我们在 Dionysos 工具箱中实现了该流水线，并引入了一个基准，用于在逻辑多样性和语言变化下评估自然语言到 LTL 的翻译。第三，通过使用最先进的 LLM 进行的实验，我们表明，随着目标规范变得更加复杂，翻译准确性会系统性地下降，这在抽象语法树（AST）大小、时间深度和 Büchi 自动机大小等多种度量上均有体现，同时也考虑了自然语言输入的长度。这些结果揭示了一个缩放定律，将 LLM 成功率与底层 LTL 公式的内在复杂性联系起来。这些贡献共同提供了一个评估框架和一条实际集成路径，使 ABCD 更易于访问，同时保留了形式化方法的严谨性。