Are LLMs Rigorous Logical Reasoners? Empowering Natural Language Proof Generation by Stepwise Decoding with Contrastive Learning
Ying Su, Mingwen Liu, Zhijiang Guo
TL;DR
This work investigates whether large language models can serve as rigorous logical reasoners when generating natural-language proofs. It introduces ConDec, a stepwise decoding framework that employs contrastive learning and two types of hard negatives (vanilla and enhanced) to correct decoding errors such as repetition and invalid entailment. Empirical evaluation on EntailmentBank shows that ConDec achieves strong performance, comparable to or surpassing several three-stage methods, while also reducing inference costs. The study also reveals that even larger LLMs still struggle with producing fully rigorous proof chains, underscoring the value of decoding-focused training for trustworthy natural-language proofs.
Abstract
Logical reasoning is a pivotal component in the field of artificial intelligence. Proof planning, particularly in contexts requiring the validation of explanation accuracy, continues to present challenges. The recent advancement of large language models (LLMs) has led to significant progress in natural language proof planning, evolving from one-stage generators to more complex three-stage systems that include additional searchers or verifiers. While these assisted methods improve the quality of generated results, they also introduce increased search efforts and computational costs. Furthermore, the generative process itself remains underexplored. In this study, we propose a stepwise decoding approach augmented by contrastive learning to address two common errors encountered during the LLM generator's decoding process. We fine-tune the language model using both vanilla and enhanced hard negatives to mitigate these decoding errors. Empirical results demonstrate the effectiveness of our strategy. Additionally, our further analysis reveals that even larger LLMs still struggle to generate rigorous logical chains.
