Solving Zebra Puzzles Using Constraint-Guided Multi-Agent Systems
作者: Shmuel Berman, Kathleen McKeown, Baishakhi Ray
分类: cs.MA, cs.CL
发布日期: 2024-07-04 (更新: 2024-07-09)
💡 一句话要点
提出ZPS：一种基于约束引导的多智能体系统，用于解决斑马难题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 多智能体系统 大型语言模型 逻辑推理 定理证明 斑马难题
📋 核心要点
- 现有方法在将自然语言线索转化为逻辑语句时存在固有的复杂性，导致大型语言模型难以解决复杂的逻辑问题，如斑马难题。
- ZPS通过将问题分解为更小的部分，并结合LLM和定理证明器，利用智能体间的反馈迭代优化，从而解决复杂逻辑难题。
- 实验结果表明，ZPS在多个LLM上均有显著提升，尤其是在GPT-4上，完全正确解的数量提升了166%。
📝 摘要（中文）
本文提出了一种多智能体系统ZPS，它集成了大型语言模型（LLMs）和一个现成的定理证明器，用于解决复杂的逻辑问题，如斑马难题。该系统将复杂的问题分解为更小、更易于管理的部分，生成SMT（Satisfiability Modulo Theories）代码，并使用定理证明器求解，同时利用智能体之间的反馈来迭代改进答案。此外，本文还引入了一个自动网格谜题评分器来评估解决方案的正确性，并通过用户研究验证了其可靠性。实验结果表明，该方法在所有测试的LLM上均有改进，其中GPT-4在完全正确解的数量上提升了166%。
🔬 方法详解
问题定义：论文旨在解决复杂逻辑推理问题，特别是斑马难题。现有方法，如思维链提示或引入符号表示，在处理此类问题时，由于自然语言到逻辑语句转换的复杂性，往往表现不足。痛点在于如何有效地利用LLM的自然语言理解能力和定理证明器的逻辑推理能力，并克服二者之间的gap。
核心思路：核心思路是将复杂的斑马难题分解为多个更小的、可管理的子问题，并分配给不同的智能体。每个智能体负责处理一部分信息，并生成相应的SMT代码。然后，使用定理证明器来验证这些SMT代码的满足性，并根据验证结果调整智能体的行为。通过智能体之间的反馈机制，不断迭代优化解决方案。
技术框架：ZPS系统包含多个智能体，每个智能体负责处理谜题的一部分信息。系统流程如下：1) 问题分解：将斑马难题分解为多个子问题；2) SMT代码生成：每个智能体根据其负责的子问题生成SMT代码；3) 定理证明：使用定理证明器验证SMT代码的满足性；4) 反馈与迭代：根据定理证明器的结果，智能体之间进行反馈，并迭代优化SMT代码，直到找到满足所有约束的解。
关键创新：关键创新在于将LLM的自然语言理解能力与定理证明器的逻辑推理能力相结合，并引入多智能体系统来协同解决复杂问题。通过将问题分解为多个子问题，并利用智能体之间的反馈机制，有效地提高了解决复杂逻辑问题的能力。此外，自动网格谜题评分器的引入，为评估解决方案的正确性提供了可靠的手段。
关键设计：论文中没有详细描述具体的参数设置、损失函数或网络结构，因为该方法主要依赖于LLM的预训练能力和定理证明器的推理能力。关键设计在于如何有效地将自然语言线索转化为SMT代码，以及如何设计智能体之间的反馈机制，以实现协同优化。
🖼️ 关键图片
📊 实验亮点
实验结果表明，ZPS系统在解决斑马难题方面取得了显著的提升。在GPT-4上，完全正确解的数量提升了166%。此外，该方法在其他LLM（具体名称未知）上也显示出改进。自动网格谜题评分器的用户研究表明，该评分器具有较高的可靠性，可以有效地评估解决方案的正确性。
🎯 应用场景
该研究成果可应用于需要复杂逻辑推理的领域，例如自动化问题求解、智能规划、知识图谱推理、软件验证等。通过将自然语言理解和逻辑推理相结合，可以提高机器在复杂环境下的决策能力，并为开发更智能的AI系统奠定基础。未来，该方法有望扩展到更广泛的逻辑推理问题，并与其他AI技术相结合，实现更强大的问题求解能力。
📄 摘要（原文）
Prior research has enhanced the ability of Large Language Models (LLMs) to solve logic puzzles using techniques such as chain-of-thought prompting or introducing a symbolic representation. These frameworks are still usually insufficient to solve complicated logical problems, such as Zebra puzzles, due to the inherent complexity of translating natural language clues into logical statements. We introduce a multi-agent system, ZPS, that integrates LLMs with an off the shelf theorem prover. This system tackles the complex puzzle-solving task by breaking down the problem into smaller, manageable parts, generating SMT (Satisfiability Modulo Theories) code to solve them with a theorem prover, and using feedback between the agents to repeatedly improve their answers. We also introduce an automated grid puzzle grader to assess the correctness of our puzzle solutions and show that the automated grader is reliable by evaluating it in a user-study. Our approach shows improvement in all three LLMs we tested, with GPT-4 showing 166% improvement in the number of fully correct solutions.