Source-linked AI summary
A Closer Look at Logical Reasoning with LLMs: The Choice of Tool Matters
Long Hei Matthew Lam, Ramya Keerthy Thatikonda, Ehsan Shareghi
TL;DR
Prior tool-augmented logical reasoning studies lack consistent solver comparisons, despite tools using different input languages. This paper evaluates three solvers with LLMs on three benchmarks and finds tool choice substantially affects performance, while tool-based reasoning is limited to tasks with complete reasoning chains.
Problem
Published tool-augmented methods use varied symbolic solvers and tool-specific formalisms, leaving no consistent comparison of their performance contributions.
Source: §1 · p. 1Method
The paper compares Z3, Pyke, and Prover9 with LLMs across three deductive-reasoning benchmarks.
Source: §2.1 · p. 2, §2.3 · p. 3Results
Takeaways & Limitations
Tool choice is a consequential factor in the downstream performance of tool-augmented LLMs across the tested benchmarks and models.
Source: §5 · p. 8Tool-based reasoning is limited to deductive datasets with complete reasoning chains.
Source: Limitations · p. 8
Abstract
from arXiv · showhide
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.
1 Introduction
Prior tool-augmented logical reasoning studies used varied symbolic solvers, making their performance difficult to compare fairly. This paper compares three solvers with multiple LLMs and benchmarks, finding substantial performance differences by tool.
1 Introduction
- Existing studies used varied tools and tool-specific formalisms, leaving no consistent comparison to clarify where reported performance gains came from.Table 1 summarizes tools used in recent state-of-the-art studies.Source: §1 · p. 1, Table 1 · p. 2
- The study compares Z3, Pyke, and Prover9 using four LLMs and three deductive-reasoning benchmarks with identical prompts and varying demonstration shots.The authors also make minimal adjustments for each solver.Source: §1 · p. 1
- LLMs found Prover9 easiest to translate for, followed by Z3 and then Pyke, and Prover9 showed a smaller gap between execution rate and accuracy.This indicates Prover9 was more likely to solve a question when the LLM produced the right syntax and format.Source: §1 · p. 1
- Up to 50% performance variation occurred for each LLM under different tools across three benchmarks.Z3 and Prover9 were competitive, while Pyke was significantly inferior except on PrOntoQA.Source: §1 · p. 2
2 Tools & Logical Reasoning with LLMs
The paper compares symbolic solvers and free-form reasoning approaches for logical tasks. It describes how solver syntax and capabilities differ, and outlines tool-based reasoning’s advantages and limits.
2 Tools & Logical Reasoning with LLMs
- Symbolic solvers combine LLM translation of natural language into logical form with deterministic proof processes that avoid reasoning shortcuts and provide verifiable proof traces.The paper frames the task as determining whether conclusion C logically follows from premises P.Source: §2 · p. 2, §2.1 · p. 2
2.1 Logical Solvers
- Z3 and Prover9 use first-order logic syntax, while Pyke separates premises into rules and facts and supports simpler connectives.Z3 requires explicit variable and function types; Prover9 is sensitive to special characters and spaces; Pyke’s limited syntax restricts existential quantifiers and may not handle FOLIO well.Source: §2.1 · pp. 2–3, Figure 1 · p. 3
2.2 Free-form Logical Reasoning with LLMs
- Free-form reasoning uses LLM internal capabilities, including Chain-of-Thought prompting, but can struggle with complex tasks and is susceptible to hallucinations and shortcuts.Prior work explored first-order logic translations and training on Pyke reasoning steps.Source: §2.2 · p. 3
2.3 Tool-based Logical Reasoning with LLMs
- Prior tool-based studies adopted different solvers, but their choices were based mainly on theoretical definitions rather than empirical performance comparisons.The paper identifies a gap in understanding how LLMs, solvers, and their performance characteristics interact.Source: §2.3 · p. 3
- Tool-based reasoning offers explicit logical grounding, solver error feedback, and exhaustive rule processing, but requires complete reasoning chains and flawless translations.The authors distinguish solver-specific errors from parse errors; minor predicate-suffix mistakes can cause execution failures, and LLM changes can produce solver-specific errors.Source: §2.3 · p. 4
3 Experiments
The experiments compare LLM–solver combinations across three deductive reasoning benchmarks and examine how solver choice, world setting, reasoning depth, and demonstration shots relate to performance. Results show solver-dependent differences in executable translations and accuracy, with Prover9's execution rate most closely aligned with accuracy.
3.1 Experimental Setup
- The one-shot evaluation pairs four LLMs with Z3, Pyke, and Prover9 on three benchmarks, measuring executable formulations and overall accuracy.The test sets were limited to 200 examples for cost reasons; ProofWriter uses both world assumptions and depths 2, 3, and 5, while PrOntoQA uses its hardest 5-hop fictional-character subset.Source: §3.1 · pp. 4–5
- Table 2 reports executable rate and accuracy for the LLM–tool combinations, averaging ProofWriter results across depths 2, 3, and 5.The experiment keeps the prompt problem consistent across solvers, varying the solver-specific translation; infeasible translations yield no answer.Source: §3.1 · p. 4, Table 2 · p. 5
3.2 Main Results
- 0.98, 0.82, and 0.94 are the Pearson correlations between executable rate and accuracy for Prover9, Z3, and Pyke, respectively; Pyke is also unable to solve FOLIO.GPT models tend to favor Prover9 on simpler datasets, while Gemini and Command R+ perform better with Z3; Pyke is only competitive on PrOntoQA and performs worse on ProofWriter.Source: §3.2 · p. 5
- In fictional settings, average accuracy drops 1.38%, while Z3 and Pyke accuracy increase 6.62% and 30.87%, respectively.The comparison is between PrOntoQA Depth 5 and ProofWriter CWA Depth 5; Prover9's performance most closely aligns with the cited expectation that fictional settings reduce logical performance.Source: §3.2 · p. 6
- GPT and Gemini often maintain or improve performance as reasoning depth increases, while Command R+ generally declines from depth 2 to 5 across tools.The relationship between depth and executable rate is mixed, especially between depths 2 and 3.Source: §3.2 · p. 6
- 66.5% was the best FOLIO result, achieved with one-shot GPT-4o and Prover9; GPT-4o and Prover9 had more parse errors with higher shot counts.FOLIO translation challenges include predicate extraction from natural wording and incomplete reasoning chains; Z3's error display is cited as useful for improvement.Source: §3.2 · p. 6, Table 3 · p. 7
4 Analysis
The analysis shows that tool choice shapes both translation executability and downstream accuracy: Prover9 formulations are generally easier for LLMs to execute, while executable output does not always mean a correct answer. It also identifies distinct error patterns across tools and more difficult questions on FOLIO.
4 Analysis
- LLMs generally produce executable formulations more easily for Prover9, but executable output can still be incorrect; Z3’s executable rate reflects accuracy.GPT models were more successful at converting formulations into accurate results than Gemini-1.0-Pro and Command R+.Source: §4 · p. 7
- Z3 supports custom complex logical rules that could help with FOLIO, but the authors did not define such a rule in their experiment.They identify adding more defined complex rules as a possibility for future studies.Source: §4 · p. 7
- Non-executable formulations include parse errors and runtime errors, while Z3 also has an execution exception for inconsistent facts.The Z3 exception occurs when both the conclusion and its negation return true; these exceptions are grouped with runtime errors in Figure 3.Source: §4 · p. 7
- A parse error occurs when the parser detects nonexistent solver rules or code, whereas runtime errors can arise from inconsistent facts or malformed predicates.The paper gives using Exist() instead of Exists() in Z3 as a parse-error example and says runtime errors can be addressed through self-refinement because errors are displayed.Source: §4 · p. 7
- For GPT-4o, Pyke’s high execution rate did not yield high accuracy, while Prover9 and Z3 errors were predominantly parse errors.Pyke had three execution errors across the easier datasets; Prover9 and Z3 had around eight execution errors, and the three solvers had no common non-executable questions.Source: §4 · p. 7, Figure 3 · p. 8
- On FOLIO, execution errors increased and parse errors dropped as complex rules and predicates raised translation error rates.The analysis also reports more questions that both solvers could not process on this dataset.Source: §4 · pp. 7–8
- Around 25–30% of questions were hard for both solvers, while FOLIO brought more shared processing difficulties.The analysis associates FOLIO’s higher execution-error and lower parse-error rates with its more complex rules and predicates.Source: §4 · pp. 7–8, Figure 3 · p. 8
5 Conclusion
The conclusion compares LLMs paired with three symbolic solvers and finds that tool choice significantly affects downstream logical-reasoning performance across benchmarks and models.
5 Conclusion
- The study compares LLMs augmented with Z3, Pyke, and Prover9 to examine how solver choice affects logical-reasoning performance.The conclusion reports a significant impact across various benchmarks and LLMs.Source: §5 · p. 8
- The choice among Z3, Pyke, and Prover9 significantly affects tool-augmented LLM performance.The conclusion reports this effect across various benchmarks and LLMs.Source: §5 · p. 8
- The reported solver-choice effect spans both multiple benchmarks and multiple LLMs.The conclusion describes downstream performance impacts across these settings.Source: §5 · p. 8
Limitations
The authors limit the tool-based approach to deductive datasets with complete reasoning chains, reflecting symbolic solvers’ requirements. They also note that their experiments used built-in solver functions and suggest that additional logical rules could ease translation.
Limitations
- Tool-based reasoning is limited to deductive datasets with complete reasoning chains because of the nature of symbolic solvers.The authors suggest that LLMs might generate missing chain segments as a potential solution.Source: Limitations · p. 8
- The experiments used only the solvers’ built-in functions, although adding logical rules could enhance tool performance.The authors give a Z3 rule linking Male(x) and Not(Female(x)) as an example and suggest more complex rules could make translation easier.Source: Limitations · p. 8
- Black-box LLM outputs can vary over time, and the authors report model-specific bracket omissions in their experiments.GPT-3.5-Turbo consistently omitted a closing bracket in Forall(), while Command R+ omitted an opening bracket.Source: Limitations · p. 8
A.1 Dataset Examples
The dataset examples show logical reasoning inputs and questions from ProofWriter, PrOntoQA, and FOLIO, with answers supplied for the first two examples.
A.1 Dataset Examples
- A ProofWriter Depth 5 Open World example asks whether a conditional statement about Bonnie is true, false, or uncertain.The excerpt also includes a separate cat-and-mouse question answered “False.”Source: §A.1 · pp. 11–12
- The PrOntoQA example gives chained predicates about Wren and asks whether Wren is not metallic; its answer is “True.”The premises connect Wren being a tumpus to properties of tumpuses, wumpuses, rom puses, impuses, and dumpuses.Source: §A.1 · p. 11
- The FOLIO example presents premises about school performances, school engagement, and community membership, including alternatives for Bonnie.The excerpt supplies part of the setup but no answer.Source: §A.1 · pp. 11–12
A.2 Prompts
The appendix gives one-shot prompt formats for translating ProofWriter problems and questions into Z3, Pyke, and Prover9 inputs. Each format reflects the target solver’s syntax and representation.
A.2 Prompts
- The examples specify three distinct translation targets: Python Z3 code, Pyke facts and rules, and Prover9 first-order logic formulas.The prompts ask the model to parse both the problem and the question for each solver.Source: §A.2 · pp. 12–14
- The Z3 example requests Python solver input, with the problem and question rendered as code and the query returned as `white(Anne)`.The supplied example uses assertions and a Python function to formulate the solver input.Source: §A.2 · pp. 12–13
- The Prover9 example asks for first-order logic formulas and marks the query as `Conclusion: white(Anne)`.Its prompt introduces a first-order-logic grammar before presenting the problem and question.Source: §A.2 · p. 13
- Pyke represents predicates with Boolean arguments and encodes rules with `>>>`, while its query is written as `white(Anne)`.The example includes predicate definitions, facts, and rules in the Pyke format.Source: §A.2 · pp. 14–15
A.3 Incorrect Example Generation
The examples show translation failures arising from omitted information, ambiguous wording, and a predicate-extraction error. These errors lead to parse failure, an incorrect answer, or an execution error.
A.3 Incorrect Example Generation
- In PrOntoQA_2, omitting the fact that Stella is a yumpus causes Prover9 to raise a parse error.The example’s rules connect vumpuses to brightness, but the LLM does not translate the premise “Stella is a yumpus.”Source: §A.3 · p. 15
- In FOLIO_dev_27, the LLM misinterprets “Marvin cannot be from Earth and from Mars,” predicting Unknown instead of the stated False answer.The analysis says the wording is ambiguous and identifies an exclusive-disjunction translation as the intended interpretation.Source: §A.3 · p. 16
- In FOLIO_dev_16, translating “Some turtles exist” with `Exist` produces a NameError during execution.The example’s query is whether Rock is a turtle.Source: §A.3 · p. 16
A.4 How Z3 tackles BoardgameQA
The BoardgameQA example demonstrates how a natural-language game state, rules, and preferences are translated into Z3 code. The translation also encodes preferences by modifying rules.
A.4 How Z3 tackles BoardgameQA
- The example represents six natural-language rules as Z3 implications and quantifiers, then encodes facts about the cat, gecko, and puffin.The question asks whether the canary removes a piece of the aardvark.Source: §A.4 · p. 17
- The code represents the Meadow–Peddi name comparison as `has_same_first_letter_name(cat, puffin) == False`.The example derives this from the different first letters of “Meadow” and “Peddi.”Source: §A.4 · p. 17
- The translation encodes preferences by altering rules: it suppresses Rule5 with Rule3’s precondition and Rule1 with Rule4’s and Rule6’s preconditions.The generated code makes the preferred-over relationships explicit in the revised rule expressions.Source: §A.4 · pp. 17–18
A.5 GPT4o and Cohere command-r-plus Prompts
The appendix describes prompt adjustments for GPT-4o and Cohere Command R+ and provides solver-specific prompt formats. It also identifies Table 4 as a comparison of average tool accuracy across models, datasets, and prompt-shot settings.
A.5 GPT4o and Cohere command-r-plus Prompts
- GPT-4o and Cohere prompts were adjusted because the models tended to generate complete executable code instead of following the example format.For Z3, GPT-4o might define `s.solver()` and create a decision rule rather than generate the requested translation.Source: §A.5 · p. 18
- The Cohere Z3 prompt adds an instruction not to define `s` or `s.solver`, addressing a mismatch with the example format.The prompt also lists Z3 syntax for logical operators and quantifiers.Source: §A.5 · p. 19
- The Prover9 prompt tells GPT-4o and Cohere to translate the problem and question into first-order logic formulas and follow the example format.The prompt also asks for no further explanations and requires keeping the `:::` symbols.Source: §A.5 · p. 20
- The Pyke prompt specifies conjunction, negation, and implication syntax, then requests predicates, facts, rules, and a query in the example format.The example represents predicates with Boolean arguments and queries `white(Anne)`.Source: §A.5 · pp. 21–22
- Table 4 reports average accuracy for four LLMs across datasets and prompt-shot settings, with red highlighting the highest accuracy among the three tools.The caption marks datasets a tool could not solve with ✗.Source: Table 4 · p. 23