Training LLMs with LogicReward for Faithful and Rigorous Reasoning

TL;DR

This work introduces LogicReward, a reward framework that enforces step-level logical correctness for LLM reasoning by leveraging a theorem prover (Isabelle/HOL) and Autoformalization with Soft Unification. It groundings premises and checks logical validity to produce a unified LogicScore that guides supervised fine-tuning and preference training, yielding state-of-the-art results on NLI and logical reasoning benchmarks. The approach demonstrates stronger reasoning faithfulness, better generalization to unseen tasks, and robustness when ground-truth labels are unavailable, highlighting its practical potential for high-stakes domains. The paper also provides extensive analyses of ablations, soft-unification benefits, and refinement strategies, and releases data and code to support reproducibility and further research.

Abstract

Although LLMs exhibit strong reasoning capabilities, existing training methods largely depend on outcome-based feedback, which can produce correct answers with flawed reasoning. Prior work introduces supervision on intermediate steps but still lacks guarantees of logical soundness, which is crucial in high-stakes scenarios where logical consistency is paramount. To address this, we propose LogicReward, a novel reward system that guides model training by enforcing step-level logical correctness with a theorem prover. We further introduce Autoformalization with Soft Unification, which reduces natural language ambiguity and improves formalization quality, enabling more effective use of the theorem prover. An 8B model trained on data constructed with LogicReward surpasses GPT-4o and o4-mini by 11.6\% and 2\% on natural language inference and logical reasoning tasks with simple training procedures. Further analysis shows that LogicReward enhances reasoning faithfulness, improves generalizability to unseen tasks such as math and commonsense reasoning, and provides a reliable reward signal even without ground-truth labels. We will release all data and code at https://llm-symbol.github.io/LogicReward.

Figures (7)

• Figure 1: Comparison between models trained on data constructed with outcome-based or probabilistic process rewards and those trained with LogicReward.
• Figure 2: LogicReward Pipeline. We begin by rolling out responses with LLMs, followed by Autoformalization with Soft Unification. Each response is first assigned a Premise Validity score by comparing the used premises $P_r$ with the given premises $P$, after which Logic Validity checks inference $I$ using Isabelle. These are combined into Reasoning Validity, which is further integrated with Outcome Validity to yield the final LogicScore. The highest-LogicScore response is used to construct SFT data, while the responses with maximum and minimum LogicScores are paired to create DPO data for training.
• Figure 3: We present an illustrative example of leveraging Isabelle’s error messages to refine the Soft Unification process. For simplicity, we show a single-step example.
• Figure 4: Panel A presents the ablation study. Panel B presents the faithfulness of different models.
• Figure 5: Panel A presents the performance of different models on previously unseen tasks. Panel B illustrates the performance when outcome information is excluded from the reward.