aiqbench analysis
This study demonstrates that integrating Large Language Models with off-the-shelf theorem provers significantly enhances the ability to solve complex logical problems like Zebra puzzles by decomposing tasks and leveraging automated feedback. The approach achieves substantial accuracy gains across multiple models, validating the utility of combining symbolic reasoning with neural generation for rigorous logic tasks.
Solving Zebra Puzzles Using Constraint-Guided Multi-Agent Systems
arXiv:2407.03956v3 Announce Type: replace-cross Abstract: 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.
Abstract: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.
Multiagent Systems (cs.MA); Computation and Language (cs.CL)
I.2.3; I.2.6; I.2.7; I.2.11
arXiv:2407.03956 [cs.MA]
(or arXiv:2407.03956v3 [cs.MA] for this version)
Full text under the publisher's open licence · 181 words