LeanReasoner: Boosting Complex Logical Reasoning with Lean
Large language models (LLMs) often struggle with complex logical reasoning due to logical inconsistencies and the inherent difficulty of such reasoning. We use Lean, a theorem proving framework, to address these challenges. By formalizing logical reasoning problems into theorems 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 by 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.
Code (1)
Tasks
Automated Theorem ProvingLogical ReasoningMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Graph Neural Reasoning May Fail in Certifying Boolean Unsatisfiability
It is feasible and practically-valuable to bridge the characteristics between graph neural networks (GNNs) and logical reasoning. Despite considerable efforts and successes witnessed to solve Boolean satisfiability (SAT)…
Logical ReasoningBoosting Deductive Reasoning with Step Signals In RLHF
Logical reasoning is a crucial task for Large Language Models (LLMs), enabling them to tackle complex problems. Among reasoning tasks, multi-step reasoning poses a particular challenge. Grounded in the theory of formal l…
Formal LogicLogical ReasoningEmpower Nested Boolean Logic via Self-Supervised Curriculum Learning
Beyond the great cognitive powers showcased by language models, it is crucial to scrutinize whether their reasoning capabilities stem from strong generalization or merely exposure to relevant data. As opposed to construc…
Logical ReasoningSelf-Supervised LearningQuantum Boosting
Suppose we have a weak learning algorithm $\mathcal{A}$ for a Boolean-valued problem: $\mathcal{A}$ produces hypotheses whose bias $\gamma$ is small, only slightly better than random guessing (this could, for instance, b…
Adaptive Selection of Symbolic Languages for Improving LLM Logical Reasoning
Large Language Models (LLMs) still struggle with complex logical reasoning. While previous works achieve remarkable improvements, their performance is highly dependent on the correctness of translating natural language (…
Logical Reasoning