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.

翻译：大型语言模型（LLM）常因逻辑不一致性及逻辑推理本身的内在难度，在复杂逻辑推理任务中表现不佳。我们采用定理证明框架Lean来应对这些挑战。通过将逻辑推理问题形式化为Lean中的定理，我们可借助证明或证伪相应定理来求解问题。该方法借助Lean的符号求解器降低了逻辑不一致风险，同时利用Lean丰富的定理证明库增强处理复杂推理任务的能力。我们的方法在FOLIO数据集上达到了最先进性能，并在ProofWriter数据集上取得了接近该水平的性能。值得注意的是，这些成果是通过在每个数据集上微调不到100个领域内样本实现的。