Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LeanReasoner: Boosting Complex Logical Reasoning with Lean

Dongwei Jiang, Marcio Fonseca, Shay B. Cohen

TL;DR

This method reduces the risk of logical inconsistencies with the help of Lean’s symbolic solver and enhances the ability to treat complex reasoning tasks using Lean’s extensive library of theorem proofs.

Abstract

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.

LeanReasoner: Boosting Complex Logical Reasoning with Lean

TL;DR

This method reduces the risk of logical inconsistencies with the help of Lean’s symbolic solver and enhances the ability to treat complex reasoning tasks using Lean’s extensive library of theorem proofs.

Abstract

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.
Paper Structure (35 sections, 1 equation, 2 figures, 4 tables)

This paper contains 35 sections, 1 equation, 2 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Problem Definition and Notation
  3. LeanReasoner
  4. Formalizer
  5. Tactic Generator
  6. Proof Search
  7. Result Intepreter
  8. Experimental Setup
  9. Evaluation Data
  10. Training Data for Domain Adaptation
  11. Model Training
  12. Results
  13. Prompting-Based Baselines
  14. Comparison of formalization accuracy.
  15. Adding textual comments increases formalization accuracy.
  16. ...and 20 more sections

Figures (2)

  • 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".
  • Figure 2: Sample proofs created by LeanReasoner without pretraining (left), finetuned on Intuitive data (middle), and finetuned on Concise data (right).