LOGIC - LM ++: Multi-Step Refinement for Symbolic Formulations (2024)

Abstract: In this paper we examine the limitations of Large Language Models (LLMs) for complex reasoning tasks. While current approaches leverage formal languages as intermediate representation for these reasoning problems, they still struggle with generating intermediate for-mal specifications with great correctness and in refining these representations. To address these issues, this paper proposes Logic-LM++, an improvement on Logic-LM (Pan et al., 2023). It uses the ability of LLMs to do pairwise comparisons, allowing the evaluation of the refinements suggested by the LLM. The paper demonstrates that Logic-LM++ outperforms Logic-LM and LLM based techniques on natural language reasoning tasks on two datasets, FOLIO, ProofWriter and AR-LSAT. Logic-LM++ show an average improvement of 18.5% on standard prompting, 12.3% on chain of thought prompting and 5% on Logic-LM.

## introduction large language models (llms) have shown proven capability of reasoning @xcite but still struggle at complex reasoning problems as seen in real world assessments @xcite . for complex multi hop reasoning tasks current state of the art approaches @xcite leverage formal languages as intermediate representation of these reasoning problems and utilize symbolic reasoners to come up with the right response. a typical workflow of such techniques consist of 3 steps: a natural language prompt which consist of the task information, a response formulation for the problem, final response generated with symbolic executor. while logic-assisted llm reasoning techniques are promising, we observe following problems in such systems: firstly, llms are poor at generating intermediate formal specifications. a few techniques try to counter this problem with a refinement loop @xcite @xcite to improve upon the syntactical correctness of the symbolic formulation. secondly, the llms are poor at repairing the formal representations with limited information with error information. for example, in figure 1 the llm initially generates a syntactically incorrect formulation. after a turn of refinement, while the llm is able to generate a response that is syntactically correct, it introduces a semantic error in the formulation by incorrectly translating the statement "no young person teaches". these kind of incorrect translations from natural language (nl) to intermediate formal specifications is a common problem we observe over the failing cases of refinement. thirdly, we observe that refinements are not always linear-resolving an error with the symbolic formulation can take multiple steps of careful edits and evaluation. the formulations generated in refinement stage in 1 introduced the wrong interpretation of "no young person teaches" to "all young people teaches". to address these challenges we propose to add following measures in logic-lm to enhance it's capabilities resulting in improved variant logic-lm++. we leverage the ability of llms to do pairwise comparison @xcite , this gives us an opportunity to evaluate the refinements suggested by the llm and do a semantic check with respect to the problem statement to ensure if the edits in the symbolic formulation generated while refinement improve the formulation semantically not just syntactically. we also improve on the refinement mechanism present in logic-lm to give more context of the problem statement during refinement stage, this eliminates cases where recommended edits are appalling and do not improve the formulation significantly. ## related work problem: all students are humans. if someone studies . . . question: based on the above information, is the following statement true, false, or uncertain? it is not true rose is a student and jerry is a human. problem: all students are humans. if someone studies, then they are a student . . . question: based on the above information . . . formulation: error: execution error predicates: student(x) ::: x is a student. . . . premises: ∀x (student(x) → human(x)) ¬∃x (young(x) ∧ teach(x)) ¬teaches(jerry) ∧ ¬manager(jerry) . . . conclusion: human(rose, manager(jerry)) predicates: student(x) ::: x is a student. . . . premises: ∀x (student(x) → human(x)) ∀x (young(x) → teach(x)) ¬teaches(jerry) ∧ ¬manager(jerry) . . . conclusion: human(rose) ∨ manager(jerry) problem statement first order logic formulation refinement prompt refined formulation with a new semantic error generated while refinement incorrect answer response: uncertain ## experiments and analysis ar-lsat @xcite is a dataset that collects all analytical logic reasoning questions from the law school admission test from 1991 to 2016. we use the test set which has 231 multiplechoice questions. ar-lsat is particularly challenging, with state-of-the-art model's performance slightly better than random guessing @xcite . proofwriter @xcite is another popular dataset on deductive logical reasoning. since the problems are in more natual language like setting it makes semantic evaluation very relevant in the problem set. logic-lm use the open-world assumption (owa) subset in which each example is a (problem, goal) pair and the label is one of proved, disproved, unknown. logic-lm evaluate the pipeline with the hardest section of proofwriter which contain total of 600 randomly sampled five step multi-hop reasoning questions. ## discussion and future work figure 3 reveals a significant observation regarding the iteration increase of logic-lm, which appears to reach convergence substantially earlier than logic-lm++. logic-lm associates attributes this to the hard limit of semantically correctness that can be achieved with logic-lm. the findings stress the importance of semantic accuracy, as the logic-lm++ exhibits consistently improved outcomes over multiple iterations, contrary to findings by logic-lm. this outcome is primarily attributed to the model's capability to revert to the initial formulation if the refined version does not offer a semantically superior representation. eventhough, logic-lm++ show promising results it only focus on symbolic formulations, this effort can be well generalised to other tool augmented techniques that rely on intermediate code representation with semantic improvements during refinement. ## conclusion we propose logic-lm++ which beats state of the art results on natural language reasoning tasks on three datasets. logic-lm++ takes leverage of llms' reasoning capabilities to show significant improvements in efficient use of logic solvers for reasoning, we demonstrate that llms show promising results at conducting comparison between symbolic formulations even in cases where generating symbolic formulations is a hard task for llm.