Automata-based representations play an important role in control and planning in sequential decision-making, but obtaining high-level task knowledge for building automata is often difficult. Although large-scale generative language models (GLMs) can help automatically distill task knowledge, the textual outputs from GLMs are not amenable for formal verification or use in sequential decision-making. We propose a novel algorithm named GLM2FSA, which obtains high-level task knowledge represented in a finite state automaton (FSA) from a given brief description of the task goal. GLM2FSA sends queries to a GLM for task knowledge in textual form and then builds an FSA to represent the textual knowledge. It fills the gap between text and automata-based representations, and the constructed FSA can be directly utilized in formal verification. We provide an algorithm for iteratively refining the queries to the GLM based on the outcomes, e.g., counter-examples, from verification. We demonstrate the algorithm on examples that range from everyday tasks, e.g., crossing a road and making coffee, to security applications to laboratory safety protocols.

翻译：基于自动机的表示在序贯决策中的控制与规划中扮演重要角色，但获取用于构建自动机的高层级任务知识往往具有难度。尽管大规模生成语言模型（GLMs）能够自动提炼任务知识，但其文本输出不适用于形式化验证或序贯决策任务。我们提出一种名为GLM2FSA的新算法，该算法能从任务目标的简要描述中获取以有限状态自动机（FSA）表示的高层级任务知识。GLM2FSA向GLM发送文本形式的知识查询，并构建FSA来表示文本知识，填补了文本与基于自动机表示之间的鸿沟，且所构建的FSA可直接用于形式化验证。我们提供了一种基于验证结果（如反例）迭代优化GLM查询的算法。我们在从日常任务（如过马路和煮咖啡）到安全应用（如实验室安全规程）的示例中展示了该算法的有效性。