Kernekoncepter
Using Lean framework improves logical reasoning in large language models by formalizing problems and enhancing performance.
Resumé
The article introduces LeanReasoner, a framework that leverages the Lean theorem proving framework to address logical reasoning challenges in large language models. It discusses the struggles of LLMs with complex logical reasoning tasks, the use of symbolic solvers, and the benefits of using Lean for theorem proving. The method achieves state-of-the-art performance on datasets like FOLIO and ProofWriter by fine-tuning on annotated data. The paper details the components of LeanReasoner, including formalizer, tactic generator, proof search mechanism, and result interpreter. Experimental results show improvements in premise selection accuracy and overall proof accuracy when pretraining on theorem-proving data.
Abstract:
- Large language models (LLMs) face challenges with complex logical reasoning.
- Lean framework addresses these challenges by formalizing problems.
- Achieves state-of-the-art performance on FOLIO dataset.
Introduction:
- Logical reasoning is challenging for machine learning systems.
- Recent advances split reasoning into symbolic formalization and problem-solving.
- Lean offers a solution to connect symbolic solvers with linguistic resources.
Problem Definition and Notation:
- Task involves logical reasoning based on natural language context.
- Components include context, question, options, formalized context, formalized question, goal, tactics.
LeanReasoner:
- Composed of a formalizer, tactic generator, proof search mechanism, result interpreter.
- Formalizer converts context and question to formalized form.
- Tactic generator generates tactics based on premises.
- Proof search controls search process for proofs.
- Result interpreter analyzes proof outcomes.
Experimental Setup:
- Evaluation done on ProofWriter and FOLIO datasets.
- Training data collected for domain adaptation from mathematical theorem proofs.
Statistik
Our method achieves state-of-the-art performance on the FOLIO dataset by fine-tuning on annotated data.
Citater
"LeanReasoner enhances our ability to treat complex reasoning tasks."
"Our contributions highlight an intersection between mathematical theorem proving and logical reasoning."