Formal-LLM: Integrating Formal Language and Natural Language for Controllable LLM-based Agents

📄 arXiv: 2402.00798v4 📥 PDF

作者: Zelong Li, Wenyue Hua, Hao Wang, He Zhu, Yongfeng Zhang

分类: cs.LG, cs.AI, cs.CL, cs.FL

发布日期: 2024-02-01 (更新: 2024-08-12)

🔗 代码/项目: GITHUB

💡 一句话要点

提出Formal-LLM框架以解决LLM生成计划不可控问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 计划生成 形式语言 自然语言处理 可控性 自动机 AI代理

📋 核心要点

  1. 现有的LLM代理在生成计划时缺乏控制，常导致无效或不可执行的计划，影响用户信任。
  2. 本文提出Formal-LLM框架，通过结合自然语言与形式语言，允许开发者以自动机形式表达规划约束，从而实现可控的计划生成。
  3. 实验表明，Formal-LLM框架在多个基准和实际任务中实现了超过50%的性能提升，验证了其有效性。

📝 摘要（中文）

近年来，大型语言模型（LLMs）的进步使得AI代理能够自动生成和执行多步骤计划以解决复杂任务。然而，由于LLM内容生成过程难以控制，现有的LLM代理常常生成无效或不可执行的计划，从而影响生成计划的性能并损害用户对LLM代理的信任。为此，本文提出了一种新颖的“Formal-LLM”框架，通过将自然语言的表达能力与形式语言的精确性相结合，帮助代理开发者以自动机的形式表达其对规划过程的需求或约束。在自动机的监督下，进行基于栈的LLM计划生成过程，以确保生成的计划满足约束，从而使规划过程可控。实验结果表明，该框架在基准任务和实际任务中均实现了超过50%的整体性能提升，验证了Formal-LLM在指导代理计划生成方面的可行性和有效性。

🔬 方法详解

问题定义：本文旨在解决现有LLM代理在生成计划时的不可控性问题，导致生成的计划常常无效或不可执行，影响用户信任和代理性能。

核心思路：提出Formal-LLM框架，通过将自然语言的灵活性与形式语言的精确性结合，允许开发者以自动机的形式表达需求和约束，从而在生成计划时进行有效控制。

技术框架：该框架主要包括两个模块：首先，开发者定义需求和约束的自动机；其次，在自动机的监督下，进行基于栈的LLM计划生成，确保生成的计划符合约束条件。

关键创新：Formal-LLM的核心创新在于将形式语言引入到LLM的计划生成过程中，使得生成的计划不仅具备自然语言的表达能力，还具备形式语言的严格性，从而显著提高了计划的有效性和可执行性。

关键设计：在设计上，Formal-LLM框架采用了栈结构来管理计划生成过程，确保生成的每一步都符合自动机的约束。此外，损失函数的设计也考虑了计划的有效性与可执行性，进一步提升了生成质量。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

在实验中，Formal-LLM框架在多个基准任务和实际应用中实现了超过50%的性能提升，显著优于现有的LLM代理，证明了其在生成有效计划方面的优势和可行性。

🎯 应用场景

Formal-LLM框架具有广泛的应用潜力，尤其适用于需要高效、有效计划生成的场景，如机器人任务规划、自动化决策系统和智能助手等。通过提高计划的可控性，该框架能够增强用户对LLM代理的信任，促进其在实际应用中的广泛采用。

📄 摘要（原文）

Recent advancements on Large Language Models (LLMs) enable AI Agents to automatically generate and execute multi-step plans to solve complex tasks. However, since LLM's content generation process is hardly controllable, current LLM-based agents frequently generate invalid or non-executable plans, which jeopardizes the performance of the generated plans and corrupts users' trust in LLM-based agents. In response, this paper proposes a novel "Formal-LLM" framework for LLM-based agents by integrating the expressiveness of natural language and the precision of formal language. Specifically, the framework allows agent developers to express their requirements or constraints for the planning process as an automaton. A stack-based LLM plan generation process is then conducted under the supervision of the automaton to ensure that the generated plan satisfies the constraints, making the planning process controllable. We conduct experiments on both benchmark tasks and practical real-life tasks, and our framework achieves over 50% overall performance increase, which validates the feasibility and effectiveness of employing Formal-LLM to guide the plan generation of agents, preventing the agents from generating invalid and unsuccessful plans. Further, more controllable LLM-based agents can facilitate the broader utilization of LLM in application scenarios where high validity of planning is essential. The source code of this work is available at https://github.com/agiresearch/Formal-LLM.