A Closer Look at Tool-based Logical Reasoning with LLM s: The Choice of Tool Matters (2024)

Abstract: The emergence of Large Language Models (LLMs) has demonstrated promising progress in solving logical reasoning tasks effectively. Several recent approaches have proposed to change the role of the LLM from the reasoner into a translator between natural language statements and symbolic representations which are then sent to external symbolic solvers to resolve. This paradigm has established the current state-of-the-art result in logical reasoning (i.e., deductive reasoning). However, it remains unclear whether the variance in performance of these approaches stems from the methodologies employed or the specific symbolic solvers utilized. There is a lack of consistent comparison between symbolic solvers and how they influence the overall reported performance. This is important, as each symbolic solver also has its own input symbolic language, presenting varying degrees of challenge in the translation process. To address this gap, we perform experiments on 3 deductive reasoning benchmarks with LLMs augmented with widely used symbolic solvers: Z3, Pyke, and Prover9. The tool-executable rates of symbolic translation generated by different LLMs exhibit a near 50% performance variation. This highlights a significant difference in performance rooted in very basic choices of tools. The almost linear correlation between the executable rate of translations and the accuracy of the outcomes from Prover9 highlight a strong alignment between LLMs ability to translate into Prover9 symbolic language, and the correctness of those translations.

## introduction the recent state-of-the-art approaches to logical reasoning have combined large language models (llms) with external symbolic mechanisms @xcite @xcite @xcite . this approach leverages llms' remarkable proficiency in translating natural language into symbolic representation such as first order logic (fol) or symbolic solvers' specified language (e.g., pyke, z3) @xcite , and the symbolic solver's ability to execute these translations through a fully deterministic proof process @xcite . these existing published methods try a variety of tools and tool-specific formalism. in this paper, we take 3 widely used tools: z3 (de @xcite , pyke @xcite , and prover9 @xcite and analyse the difficulty llms face for translating natural language into their desired input format, and the internal capability of these tools at solving certain satisfiability tasks. we select gpt4o, @xcite , gemini-1.0-pro @xcite and cohere command r plus, as representatives of the most capable family of llms, along with 3 widely used deductive reasoning benchmarks proofwriter @xcite , fo-lio @xcite , and prontoqa @xcite . we conduct a fair side-by-side comparison of tools by trying various number of identical prompts, demonstration shots, and minimal adjustment for each solver. our findings indicate that llms find it easier to translate for prover9, followed by z3, and lastly pyke. although prover9 can solve more questions accurately, prover9 demonstrates a lower discrepancy between execution rate and overall accuracy. this means that prover9 is more likely to solve a question given the right syntax and format produced by llms. overall, z3 and prover9 are all solver dataset papers problem z3 ar-lsat @xcite , prontoqa @xcite , proofwriter @xcite , boardgameqa @xcite logiclm, satlm analytical, deductive, fol pyke prontoqa @xcite , proofwriter @xcite logiclm, logical solver deductive, fol prover9 folio @xcite logiclm, linc deductive, fol ## tools & logical reasoning with llms the tool-based approaches to logical reasoning combine llms with external symbolic solvers. this synergy harnesses the capability of llms to convert diverse natural language statements into logical symbolic formalism. while being less flexible compared with free-form reasoning methods, such as chain-of-thought @xcite , the tool-based approach, given a correct formal translation, has important advantages: logical coherence during the reasoning (i.e., unlike llms, theorem provers cannot make reasoning shortcuts or hallucinate) is guaranteed, while the internal proof trace of the theorem provers offers a transparent and verifiable reasoning chain. ## analysis as indicated by the executable rate in as shown in figure 3 , for gpt4o, while pyke produced 3 execution errors on easier logical reasoning datasets in total, its high execution rate did not translate to high accuracy. predominately prover9 and z3's error is a parse error, with execution error controlled at around 8 questions. in addition, all non-executable questions are different, there are no common questions that all 3 solvers find difficult to solve. for folio, the execution error increases, and the parse error drops significantly. challenging datasets, such as folio, encompass a larger number of unseen, complex logical rules and more intricate predicates, which result in higher error rates during translation by llms. additionally, there is an increasing number of questions that both solvers are unable to process. this suggests that ## conclusion in this study, we investigated and compared the performance of llms combined with three widely used symbolic solvers to closely examine how each solver influences the performance of toolaugmented llms in logical reasoning. our experiments demonstrated that the choice of tools (i.e., z3, pyke, prover9) has a significant impact on the downstream performance across various benchmarks and llms.