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在构建和优化日常任务（如过马路）以及需要高度专业化知识的任务（如执行安全多方计算）的基于自动机的表示方面的能力。