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 or making a phone call), and also of tasks that require highly-specialized knowledge (e.g., executing secure multi-party computation).

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