Papers Explained: Logic-LM Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning
Background
Large Langauge Models
Language Models are Machine Learning models aimed at understanding Natural Language. A common architecture for these models is to predict the next word given some context. People have tried to make these models Large and train these Large Language Models on massive datasets. Studies have noticed that LLMs have emergent abilities with scale meaning there are abilities that small Language Models don’t possess but are possessed by Large Language Models. Essentially as you make a model very good at filling out blanks in massive datasets crawled from the web, it not only gets good at understanding Natural Language but also eventually gets good at other things such as Maths / Science / Reasoning, etc. Interestingly these models also get better when you provide them in-context examples through prompts without any finetuning.
Reasoning with LLMs
One important emergent ability in LLMs is that of reasoning. LLMs are good at reasoning tasks and can improve with prompting strategies such as Chain of Thought prompting. But LLMs remain black-box probabilistic models trying their best to predict the next word correctly. It so happens that in this process of predicting the next word correctly, they end up solving more complicated tasks such as reasoning. There are no guarantees that these sequences of tokens generated to reach the final answer are coherent. There is no way to guarantee the correctness/faithfulness of the underlying process in strategies such as Chain of Thought prompting. LLMs are fundamentally Natural Language models, while they can do reasoning to some extent, they don’t provide any guarantees for the kind of reasoning they do. They often end up making mistakes and they still struggle with more complicated forms of non-linear reasoning involving planning and search.
Classical AI and Symbolic Solvers
In classical AI, logic plays a fundamental role in representing and reasoning about knowledge and information. Classical AI systems often rely on symbolic logic, such as propositional logic and first-order logic, to perform reasoning tasks. These logical systems provide a structured and formal framework for representing facts, rules, and relationships in a way that enables faithful and precise reasoning.
Unlike LLMs, which primarily rely on statistical patterns learned from vast amounts of text data, classical AI systems use explicitly defined rules and logical deductions to derive conclusions. This explicit rule-based approach allows classical AI to perform faithful reasoning because it ensures that conclusions are based on well-defined logical principles and accurately reflect the information provided.
A symbolic solver is a software tool or system that is designed to perform symbolic computations and manipulate mathematical expressions or equations in their symbolic form. Symbolic solvers are closely intertwined with logic and classical AI, serving as tools for working with symbolic representations of knowledge, performing logical inference, solving complex problems, and building expert systems. Think of Symbolic solvers as very smart calculators working with well-defined formal languages ( very similar to programming languages) performing deterministic algorithms on programs specified in these languages to answer reasoning questions (specified in these languages). These algorithms involve logical deductions from facts, searching for potential answers based on pre-existing knowledge, etc.
Symbolic Solvers work with Symbolic Languages such as Prolog. These Languages are Formal Languages with well-defined syntax (rules that tell you how to write or say things correctly so that others can understand) and semantics (meaning of these rules).
Logic-LM
Overview
Logic-LM is a novel framework to combine LLMs and Symbolic Solvers for faithful Logical Reasoning. Instead of making the LLM solve the reasoning problem (something it is not that good at inherently), Logic-LM introduces a new paradigm where the LLM represents the problem in Symbolic Language and the Symbolic Solver performs the actual reasoning on this Symbolic representation. The LLM translates the problem from Natural Language to a Symbolic Language. This is essentially a Machine Translation task (something LLMs are very good at), which purely involves understanding Language and does not involve reasoning. The Symbolic Solver does the actual reasoning which involves planning, searching, logical deductions, arithmetic, etc. The Symbolic Solver is an algorithm, that provides correctness guarantees, it is efficient, and we understand very well what is doing exactly and how it is answering questions we pose it.
The reason it can do so is it works on abstract symbols and abstract representations with well-defined syntax and semantics for which making rule-based approaches is easy. These symbolic solvers can’t be made to work on Natural Language, because it is inherently ambiguous and unstructured, unlike Symbolic Languages. Working with Natural Language is something that requires experience (in other words learning from data), it is not possible to make rule-based approaches that work well with Natural Language. LLMs on the other hand have learnt from experience on massive datasets and have become very good at understanding Natural language. Logic-LM is a novel paradigm to combines the complementary strengths of two important ideas in Classical AI (Symbolic Solvers) and Modern AI (LLMs).
Logic-LM is aimed at answering Logical Reasoning Questions posed in Natural Language. The question is accompanied by a Goal which can be for example a Multiple-Choice Question.
Problem Formulation: The goal of this stage is to translate the Natural Language Question (including both the context and query) into a Symbolic Representation. The LLM is prompted to make this conversion. The LLM is provided with detailed instructions about the Symbolic Language it has to use including details such as the grammar of the the Symbolic Language. The LLM also leverages in-context learning meaning it is given some demonstrations that show how this transformation is achieved for other related problems.
The result of this stage is the question including the goal and the context both translated to a Symbolic Representation
Symbolic Reasoner: A Symbolic Solver performs reasoning on the resulting facts to answer the Query. The result is the answer to the Query in Symbolic Representation
Result Interpretation: This Symbolic Result (in Symbolic Language) is then interpreted to generate the answer to the original query (in Natural language). This can be done using rule-based approaches or another LLM call depending on the complexity of this conversion and the nuances of the Symbolic Representation.
Self-Refinement: For complicated programs, the LLM may struggle to generate a Symbolic Representation that is syntactically correct. For such cases, self-refinement is introduced which prompts the LLM what is wrong in the Symbolic Representation (error messages from the Symbolic Solver). Along with a few shot demonstrations showing how common errors can be fixed.
Other details:
The paper evaluates Logic-LM on several datasets involving different kinds of reasoning. For each dataset, they choose a Symbolic language suited to the kind of reasoning involved in the dataset.
The paper shows that Logic-LM is better than Standard LLM prompting and Chain of Thought prompting.
The paper also shows that self-refinement is effective and with several rounds of refinement the executable rate improves (meaning more problems are converted to syntactically correct representations)
The paper shows that Logic-LM is robust (meaning it is not affected much by the difficulty of the reasoning problems) whereas the performance of other techniques degrades with an increase in the difficulty of reasoning.
