L ean R easoner: Boosting Complex Logical Reasoning with Lean (2024)

Abstract: Large language models (LLMs) often struggle with complex logical reasoning due to logical inconsistencies and the inherent difficulty ofsuch reasoning. We use Lean, a theorem proving framework, to address these challenges. By formalizing logical reasoning problems intotheorems within Lean, we can solve them by proving or disproving the corresponding theorems. This method reduces the risk of logical inconsistencies with the help of Lean’s symbolic solver. It also enhances our ability to treat complex reasoning tasks using Lean’s extensive library of theorem proofs. Our method achieves state-of-the-art performance on the FOLIO dataset and achieves performance near this level on ProofWriter. Notably, these results were accomplished by fine-tuning on fewer than 100 in-domain samples for each dataset

## introduction logical reasoning, a bedrock of intelligence and a core capability of humans, has been a challenging issue for machine learning systems for a long time. llms, despite their impressive abilities to understand and generate natural language, often fall short when dealing with complex logical reasoning tasks. they frequently suffer from logical inconsistencies, where the model hallucinates and makes statements not grounded in premises, leading to spurious results @xcite . recent advances in ai have adopted a structured approach to tackle these reasoning problems by splitting them into symbolic formalization and problem-solving @xcite @xcite . specifically, the formalization step is often handled by a large language model, while problem-solving is handled by an offthe-shelf symbolic solver. in this approach, sym1 our code and data is available at https://github.com/some-random/ theorem-proving-reasoning . as a powerful theorem prover and a versatile programming language, lean (de @xcite presents a compelling solution to connect symbolic solvers with linguistic resources. much like symbolic solvers, lean has a strict checking system that ensures each reasoning step is certified. what distinguishes it, however, is its additional functionality as a programming language developed specifically for theorem proving. every day, a substantial amount of code is written in lean, capturing reasoning "nuggets" with step-by-step rationals that are useful for training llms. a few recent studies have already tapped into lean for mathematical theorem-proving tasks @xcite @xcite , showing its potential in tackling difficult reasoning challenges. in this paper, we propose leanreasoner, a leanbased framework to tackle logical reasoning problems. we use llms to formalize natural language context into lean and fine-tune a custom model on these problems using a modest amount of data annotated ourselves. as we use llms to dynamically generate solutions within the lean environment, our approach stands in stark contrast to the static, pre-defined solution-finding methods of log-iclm @xcite , which only rely on traditional techniques like forward and backward chaining, and satlm @xcite , which operates within the z3 environment using a suite of prede-arxiv:2403.13312v1 [cs.cl] 20 mar 2024 termined algorithms and heuristics. the adaptive nature of llms as a solution-finding tool allows our system to evolve continuously, harnessing a vast array of reasoning data and information. our contributions in this paper are three-fold. ## problem definition and notation the task we aim to solve is logical reasoning, taking the form of multi-choice questions given a natural language context. the answer to the question can be logically deduced based on the context. the framework we use for solving the problem is lean. 2 lean is an open-source theorem-proving programming language with vibrant community support. its current base includes over 100,000 theorems and 1,000,000 lines of code. 3 we use lean as a generic theorem prover, outside of mathematics. the task and our solution to it, consist of the following components: when we set out to answer a question using the lean prover, this question becomes our root goal. at that point, we can apply various instructions in lean to simplify or break down this primary goal and generate intermediate goals. for instance, using our earlier examples, if the root goal is proving theorem hud-son_often_meows: often_meow hudson, an intermediate goal might be proving that hudson is a cat. we aim to resolve each intermediate goal using our provided context, gradually working our way towards proving the root goal. once all intermediate goals are resolved, we have effectively proven our root goal, and the proof search concludes successfully. ## leanreasoner our framework, leanreasoner, is composed of four main components: a formalizer, a tactic generator, a proof search mechanism, and a result interpreter. the formalizer converts the context and question to formalized context and formalized 2 context, question and options context: the cow is big. the cow likes the dog. the cow visits the dog. the dog needs the cow the cow needs the cow. if something visits the dog and the dog needs the cow then it needs the cow. if the dog visits the cow then the cow visits the dog. if something needs the cow and the cow likes the dog then it likes the cow. question: does the cow like the cow options: true, false or unknown formalizer constant cow: obj constant dog: obj constant cat: obj constant big: obj -> prop constant likes: obj->obj->prop constant needs: obj->obj->prop axiom r1: ∀ x : obj, visits x dog ∧ needs dog @xmath0: visits dog @xmath1: ∀ x : obj, needs x cow ∧ likes cow @xmath2: ∀ x : obj, needs cat cow ∧ likes cow @xmath3: likes cow cow formalizer axiom t1: big cow axiom t2: likes cow dog axiom t3: visits cow dog axiom t4: needs dog cow axiom t5: needs cow cow likes cow cow no goals needs cow cow ∧ likes cow dog needs cat cow ∧ likes cow cat needs cow cow, likes cow dog likes cow dog no goals apply r3 cow sorry apply r4 exact t2 exact t5 apply r1 cow split … … unknown true false check every proof path exists path that found a proof theorem is the positive version formalizer tactic generator + proof search result interpreter figure 1 : an overview of our approach. the natural language context is first processed by the "formalizer". it then advances to the proof search stage, where all the tactics (in red) generated by the "tactic generator" are used to manipulate goals. finally, the outcome is interpreted by the "result interpreter". ## experimental setup we now describe our experimental setup: the datasets we used for evaluation and model training and the details of model training. ## results we present our experimental results, including an examination of prompting-based baseline, experimental results for leanreasoner, and a comparison between our work and other baselines. ## related work combining llm with symbolic solver. several past studies @xcite @xcite used symbolic solvers to augment neural networks with logical reasoning. many of these approaches have limitations, like the necessity for custom or specialized module designs that lack broad applicability. recent work @xcite @xcite presents a more general framework that combines contemporary llms with symbolic logic, bypassing the need to train or craft intricate modules tailored for specific problems. while our research aligns with these, we do not exclusively rely on off-the-shelf solvers. boosting the reasoning skill of llm by training on reasoning data. a common way to boost the reasoning skills of llms is by training them on data that requires some form of reasoning. as noted by @xcite , llms trained with science and math data do better on tasks that require reasoning, especially when using cot 8 prompting. other results by @xcite and @xcite suggest that powerful llms obtain advanced reasoning capabilities from being trained on code. this work is an extension of this idea to theorem proving. ## conclusion we introduced leanreasoner, a framework based on lean that augments the logical reasoning abilities of llms. we follow an extensive examination of errors from the formalization and proof generation stages that are present in our framework. we also examine the performance enhancements from pretraining on theorem-proving data and annotation styles (concise v.s. intuitive). we offered a comprehensive comparison with other techniques that highlight the strengths of our model. our results underscore the potential of integrating theoremproving frameworks with llms in advancing logical reasoning.