Automaton-based representations of task knowledge play an important role in control and planning for sequential decision-making problems. However, obtaining the high-level task knowledge required to build such automata is often difficult. Meanwhile, large-scale generative language models (GLMs) can automatically generate relevant task knowledge. However, the textual outputs from GLMs cannot be formally verified or used for sequential decision-making. We propose a novel algorithm named GLM2FSA, which constructs a finite state automaton (FSA) encoding high-level task knowledge from a brief natural-language description of the task goal. GLM2FSA first sends queries to a GLM to extract task knowledge in textual form, and then it builds an FSA to represent this text-based knowledge. The proposed algorithm thus fills the gap between natural-language task descriptions and automaton-based representations, and the constructed FSA can be formally verified against user-defined specifications. We accordingly propose a method to iteratively refine the queries to the GLM based on the outcomes, e.g., counter-examples, from verification. We demonstrate GLM2FSA's ability to build and refine automaton-based representations of everyday tasks (e.g., crossing a road), and also of tasks that require highly-specialized knowledge (e.g., executing secure multi-party computation).

翻译：基于自动机的任务知识表征在序贯决策问题的控制与规划中发挥着重要作用。然而，构建此类自动机所需的高层任务知识往往难以获取。与此同时，大规模生成式语言模型（GLM）能够自动生成相关任务知识，但其文本输出无法被形式化验证或直接用于序贯决策。我们提出一种名为GLM2FSA的新算法，该算法通过简短的**自然语言**任务目标描述，构建编码高层任务知识的**有限状态自动机**（FSA）。GLM2FSA首先向GLM发送查询以提取文本形式的任务知识，进而构建FSA来表征这些基于文本的知识。该算法填补了自然语言任务描述与基于自动机的表征之间的鸿沟，且构建的FSA可依据用户定义的规范进行形式化验证。我们据此提出一种方法，基于验证结果（如反例）迭代优化向GLM发送的查询。实验证明GLM2FSA能够构建并优化日常任务（如过马路）及需要高度专业知识任务（如执行安全多方计算）的基于自动机的表征。