一句话：提出 DeepSTL，用文法合成数据训练 Transformer 神经翻译器，将英文非形式化需求自动翻译为信号时序逻辑 STL 规约。
形式化方法虽强大，但其应用受限于编写逻辑规格需要专业知识且容易出错。本文将非形式化的自由英文需求翻译为信号时序逻辑（STL）——一种面向信息物理系统的形式规格语言。主要挑战在于缺乏公开的非形式化需求与形式规格配对数据。为此作者提出两步工作流：第一步设计基于文法的合成数据生成技术，每条输出是一个随机 STL 公式及其对应的若干可能英文翻译；第二步使用基于 Transformer 的神经翻译技术，训练出准确的英文到 STL 注意力翻译器。实验表明，对于训练充分的英文需求模式，翻译质量很高，该工作流有望扩展到更复杂的翻译任务。
Formal methods provide very powerful tools and techniques for the design and analysis of complex systems. Their practical application remains however limited, due to the widely accepted belief that formal methods require extensive expertise and a steep learning curve. Writing correct formal specifications in form of logical formulas is still considered to be a difficult and error prone task. In this paper we propose DeepSTL, a tool and technique for the translation of informal requirements, given as free English sentences, into Signal Temporal Logic (STL), a formal specification language for cyber-physical systems, used both by academia and advanced research labs in industry. A major challenge to devise such a translator is the lack of publicly available informal requirements and formal specifications. We propose a two-step workflow to address this challenge. We first design a grammar-based generation technique of synthetic data, where each output is a random STL formula and its associated set of possible English translations. In the second step, we use a state-of-the-art transformer-based neural translation technique, to train an accurate attentional translator of English to STL. The experimental results show high translation quality for patterns of English requirements that have been well trained, making this workflow promising to be extended for processing more complex translation tasks.