LeanReasoner：用Lean提升复杂逻辑推理
LeanReasoner: Boosting Complex Logical Reasoning with Lean
AI总结：
针对LLMs复杂逻辑推理不足的问题，提出LeanReasoner，通过Lean定理证明框架将问题形式化为定理进行证伪，有效降低逻辑不一致性，在FOLIO和ProofWriter数据集上取得优异性能。
摘要：
大型语言模型（LLMs）常因逻辑不一致性及此类推理的固有困难而在复杂逻辑推理上表现不佳。我们使用Lean（一个定理证明框架）来解决这些挑战。通过将逻辑推理问题形式化为Lean中的定理，我们可以通过证明或证伪相应的定理来解决它们。该方法借助Lean的符号求解器降低了逻辑不一致的风险。它还通过使用Lean广泛的定理证明库，增强了处理复杂推理任务的能力。我们的方法在FOLIO数据集上取得了最先进的性能，并在ProofWriter上达到了接近该水平的性能。值得注意的是，这些结果是通过在每个数据集上对少于100个领域内样本进行微调而实现的。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
