LogicReward: Incentivizing LLM Reasoning via Step-Wise Logical Supervision
Authors: Jundong Xu
Hao Fei
Huichi Zhou
Xin Quan
Qijun Huang
Shengqiong Wu
William Yang Wang
Mong-Li Lee
Wynne Hsu
Venue: ICLR 2026 Poster (2026)
Keywords: reasoning
logic
symbolic
Primary area: unsupervised, self-supervised, semi-supervised, and supervised representation learning
TL;DR: We introduce LogicReward, a novel reward function that guides LLMs to reason more effectively, generalize better, and remain more faithful.

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.
The code and data are available at https://llm-symbol.github.io/LogicReward.

Publiced as a conference paper at ICLR 2026
LOGICREWARD: INCENTIVIZING LLM REASONING VIA STEP-WISE LOGICAL SUPERVISION
Jundong Xu'; Hao ; Huichi Zhou?, Xin Quan', Qijun Huang', Shengqiong Wu', William Yang Wang', Mong-Li Lee', Wynne Hsu'
National University of Singapore, University College London, 'University of Manchester, Unniversity of Melbourne, University of California, Santa Barbara
ABSTRACT
Although LLMs exhibit strong reasoning capabilities, existing training methods largely depend outcome-basee 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, novel reward function that guides model training by enforcing step-level logical correctness with theorem prover. We further introduce Aut- oformalization 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 04-mini by 1 11.6% and 2% natural language inference and logi- cal reasoning tasks with simple training procedures. Further analysis shows that LogicReward enhances reasoning faithfulness, improves generalizability to seen tasks such as math and commonsense reasoning, and provides a reliable re- ward signal even without ground truth labels. The code and data are available at https: http://mmmmmmmmooomm github. 1o/ Log cReward
INTRODUCTION
Reasoning is a pinnacle of human cognition, and enabling large language models (LLMs) to perform rigorous, human-likk reasoning is a key step towards achieving artificial superintelligence (Feng eet al. 2024, Li et al.) 2025b). In prior work, a representative approach to improve LLM reasoning to prompt the model to "think step by step",, termed chain-of-thought (CoT) prompting, which has been shown to enhance LLMSs reasoning performance (Wei et al. 2022b). More recently, re- searchers have found that increasing a model's inference-time computation by allowing it to gener- ate longer reasoning chains can further enhance its reasoning capabilities (Liang et al. 2024 Snell cet al., 2024). Representative works, e.g., DeepSeek-RI (Guo et al. 2025). adopt this paradigm by harnessing the answer as a feedback signal during training to incentivize longer and more thorough reasoning chains, which enable it to tackle more complex reasoning tasks. Nevertheless, relying solely final-outcome feedback means the reasoning process receives direct supervision. Con- sequently, a model might arrive at a correct answer via flawed reasoning, resulting in an unfaithful or logically inconsistent explanation. It may also internalize such flawed reasoning during training. which can hinder its ability to solve unseen tasks where the same shortcuts fail (Chua & Evans 2025 Arcuschin et al. 2025 Chen al. 2025).
To combat the lack of step-level supervision, prior works have proposed training strategies that
provide feedback on intermediate reasoning steps (Lightman et al.) Uesato et al. (002). While such finer-grained supervision has been shown to improve reasoming ability generally, it fails to evaluate the logical validity of the reasoning chains. For example, some approaches guide intermediate steps using token-level probabilities (Zhao et al.] [025] Li et al.] (025a) or learned reward models (Zhang et al. 2025b Wang et al. 2024). but these feedbacks are inherently probabilistic and do not
"Emiil: jundong.xud ww@uu.uu.eed.
1 "Correponniigg author: Hao Fei; Email: haofei37 nus.ccuu.sg

---

Publiced as a conference paper at ICLR 2026
Premise: If legislator is found guilty of stealing government funds, they will be suspended
+
Outcome Probabilistic Reward
Tiffany Alsion was convicted of stealing govemmeen funds in 2012 and suspended from office.
Since suspension not imprisonment, she did not autometically go to prison, so the answer false.
Tiflany Alston was legissatoor Maryland's House of Delegates from 2011 to 2013. Tiffany T. Alston was
Logical Fallacy: Argument from Ignorance
(a) Models trained with aulcome based or probabilistic process rewards learned flawed logic
found guilly of stealing government funds in 2012.
LogicReward
Question: la the following claim True, False, or Uncertain? Tiffany T.
Tifaany Alston, Maryland delegate, was convicted of stealing government funds in 2012. The
Alston went to prison for stealing government funds.
low mandates suspension from office but not necessanly prison, so while her suspension certain, her imprisonment uncertain.)
Correct Non-Entenn Von-Entailment
Answer: Uncertain.
(b) Models trained with LogicReward learns valid logic
Figure I:
Comparison between models trained on data constructed with silcome-based or proba- bilistic process rewards and those trained with LogicReward.
provide formal and symbolic assessment of logical validity. As result, models trained in this way may produce reasoning that appears plausible but is logically flawed, as illustrated in Figure I (a). This limitation particularly concerning in domains that demand strict logical guarantees, such as medicine and law. More fundamentally, evidence suggests that logical reasoning itself constitutes critical driver of improved reasoning performance large language models. playing role analogous
to large-scale supervision on code and mathematics (Xie et al., 2025 Liu et al. 2025b).
To bridge this gap, we propose LogicReward, a novel reward system that evaluates the formal log- ical validity of reasoning chains. Legid comprises two components: (1) Autoformalization with Soft Unification translates natural language into formal logic while capturing implicit assump- tions and ambiguous information, thereby improving the formalization correctness; (2) LogicScore assesses reasoning quality by verifying the use of faithful information to avoid hallucination, and applying theorem prover to check the logical validity. Using LogicReward, aware datasets and train LLMs via either supervised fine-tuning (SFT (Wei et al. 2022a)) or direct preference optimization (DPO (Rafailov et al. 2023)). )) Models trained using this data demonstrate stronger rigor and greater accuracy in reasoning, reducing illogical or unsound inferences.
construct logic-
We evaluate the model trained on datasets constructed with LegidReward eight natural language inference and logical reasoning benchmarks. The model yields consistent improvements over strong baselines, with an 8B model surpassing the current state of the by 2.0% with 04-mini (OpenAl) 2025b), 16.9% with DeepSeck-R1 -1-8BB (Guo et al.) 2025), and 10% with GPT-4.1 (OpenAl [2025a). Further analysis shows that the trained models outperform those trained with datasets derived from other leading reward systems. It also demonstrates greater generalizability on other reasoning tasks, such as math and commonsense, superior faithfulness, and effectiveness even scenarios without ground-truth supervision. In summary, our main contributions are as follows:
We propose LogicReward. a novel reward system for step-level reasoning's logical validity. Using LogicReward to construct datasets and following simple training procedures, we achieve new SoTA performance on Natural Language Inference (NLI) and Logical Reasoning tasks.
The trained model shows strong generalizability to unseen tasks (c.g., mathematics, common- sense), along with improved faithfulness, and effectiveness in settings without ground-truth labels. We conduct extensive analyses of the efficacy of the proposed LogicReward mechanism, providing insights for future research.
2 RELATED WORK ON REASONING WITH LLMS
Early works improve reasoning through prompting strategies such as Chain-of-Thought (Wei et al., 2022b), Self-Consistency (Wang et al. 2023). Tree-of-Thoughts (Yao et al.) 2023). and Least-to- Most (Zhou et al. 2023). which guide models to produce intermediate steps prior to arriving at the final answer. More recently. this approach has been scaled further. OpenAl ol (Jacch et al.) 2024) improves performance by allocating additional test-time compute and generating longer rea- soning chains. Similarly, DeepSeek-R1 (Guo al. 2025) employs reinforcement learning with
2

---

Publiced as a conference paper at ICLR 2026
outcome correctness as the reward, thereby incentivizing longer reasoning chains. Building these
ideas, subsequent work has extended this approach to many different domains (Xie et al. 2025 Liu
et al. 2025d Jin al. 2025). However, these methods rely primarily on outcome-level feedback
without formally verifying the reasoning process, which can lead to explanations that are logically inconsistent (Chua & Evans 2025 Areuschin al. 2025). In contrast, our proposed LogicReward introduces step-level logical evaluation, ensuring that reasoning is both correct and logically sound.
Prior work introduced process-level crities that evaluate intermediate reasoning steps rather than only final outcomes. Existing process-level critics can be broadly categorized into probabilistic- based and symbolic-based approaches. Probabilistic methods rely on models' internal signals to train models, such as entropy and token-level probabilities (Prabhudesal et al.) [025]] Leang et al.) 2025b [uu al. 2025), or process reward models (PRMs) trained with human or automatically gen- erated step-level labels (Lightman et al. Uesato et al., 2022 /hang et al. 2025b; Wang et al.. 2024). as well as using an LLM assess step correctness (Zhang et al. 2025a Gao al. [0255] Xu al,)
2024). Although models trained on data constructed with such reward functions show improved rea- soning coherence, they remain non-deterministic and often overlook subtle logical errors. Symbolic methods, in contrast, leverage external engines (e.g., theorem provers code compilers) verify reasoning deterministically. However, current work is mostly restricted to structured domains such as mathematics or programming (Jha et al. 2025 Leang et 2025a Le al., 2022 Gehring al.) 2025). In contrast, LogicReward applies formal logical evaluation to NLI, an inherently ambiguous domain that harder to formalize but more reflective of everyday reasoning tasks.
Many other works use LLMs to tackle logical reasoning tasks by integrating symbolic structure or external solvers (Cheng et al.
2025
Liu et al. 2025a 2023 Sun et al. 2024 Servantez al. 2024
Liu et al. 2025c; Chen et al.
2026
Yang et al.) 2026). For example, LAMBADA (Kazemi et al.
2023) applies backward chaining directly over natural language, while LINC (Olausson al. 2023)
and Logic-LM (Pan et al. 2023) translate natural natural-language language statements into formal logic and rely on a prover to perform inference. SymbCoT (Xu et al., 2024) and Aristotle (Xu et al. 2025) extend this line by guiding LLMs to act as symbolic provers themselves. Other works incorporate prover feedback to iteratively refine or validate LLM-generated explanations (Quan et al. 2024a 2025]
2024b). In contrast, LogicReward employs theorem prover to construct informative rewards that guide LLM training, directly strengthening the model's internal logical-reasoning ability rather than relying on prompting or invoking a prover at inference time.
METHODOL.OGY
In this section, we detail LogicReward, its role in data construction, and the training process.
3.1 DATASET COLLECTION AND ROLLOUT
We first sample around 6,000 instances, balanced across eight widely used NLI and logical rea- soning datasets, including Multi-LogiEval (Patel al.] [024), ProofWriter (Tafjord et al. 2021), FOLIO (Han et al. 2024), ProntoQA (Saparov & He 2023), ProverQA (Qi et al. 2025). LogiQA (Liu et al., 2020), SNLI (Camburu et al.] 2018), QASC (Khot et al.) 2020). Further details are
provided in Appendix C.I Each instance consists of the premises P (Pi.P2..... Pm and
a question Q. Given (P.Q). we generate multiple candidate answers using Qwen3-8B (Yang
2025) and GPT-4o (OpenAT 2024), resulting in total of 8 responses per question, de- al.
noted as = (r1, (r1, r,,,,,,,,, ). We denote all these generations as = { {R1, R2...., Rm To ensure consistency in down- stream reasoning analysis, we standardize responses r by prompting the models to follow the format: Step 1: 81; Step 2: 82i.... Step n: 8m; Answer: A. Therefore, each response consists of reasoning steps and a final answer, denoted as = {s1, s2...., 3m A A.
where each RG contains the 8 responses to single question.
3.2 LOGICREWARD
For effective reasoning, two aspects are crucial. First, the model must ground its reasoning in the given context, using unsupported information undermines reliability. Second, the reasoning steps must also be logically valid: otherwise, the conclusions may be flawed. To capture these dimensions, introduce Premise Validity and Logic Validity, corresponding to contextual grounding and
3

---

Publiced as conference paper at ICLR 2026
(4) oog MensoningVallidiyyl wy Outcome Validiyy))))
(1)
(3)
Neeumi Resseeny
Formuliod Nessoring
(
Premise (ail LogioValldiy(en (su)
LLM Rollout
costir P)
IxabelletTV (okenihohh))
LogicScore
Min
PP
0.4
Tunad LLM
S1
S>
Chosen
Reject
Pr
Preferance Data
Maximum Livelhoad
LLM Refine
Sult Unfication
SL
Pr
0.8
Figure 2: LogicReward Pipeline. We begin by rolling out responses with LLMs, followed by Aut- oformalization with Soft Unification. Each response is first assigned a Premise Validity score by comparing the used premises P. with the given premises P. after which Logic Validity checks in- ference using Isabelle. These are combined into Reasoning Validity, which is further integrated with Outcome Validity 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.
logical soundness, respectively. For this purpose, we represent each reasoning step 8; E pair 8t = (Pr. I), where P, denotes the premise(s) used in the step, and / represents the inference made based on P.. We then define Premise Validity and Logic Validity in detail as follows.
Premise validity. For reliability, we measure Premise Validity by checking whether the referenced premises P, in each step are grounded (M. ... qm where m is the number of sentences. For each sentence 9j. we compute the cosine similarity with every given premise pı E P as C = cos( pk). We then set ej- = e Cj,k- Finally, the Premise Validity of step is defined as the average of these maxima:
If P. contains multiple sentences, we split it as P;
m
Premise Validity (s:)
PremiseValidity
max cos(aj, Pk), 95 P. Pk P PEEP
m
Logic Validity. Second, we evaluate Logic Validity determine whether reasoning follows logi- cal principles. To ensure logical guarantees, use the theorem prover Isabelle (Paulson 1994) to verify each inference step. However, reasoning needs to be converted into symbolic logic for the theorem prover to check, which is hard due to ambiguities and implicitness in natural language. For example, while humans recognize Dad and Father as equivalent, a symbolic system treats them as distinct predicates, causing validation errors. To address this, design Autoformalization with Soft Unification. We prompt the L.LM to supplement valid but implicit assumptions within each rea- soning step that not stated in P,, thereby reducing ambiguity. This soft unification increases the likelihood of correct formalization and successful verification by the theorem prover. An illustrative example is shown in the Figure 3 and more detailed analysis is provided in Section 5.5
Following Quan et al. 2024c), we parse the P, with Soft Unification into neo-davidsonia event se- manties form (Parsons 1990) and then convert Isabelle/HOL theory (Nipkow al. 2002) using an
LLM. Isabelle will then evaluate their syntactic and semantic validity. Specifically, Syntactic validity checks whether the converted theory satisfies the grammar rules. Semantic validity checks whether the inference is logically valid, which can only be evaluated with correct syntax. If the syntax is invalid, we fall back the confidence of the inference I, defined as the average token probability of the reasoning step: Conf(/) + Exer token_ for / si, where I = (f1, (61,,,.... (x) denotes the inference of reasoning step, and 1, represents the j-th token in T. We then map them
4

---

Publiced as conference paper at ICLR 2026
into unified Logic Validity score, and formally define it as follows:
if Syntax True and Logic True,
LogicValidityy (alidit((s))
if Syntax True and Logic False,
(2)
Conf(T 8;) E [0, 1]
if Syntax False.
Reasoning Validity. To capture overall reasoning validity, combine Premise Validity and Logic Validity, ensuring both faithfulness to the given context and the logical soundness of inference steps. We define the reasoning validity of generation the average, across all reasoning steps (Irl in total), of the combined Premise Validity and Logic Validity at each step. Together, they form:
ReasoningValidit(r))
Σ BLEr
(Premise (PremiieeValidiyy (s:), Logic Vagictyaiiit E [0, 1]
(3)
Outcome Validity. While reasoning faithfulness is crucial, the final prediction must still match the ground truth. To capture this, we define Outcome Validity, which takes the value if the predicted answer matches the ground truth and 0 otherwise.
Finally, we integrate both reasoning validity and outcome validity as LogicScore, denoted as:
LogicScore(r, A) -vvg(w) Reesoninn Validity(r), w2 OutcommVallidty(()) E [0.1] (4)
Here, Wi and wh denote the weights assigned to reasoning validity and outcome validity, respec- tively. These weights satisfy w1, W2 2 0 and wi + w2 = 1. For simplicity, we set w1 W2 0.5, giving equal importance to reasoning faithfulness and final correctness. Each instance D as- signed LogieScore, resulting in D,..
3.3 REFINING REASONING WITH THEOREM PROVER FEEDBACK
Based on the above rewarding process, we observed that many LLM- ALM-generated reasoning steps were judged logically invalid, even when the final answer was correct. We then randomly sampled 300 instances for in-depth analysis and identified two main sources of error. We found that, first, some inferences are logically invalid, which is expected. Second, some other inferences appear valid but judged invalid due to missing information, such as unstated assumptions, even after applying soft unification. To address these issues and improve data quality, we construct a synthetic subset, Drefined, which refines not only the inference but also the soft unification process. As shown in Figure 3 for a response judged logically invalid by Isabelle, we prompt the L.LM to iteratively refine the Soft Unification in the reasoning step using the error messages, until the reasoning is judged logically valid or a maximum iteration limit is reached. For each question Q, we randomly pick 2 of its responses refine. After refinement, each response re-evaluated using the same procedure to obtain an updated LogieScore. Further analysis is provided in Section 5.5
Notural Language Reveerring g
Formadted Reasoning
Prantos A man coalame puatyy
Holbuu
seatt costume party Soft uniiication
zalom, vaayet Someons Speech a.a vDi Agan c2
Logisdly
Refined Reasoning
Quaudse: Arnnn public opeaiing
maa public speaiang
tayy op
Orroser Comuum Glver Ageet a ayy
shows Vann
Invaldd
Relined Ressering
Prumoe Arean gieea spoach
Patiod al Gonsingg 4 Aigntii
Unifcation
Uniheattnn
Froe Massage
Sunt Liviication ia mun paas
inhreno:: pupulic
Figure 3: We present an illustrative example of leveraging Isabelle's error messages refine the Soft Unification process. For simplicity, we show single-step example.
5

---

Publiced as conference paper at ICLR 2026
Model
M.-Logi.
PW. FOLIO
Pron. QA
ProverQA
LogiQA
E-SNLI
QASC
Avg
Non-Reasoning Models
Qwen2.5-7B
53,9
63.3
59.0
69.7
97.3
66.2
GPT-4o
68.0
71.3
63.5
91.0
78.4
69.3
80.0
97.3
73.9
GPT-4.1
67.7
79.0
68.8
95.3
76.3
67.3
78.7
97.3
75.0
Reasoning Models
Skywork-o1-8B
50.9
33.3
33.3
37.8
44.3
38.0
31.7
72.9
41.2
Nemotron-8B
50,2
54.2
47.6
74.9
52.6
52.2
39.0
87.2
54.9
MiniCPM-SB
69.1
45.3
53.9
73.4
57.1
54.3
52.3
59.6
Deepseck-Ri-e -1-sckk-R1-8B
64.8
75.6
57.3
59.2
53.2
47.5
95.4
68.6
QwQ:32B
79.9
85,4
78.9
100.0
78.1
67.7
74.0
97.0
82.6
o4-mini
82.0
90.3
80.8
100.0
78.8
65.7
72.3
98.0
83.5
LogicReward
Llama3. 1aima3.1-8B-ime Insttrrt
54.7
86.0
50.5
81.2
60.4
+LogicReward
79.0
48.4
57.1
90.3
60.1
56.0
62.1
97.8
71.4
(126)
(15.5)
(111.0)
Qwen3-8B
82.5
94.5
62.8
100.0
87.2
67.9
63.5
91.3
82.3
+LogicReward
89.7
97.0
89.0
99.6
92.1
63.2
65.3
99.6
85.5
(17.3)
(12.5)
(126.)
(10.4)
(14.))
(14.7)
(11.8)
(18.3)
(?3.2)
Table 1: Main Results. Parentheses show change with Logic
3.4 TRAINING
Training Data Construction. The final training set is constructed from Dinat = D, Dellined For training, adopt SFT (Wei al., 2022a) and DPO (Rafailov et al. (2023) due to their efficiency and lower computational cost. For SFT, we use the highest LogicScore for each R E Diinal as the training target. For DPO, we select the response with the highest LogieScore as the chosen instance and the lowest as the rejected for each R. Dinal Additional analyses for data constructing strategies and training algorithms are discussed in the Appendix and F.I
Training Procedure. We Llama3. 1-8B and Qwen3-8B base models and follow two-stage training pipeline with SFT followed by DPO. We apply Low-Rank Adaptation (LoRA (Hu et al.) 2022 for computational efficiency. Further implementation details are provided in Appendix
EXPERIMENTS
4.1 EXPERIMENTS SETUP
Dataset. We evaluate on the test sets corresponding to the source dataset used for training. For each dataset, we randomly sample 300 questions whenever sufficient test data is available; otherwise, we use the entire test set. We measure accuracy by exact match.
Baselines. We include broad range of baselines. These include non-reasoning models GPT-4o OPenAA 2024), GPT-4.1 (OpenAI] 2025a). and LLAMA3.1 (All (2024), and reasoming models post-trained for reasoning tasks, including 04-MINT (OpenAl 2025b), DEEPSEEK-R -8B (Guo
et al. 2025), OWEN3-8B (Yang et al. 2025), MINICPM-8B (OpenBMB) 2024), NEMOTRON-SB (Nvidia 2025), SKYWORK-Ol (Al 2025), and QwQ-32B (Qwen Team 2025).
Since these models may have been trained on different data sources using different base models, di- rect comparison is not entirely fair. To ensure fairness, we further establish baselines using the same backbone models (LLAMA3. 1-B),, source data, and hyperparameters as LogicReward, but with alternative reward functions to construct training data from the source. Specifically, we consider (i) confidence- bassed reward (average token probability). (īi) LLM-as LLM-as-Judge (GPT-40 (OpenAl 2024
and (iii) a process reward model based on NEMOTRON- 7OR-EEARR REWARD (NVIDIA 2024).
Settings. For all non-reasoning models, we use temperature to ensure reproducibility. For rea- soning models, follow recommended practices and set the temperature to 0.6. For 04-MINI, use the default temperature, as no alternative setting is available. All models are under a zero-shot Chain-of-Thoome Thought setting. Details of the implementations provided in Appendix

---

Publiced as conference paper at ICLR 2026
Reward Systems
M.-Logi.
PW.
FOLIO
Pron. QA
ProverQA
LogiQA
E-SNLI QASC
Avg
Confidence
76.9
52.4
81.0
$2.3
57.4
89.8
64.3
LLM-as-judge!
65.8
40.3
51.5
84.6
47.5
51.5
62.7
95.3
60.2
66.7
59.1
52.4
90.6
62.1
54.3
97.0
66.0
LogicReward
79.0
48.4
57.1
90.3
60.1
56.0
62.1
97.8
71.4
Table 2: Comparison of the same model trained with different reward systems.
A
B
80
Faithfulness (%)
80
Accuracy (%)
70
65.5
66.7
68%
62.5
60
50
48.5
433
LogicReward
w/o DPO
w/o SFT
w/o LV
w/o PV
Deepseek-R1
Qwen3
LogicReward
Figure 4: Panel A presents the ablation study. Panel B presents the faithfulness of different models.
4.2 MAIN RESULTS
Overall, the model trained on data constructed by LogicReward achieves the best average performance. As shown in Table LOGICREWARD-QWERE surpasses strong baselines including -I-SEE QwQ-32B, and 04-MINI by 16.9% 2.9%, and 2.0%, respectively. Moreover, attains SoTA or near SoTA results on most benchmarks. Furthermore, LOGICREWARD-LJ. improves upon its base model by 11%, demonstrating the effectiveness of LogicReward across dif- ferent architectures. These results demonstrate that LOGICREWARD substantially enhances reason- ing robustness and establishes new SoTA performance, without relying on scaling model size.
Model trained on datasets constructed with LogicReward outperforms those trained on datasets derived from other reward functions. To ensure rigorous and fair evaluation of differ- ent reward methodologies, we conduct additional experiments where all models are trained under the same settings. As shown in Table 2 the model trained on datasets constructed with LegieReward achieves the highest overall average performance (71.4), surpassing Confidence, LLM-as-judge, and PRM by 7.1 %, 11.2%, and 5.4%, respectively. We attribute these gains to the design of LogicRe- ward, which is more closely aligned with the underlying reasoning objective. The Premise Validity component supervises models to ground their reasoning correct premises, while the Logic Valid- ity component ensures that inferences are logically valid. Training with this joint LogicReward helps the model not only select relevant evidence but also maintain rigorous logical consistency, leading to more robust reasoning performance.
ANALYSIS
We now delve deeper into our system to examine why it achieves such ad advances.
5.1 ABLATION STUDY
The ablation study in Figure 4A shows that the complete LogicReward-Llama model achieves the highest accuracy, confirming the necessity of integrating components. Removing DPO reduces performance by 5.9%, highlighting the effectiveness of using LogicReward to construct preference data. The most severe degradation (22.9%) occurs when SFT removed, demonstrating that Logi- cReward accurately captures reasoning quality; using the highest-LogicScont responses SFT tar- gets is therefore key to achieving this improvement. Excluding Logic Validity decreases accuracy by 8.9%, underscoring its importance in enforeing logical consistency and preventing reasoning short- cuts that compromise the answer's validity. Finally, removing Premise Validity results decline of 4.7%, indicating its contribution teaching the model to correct premises.

---

Publiced as conference paper at ICLR 2026
A
90
B
Accuracy (%)
80
81.8
82.4
Accuracy (%)
65.0
64,3
70-
62.5
62.3
62.4
60
58.3
60.0
59.6
55.3
50
50.1
57.5
55.0
BBH
GSMBK CommonsenseQA OutcomeReward LogicReward
Confidence
LLM-judge PRM
LogicReward
Llama-8B
Figure 5: Panel A presents the performance different models on previously unseen tasks. Panel B illustrates the performance when outcome information is excluded from the reward.
5.2 FAITHFULNESS
Lewir enhances reasoning faithfulness. Since current training either uses outcome as the only reward without process supervision or probabilistic process signals, such as confidence, without logical guarantees, intermediate reasoning steps can still be logically flawed. This poses a critical problem in high-stakes domains such as medicine and law, where trustworthiness is paramount and even minor reasoning errors can lead to serious consequences.
Therefore, we evaluate the faithfulness of their outputs. We define unfaithfulness where the final answer is correct but produced through flawed reasoning, such as misusing premises, making invalid inferences, omitting critical steps, using shorteuts, or relying on unsupported assumptions.
To measure this, we randomly sampled 100 correct instances from models' responses and manually evaluated their reasoning using the strictest criteria. In Figure 4B, our results show that the model trained on LogieReward-derive
data achieves higher faithfulness, outperforming Deepseek- RI-8B and Qwen3-8B by 25% and 11 %, respectively. The improvements stem from LogicRe- ward's ' design, in which reasoning must pass theorem prover checks earn higher reward, provid- ing rigorous, logic-verifie verified supervision, which stronger than uutcome-only or other probabilistic process signals. This discourages shortcut behaviors (e.g., guessing the answer skipping justifi- cations) and promotes reasoning paths that are logically consistent with the premises. As a result, LogicReward helps produce more faithful reasoning traces, making them more trustworthy and in- terpretable in real-world applications.
5.3 GENERALIZABILITY TO UNSEEN TASKS
LogicReward helps models improve generalizability. assess whether our model generalizes to unseen tasks, evaluate three
(OOD) benchmarks: BBH (Suzgun et al., 2023). GSM8K (Cobbe et al. 2021). and CommonsenseQAA (Talmor et al. 2019). Compared to the base model and models that rely only nutcome-based reward to construct SFT and DPO training. LogicReward-LLfan demonstrates stronger generalizability to OOD settings. As shown Figure 5A. it achieves improvements of 8.2% on BBH, 3% on GSM8K, and 13.6% on CommonseQA. These results show that the method not only enhances in-domain performance but also transfers effectively to tasks encountered during training.
The gains are most pronounced on BBH and CommonQA. For BBH, which demands structured and rigorous reasoming, LogicReward plays key role by enforcing logical validity. For Com- monsenseQA, the improvement can be attributed to our proposed Soft Unification strategy and the Synthetic Refined-Rest -eanne-nn Dataset. Soft unification works by making implicit information and assumptions explicit, which aligns closely with the nature of commonsense reasoning, where hu- mans often omit commonsense steps when reasoning. By explicitly surfacing these assumptions during training, the model learns to incorporate them into its reasoning process, thus improving its commonsense reasoning ability. The refined dataset further amplifies this effect by iteratively refining reasoning steps, including the Soft Unification, thereby improving the model's 's ability to in- corporate commonsense knowledge during reasoning. In contrast, the gains on GSM8K are smaller, likely because mathematical reasoning relies less commonsense knowledge and more domain-
8

---

Publiced as conference paper at ICLR 2026
A
B
Success Rate (%)
80
72.6
Seft Unification on Refined
w/o Soft Unification
Original
60
Ref ned
Density
40
39.5
27.3
20
13.5
Syntactic
Logic
0.25
0.50
0.75
1.00
Reward
Figure 6: Panel A reports the success rates in terms of syntactic validity and logical validity, compar- ing reasoning without soft unification, with soft unification, and with refinement. Panel B presents the reward distributions for original reasoning and refined reasoning.
specific reasoning. Overall, these findings suggest that LogicReward enhances the model's ability to learn transferable reasoning principles, improving robustness and adaptability in OOD scenarios.
5.4 LEARNING WITHOUT GROUND-TRUNE OUTCOME SUPERVISION
LewirReward outperforms other reward systems in the absence of ground-truth labels. In many real-world applications, ground-truth answers are unavailable, necessitating the use reward functions that do not require ground-truth supervision. To evaluate in this setting, we compare LogicReward against token probability, PRM, and LLM-as-judge. all without using outcome signals to construct the training data. As shown in Figure 5B. the model trained on data constructed with LogieReward achieves the highest average accuracy, surpassing Confidence, PRM, and LLM-as- judge by 1%, 2%, and 4.7%, respectively. These results underscore the advantage of LogicReward label-free scenarios.
This is because token probability reflects model's internal confidence but is purely statistical, offer- ing no guarantee logical correctness. PRMs, trained on step-by-step process labels, suffer from limited generalizability in domains lacking consistent fine-grained annotations. LLM-as-judge is also unreliable, as its evaluations can be inconsistent and subjective, driven by heuristics rather than robust logical criteria, making it unstable reward signal. In contrast, LegieReward leverages theorem- prover signals that explicitly enforce logical validity. This design avoids reliance on statis- tical confidence or costly process labels, providing principled, domain-agnostic reward signal for training reasoning models.
5.5 ANALYSIS ON SOFT UNIFICATION AND REASONING REFINEMENT
Soft Unification improves syntactic correctness and Logic Validity. shown in Figure GA, soft unification increases the rate of syntactic validity by improving syntactic correctness. This al- lows more reasoning traces to verified by the Theorem Prover. Additionally, it enhances logical validity during theorem verification. The reason is that natural language often omits implicit infor- mation or assumptions that humans can easily interpret but symbolic systems cannot, leading the Theorem Prover judge them logically invalid even if they appear valid humans. Soft unifica- tion leverages the LLMs' strong language interpretability to inject these assumptions into symbolic forms, thereby enabling the Theorem Prover perform genuine verification.
Our refinement strategy substantially improves reasoning quality. As shown in Figure the grey two-humped pattern reflects the reward distribution before refinement. It shows separation between incorrect and correct outcome rewards: the peak on the left corresponds to an outcome reward of 0, while the peak the right corresponds to an outcome reward of 1. The main mass of the distribution lies in 0-0.25 on the left and 0.5-0.75 on the right. We further analyzed this pattern and found that it occurs because instances before refinement generally receive high premise validity, indicating that the model is often using correct premises; however, they also receive low logic validity, suggesting that much of the reasoning fails the theorem prover's logical check.

---

Publiced as conference paper at ICLR 2026
After applying our refinement method (blue distribution), observe more balanced spread across the entire 0-1 range, with notable increasing density the 0.25-0.. 0.5 and 0.75-1 intervals. This shift indicates that the reward distribution is moving toward higher-quality reasoning. The improvement further supported by the mean average reward, which rises from 0.47 to 0.6. Together, these results demonstrate that our refinement method effectively enhances the quality of reasoning.
CONCLUSION
This study introduces LogicReward, novel reward system that leverages theorem prover to capture logical correctness and guide model training. We further introduce Autoformalization with Soft Unification, which reduces natural language ambiguity and improves the formalization quality, enabling a more effective use of the theorem prover. With LogicReward, we construct supervised fine-tuning (SFT) datasets and preference datasets (e.g., for DPO) train models. Experiments show that our method outperforms strong baselines such as o4-mini and GPT-4.1, demonstrating strong generalizability, faithfulness, and effectiveness even in the absence of ground-trule labels.
Future work could focus on two aspects. First, the auto-formalization process is still imperfect. Even with soft unification, certain ambiguities in natural language remain difficult to formalize. Future work could explore pipelines that proactively ask clarification questions to resolve these ambigu- ities, enabling more accurate auto-formalization. Second, the labeling process LogicReward relatively slower than approaches that only compare final outcomes. As result, in on-policy rein- forcement learning scenarios, training can take longer when using LogicReward. Future work should focus optimizing the LogicReward pipeline for efficiency, allowing it to scale more effectively to training paradigms such as on on-policy reinforcement learning.
ACKNOWLEDGMENTS
This work is supported by the Ministry of Education, Singapore, under its MOE AcRF TIER Grant (MOE-MOET3202--001),
REFERENCES
Meta AI. The Ilama 3 herd of models. CoRR, abs/2407.21783, 2024.
Skywork AI. Skywork open reasoner technical report. CoRR, abs/2505.22312, 2025.
Iván Arcuschin, Jett Janiak, Robert Krzyzanowski, Senthooran Rajamanoharan, Neel Nanda, and Arthur Conmy. Chain-of-thought reasoning in the wild is not always faithful. CoRR, abs/2503.08677 2025.
Oana-Maria Camburu, Tim Rocktäschel, Thomas Lukasiewicz, and Phil Blunsom. e-snli: Natural language inference with natural language explanations. In Proceedings of the Annual Conference on Neural Information Processing Systems, 2018.
Yanda Chen, Joe Benton, Ansh Radhakrishnan, Jonathan Uesato. Carson Denison, John Schulman, Arushi Somani, Peter Hase, Misha Wagner, Fabien Roger, Vladimir Mikulik, Samuel R. Bowman, Jan Leike, Jared Kaplan, and Ethan Perez. Reasoning models don't 't always say what they think. CoRR, abs/2505.05411 2025.
Zheng Chen, Chuan Zhou, Fengxiang Cheng, Yip Tin Po, Fenrong Liu, Yisen Wang, Jiajun Chai, Xiaohan Wang, Guojun Yin, Wei Lin, Bo Li, Haoxuan Li, and Zhouchen Lin. LogiConBench: Benchmarking logical consistencies of LLMs. In The Fourteenth International Conference Learning Representations, 2026.
Fengxiang Cheng, Haoxuan Li, Fenrong Liu, Robert van Rooij, Kun Zhang, and Zhouchen Lin. Empowering Ilms with logical reasoning: A comprehensive survey. In Proceedings of the Inter- national Joint Conference on Artificial Intelligence, pp. 10400-10408, 2025.
K. Chua and O. Evans. Are deepseek-rl and other reasoning models more faithful? CoRR, abs/2501. 1.001101110 18668,8666000 2025.
10

---

Publiced as a conference paper at ICLR 2026
Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reichhro Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems. In Proceedings of the Conference Empirical Methods in Natural Language Processing, pp. 20867-20880, 2021.
Tao Feng, Chuanyang Jin, Jingyu Liu, Kunlun Zhu, Haoqin Tu, Zirui Cheng, Guanyu Lin, and Jiaxuan You. How far are we from AGI: Are LLMS all we need? Transactions on Machine Learning Research, 2024. ISSN 2835-8856.
Yichao Fu, Xuewei Wang. Yuandong Tian, and Jiawei Zhao. Deep think with confidence. arXiv preprint arXiv:2508. 15260, 2025.
Bofei Gao, Zefan Cai, Runxin Xu, Peiyi Wang, Ce Zheng, Runji Lin, Keming Lu, Dayiheng Liu, Chang Zhou, Wen Xiao, Junjie Hu, Tianyu Liu, and Baobao Chang. Llm crities help catch bugs in mathematics: Towards better mathematical verifier with natural language feedback. In Findings of the Association for Computational Linguistics: ACL 2025, pp. 14588-14604, 2025.
Jonas Gehring, Jialu Xu, Shruti Bhosale, and et al. Rlef: Grounding code llms in execution feedback with reinforcement learning. In International Conference on Machine Learning (ICML). 2025.
Daya Guo, Dejian Yang, Haowei Zhang. Junxiao Song. Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, Xiaokang Zhang, Xingkai Yu, Yu Wu, Z. F. Wu, Zhibin Gou, Zhihong Shao, Zhuoshu Li, Ziyi Gao, Aixin Liu, Bing Xue, Bingxuan Wang. Bochao Wu, Bei Feng. Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang. Chong Ruan, Damai Dai, Deli Chen, Dongjie Ji. Erhang Li, Fangyun Lin, Fucong Dai. Fuli Luo, Guangbo Hao, Guanting Chen. Guowei Li, H. Zhang, Han Bao, Hanwei Xu, Haocheng Wang. Honghui Ding, Huajian Xin, Huazuo Gao, Hui Qu, Hui Li, Jianzhong Guo, Jiashi Li, Jiawei Wang, Jingchang Chen, Jingyang Yuan, Junjie Qiu, Junlong Li, J. I.. Cai,, Jiaqi Ni, Jian Liang, Jin Chen, Kai Dong, Kai Hu, Kaige Gao, Kang Guan, Kexin Huang, Kuai Yu, Lean Wang, Lecong Zhang, Liang Zhao, Litong Wang, Liyue Zhang, Lei Xu, Leyi Xia, Mingchuan Zhang, Minghua Zhang, Minghui Tang, Meng Li, Miaojun Wang, Mingming Li, Ning Tian, Panpan Huang, Peng Zhang, Qiancheng Wang, Qinyu Chen. Qiushi Du, Ruiqi Ge, Ruisong Zhang, Ruizhe Pan, Runji Wang. R. J. Chen, R. Jin, Ruyi Chen. Shanghao Lu, Shangyan Zhou, Shanhuang Chen, Shengfeng Ye, Shiyu Wang, Shuiping Yu, Shunfeng Zhou, Shuting Pan, and S. Li. Deepseek-rl: Incentivizing reasoning capability in Iims via reinforcement learning. Nature, (55(8081)9442)) 2025.
Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi. Martin Riddell, Wenfei Zhou, James Coady, David Peng. Yujie Qiao, Luke Benson, Lucy Sun, Alex Wardle-Solano, Hannah Szabo, Ekaterina Zubova, Matthew Burtell, Jonathan Fan, Yixin Liu, Brian Wong, Malcolm Sailor, Ansong Ni, Linyong Nan, Jungo Kasai, Tao Yu, Rui Zhang, Alexander R. Fabbri, Wojeiech Kryšcińsski, Semih Yavuz, Ye Liu, Xi Victoria Lin, Shatiq Joty, Yingbo Zhou, Caiming Xiong, Rex Ying. Arman Cohan, and Dragomir Radev. Folio: Natural language reasoning with first-order logic. In Proceedings of the Conference on Empirical Methods in Natural Language Processing, pp. 22017-22032 2024.
Edward J. Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen. Lora: Low-rank adaptation of large language models. In Proceedings of the International Conference Learning Representations, 2022.
Aaron Jaech, Risto Mikkulainen, Hao Chen, Yushi Bai, Nelson Elhage, and al. Openai ol system card. CoRR, abs/2412.11670, 2024.
Piyush Jha, Prithwish Jana, Pranavkrishna Suresh, Amny Arora, and Vijay Ganesh. RIsf: Fine- tuning iims via symbolic feedback. CoRR, 2025.
Bowen Jin, Hansi Zeng, Zhenrui Yue, Jinsung Yoon, Sercan O. Arik, Dong Wang, Hamed Zamani, and Jiawei Han. Search-rl: Training Ilms to reason and leverage search engines with reinforce- ment learning. In Proceedings of the Conference on Language Modeling, 2025.
Mehran Kazemi, Najoung Kim, Deepti Bhatia, Xin Xu, and Deepak Ramachandran. LAMBADA: Backward chaining for automated reasoning in natural language. In Proceedings of the Annual Meeting of the Association for Computational Linguistics, pp. 6547-6568, 2023.
11

---

Publiced as a conference paper at ICLR 2026
Tushar Khot, Peter Clark, Michal Guerquin, Peter Jansen, and Ashish Sabharwal. Qase: A dataset for question answering via sentence composition. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pp. 8082-8090 2020.
Hung Le, Yue Deng. Alexander M. Rush, and Akhilesh Deepak Gotmare. Coderl: Mastering code generation through pretrained models and deep reinforcement learning. In Proceedings of the Annual Conference on Neural Information Prucessing Systems, 2022.
Joshua Ong Jun Leang, Giwon Hong, Wenda Li, and Shay B. Cohen. Theorem prover as a judge for synthetic data generation. In Proceedings of the Annual Meeting of the Association for Computa- tional Linguistics, pp. 29941-29977, 2025a.
Joshua Ong Jun Leang, Zheng Zhao, Aryo Pradipta Gema, Sohee Yang, Wai-Chung Kwan, Xuanli He, Wenda Li, Pasquale Minervini, Eleonora Giunchiglia, and Shay B. Cohen. Picsar: Proba- bilistic confidence selection and ranking for reasoning chains. CoRR, 2025b.
Pengyi Li, Matvey Skripkin, Alexander Zubrey, Andrey Kuznetsov, and Ivan Oseledets. Confidence is all you need: Few-shot rl fine-tuning of language models. arXiv preprint arXiv:2506.06399 2025a.
Zhong-Zhi Li, Duzhen Zhang. Ming-Liane Zhang, Jiaxin Zhang, Zengyan Liu, Yuxuan Yao, Haotian Xu, Junhao Zheng, Pei-Jie Wang, Xiuyi Chen, Yingying Zhang, Fei Yin, Jiahua Dong. Zhijiang Guo, Le Song, and Cheng-Lin Liu. From system to system A survey of reasoning large language models. CoRR, abs/2502. 17419, 2025b.
Zhenwen Liang, Ye Liu, Tong Niu, Xiangliang Zhang, Yingbo Zhou, and Semih Yavuz. Improving LLM reasoning through scaling inference computation with collaborative verification. CoRR, abs/2410.05318,, 2024.
Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let's verify step by step. In Proceedings of the International Conference on Learning Representations, year = 2024.
Hanmeng Liu, Zhiyang Teng, Leyang Cui, Chaoli Zhang, Qiji Zhou, and Yue Zhang. LogiCoT: Logical chain-of-thought instruction tuning. In Findings of the Association for Computational Linguistics: EMNLP 2023, pp. 2908-2921, 2023.
Hanmeng Liu, Zhizhang Fu, Mengru Ding, Ruoxi Ning, Chaoli Zhang, Xiaozhang Liu, and Yue Zhang. Logical reasoning in large language models: A survey. CoRR, abs/2502.00100, 2025a.
Jian Liu, Leyang Cui, Hanmeng Liu, Dandan Huang, Yile Wang, and Yue Zhang. Logiqa: A challenge dataset for machine reading comprehension with logical reasoning. In Proceedings of the International Joint Conference on Artificial Intelligence, pp. 3622-3628, 2020.
Junteng Liu, Yuanxiang Fan, Zhuo Jiang, Han Ding, Yongyi Hu, Chi Zhang, Yiqi Shi, Shitong Weng, Aili Chen, Shiqi Chen, Yunan Huang, Mozhi Zhang, Pengyu Zhao, Junjie Yan, and Junxian He. Synlogie: Synthesizing verifiable reasoning data at scale for learning logical reasoning and beyond. arXiv preprint arXiv:2505. 19641, 2025b.
Tongxuan Liu, Wenjiang Xu, Weizhe Huang, Yuting Zeng, Jiaxing Wang, Xingyu Wang, Hailong Yang, and Jing Li. togic-of-thought: Injecting logic into contexts for full reasoning large language models. In Proceedings of the Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics, pp. 10168-10185, 2025c.
Yang Liu, Jiaqi Li, and Zilong Zheng. Rulereasoner: Reinforced rule-based reasoning via domain- aware dynamic sampling. CoRR, abs/2506.08672, 2025d.
Yu Meng, Mengzhou Xia, and Danqi Chen. Simpo: Simple preference optimization with
reference-free reward. In Proceedings of the Annual Conference on Neural Information Pro- cessing Systems, 2024.
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: Proof Assistant for Higher-Order Logic, volume 2283. Springer, 2002.
12

---

Publiced as conference paper at ICLR 2026
NVIDIA. Llama-3.1-am -eeooooooomton-- Model card. bttps://buuid..viii.. awidia/llama ---emctron--- 70b- 2024.
Nvidia. Llama-nemotron: Efficient reasoning models. CoRR, abs/2505.00949, 2025.
Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar- Joshua Tenenbaum, and Roger Levy. LINC: neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. In Proceedings of the Conference on Empirical Methods in Natural Language Processing, pp. 5153-5176, 2023.
OpenAl. Gpt-4o system card. CoRR, 2024.
OpenAl. Introducing gpt-4.1 in the BLt.s///peeaa...omm////e//////g
2025a. 2025a
OpenAL. Introducing o3 and 04-mini.
atrp:://opema...om/iddeee
int roducingg- o3 and- 04 mini/ 2025b.
OpenBMB. Minicpm: Unveiling the potential of small language models. CoRR, abs/2404.06395, 2024.
Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. Logic-LM: Empowering large lan- guage models with symbolic solvers for faithful logical reasoning. In Findings of the Association for Computational Linguistics: EMNLP 2023, pp. 3806-380 3824, 2023.
Terence Parsons. Events in the Semantics of English: A Study in Subatomic Semantics. MIT Press, 1990.
Nisarg Patel, Mohith Kulkarni, Mihir Parmar, Aashna Budhiraja, Mutsumi Nakamura, Neeraj Varsh- ney, and Chitta Baral. Multi-logieval: Towards evaluating multi-step logical reasoning ability of large language models. In Proceedings of the Conference on Empirical Methods Natural Lan- guage Processing, pp. 20856-20879, 2024.
Lawrence C. Paulson. Isabelle: A generic theorem prover. In Proceedings of the International Conference on Automated Deduction, volume 828, pp. 238-242, 1994.
Mihir Prabhudesai, Lili Chen, Alex Ippoliti, Katerina Fragkiadaki, Hao Liu, and Deepak Pathak. Maximizing confidence alone improves reasoning. arXiv preprini S0Kiv:2500.22666 2025.
Chengwen Qi, Ren Ma, Bowen Li, He Du, Binyuan Hui, Jinwang Wu, Yuanjun Laili, and Conghui He. Large language models meet symbolic provers for logical reasoning evaluation. In Proceed- ings of the International Conference on Learning Representations, 2025.
Xin Quan, Marco Valentino, Louise Dennis, and Andre Freitas. Enhancing ethical explanations of large language models through iterative symbolic refinement. In Proceedings of the Conference of the European Chapter of the Association for Computational Linguistics, pp. 1-22, 2024a.
Xin Quan, Marco Valentino, Louise A. Dennis, and Andre Freitas. Verification and refinement of natural language explanations through LLM-symbolie theorem proving. In Proceedings of the Conference on Empirical Methods in Natural Language Processing, pp. 2933-2992 2024b.
Xin Quan, Marco Valentino, Louise A. Dennis, and André Freitas. Verification and refinement of natural language explanations through llm-symbolic theorem proving. Proceedings of the 2024 Conference Empirical Methods in Natural Language Processing, pp. 2933-2993552 2024c.
Xin Quan, Marco Valentino, Louise A. Dennis, and Andre Freitas. Faithful and robust M--M-driven theorem proving for NLI explanations. In Proceedings of the Annual Meeting of the Association for Computational Linguistics, pp. 17734-17755, 2025.
Qwen Team, Qwq-32b: Embracing the power of reinforcement learning. httpp::///// http///wwnnnlnnn github. wttblllllbl..ssse 32b/ 2025.
Rafael Rafailov, Archit Sharma, Eric Mitchell, Stefano Ermon, Chelsea Finn, and Chris Manning. Direct preference optimization: Your language model is secretly a reward model. In Proceedings of the Annual Conference on Neural Information Processing Systems, 2023.
13

---

Publiced as a conference paper at ICLR 2026
Abulhair Saparov and He He. Language models are greedy reasoners: A systematic formal analysis of chain-off of ofothhtt... In Proceedings of the International Conference on Learning Representations, 2023.
Sergio Servantez, Joe Barrow, Kristian Hammond, and Rajiv Jain. Chain of logic: Rule-based rea- soning with large language models. In Findings of the Association for Computational Linguistics: ACL 2024, pp. 2721 2024.
Charlie Snell, Jaehoon Lee, Kelvin Xu, and Aviral Kumar. Improving LLM reasoning through scaling inference computation with collaborative verification. CoRR, aws/2400.0033000 2024.
Hongda Sun, Weikai Xu, Wei Liu, Jian Luan, Bin Wang. Shuo Shang, Ji- Ji-Rong Wen, and Rui Yan. DetermLR: Augmenting LLM-based logical reasoning from indeterminacy to determinacy. In Proceedings of the Annual Meeting of the Association for Computational Linguistics, pp. 9828- 9862, August 2024.
Mirac Suzgun, Nathan Scales, Nathanael Schärli, Sebastian Gehrmann, Yi Tay, Hyung Won Chung, Aakanksha Chowdhery, Quoe Le, Ed Chi, Denny Zhou, and Jason Wei. Challenging BIG-bench tasks and whether chain-of-thought can solve them. In Findings of the Association for Computa- tional Linguistics: ACL 2023, pp. 13003-13051, 2023.
Øyvind Tafjord, Bhavana Dalvi Mishra, and Peter Clark. Proofwriter: Generating implications, proofs, and abductive statements natural language. In Proceedings of the Annual Meeting of the Association for Computational Linguistics, pp. 3621-3634, 2021.
Alon Talmor, Jonathan Herzig, Nicholas Lourie, and Jonathan Berant. Commonsensega: A question answering challenge targeting commonsense knowledge. In Proceedings of the North American Chapter of the Association for Computational Linguistics, pp. 4149-4158 2019.
Jonathan Uesato, Nate Kushman, Ramana Kumar, H. Francis Song, Noah Y. Siegel, Lisa Wang, Antonia Creswell, Geoffrey Irving, and Irina Higgins. Solving math word problems with process- and outcome-based feedback. CORR, abs/2211 1.12275, 2022.
Peiyi Wang, Lei Li, Zhihong Shao, Runxin Xu, Damai Dai, Yifei Li, Deli Chen, Yu Wu, and Zhifang Sui. Math-shepherd: Verify and reinforce LLMs step-by-step without human annotations. In Proceedings of the Annual Meeting of the Association for Computational Linguisties, pp. 9426- 9439, 2024.
Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoe V. Le, Ed H. Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. In Proceedings of the International Conference on Learning Representations, 2023.
Jason Wei, Maarten Bosma, Vincent Y. Zhao, Kelvin Guu, Adams Wei Yu, Brian Lester, Nan Du, Andrew M. Dai, and Quoe V. Le. Finetuned language models are zero-shot learners. In Proceed- ings of the International Conference on Learning Representations, 2022a.
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoe V. Le, and Denny Zhou. Chain-of-thought prompting elicits reasoning in large language models. In Proceedings of the Annual Conference on Neural Information Processing Systems, pp- 14824-24833 2022b.
Tian Xie, Zitian Gao, Qingnan Ren, Haoming Luo, Yuqian Hong, Bryan Dai, Joey Zhou, Kai Qiu, Zhirong Wu, and Chong Luo. Logic-rl: Unleashing L.MM reasoning with rule-based reinforcement learning. CoRR, abs/2502. 14768, 2025.
Jundong Xu, Hao Fei, Liangming Pan, Qian Liu, Mong- Li Lee, and Wynne Hsu. Faithful logical reasoning via symbolic chain-of- -ii---fff-thuttt In Proceedings of the Annual Meeting the Association for Computational Linguistics, pp. 13326-13365, 2024.
Jundong Xu, Hao Fei, Meng Luo, Qian Liu, Liangming Pan, William Yang Wang, Preslav Nakov, Mong-Li Lee, and Wynne Hsu. Aristotle: Mastering logical reasoning with A logic-complete decompose- decompose-searchh-eeeee resovve framework. In Proceedings of the 63rd Annual Meeting of the Associ- ation for Computational Linguistics, 2025.
14

---

Publiced as conference paper at ICLR 2026
An Yang, Binyuan Hui, Ming Gong, Yingwei Pan, Jiannan Liu, Bowen Li, Xinyu Chen, et Qwen3 technical report. CoRR, 2025.
Haocheng Yang, Fengxiang Cheng, Tianjun Yao, Mengyue Yang, Jiajun Chai, Xiaohan Wang, Guo- jun Yin, Wei Lin, Soummya Kar, Fenrong Liu, Haoxuan Li, and Yisen Wang. MAD-Logic: Multi-agent debate enhances symbolic translation and reasoning. In The Fourteenth International Conference on Learning Representations, 2026.
Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Tom Griffiths, Yuan Cao, and Karthik Narasimhan. Tree of thoughts: Deliberate problem solving with large language models. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine (eds.), Proceedings of the Annual Conference Neural Information Processing Systems, 2023.
Lunjun Zhang, Arian Hosseini, Hritik Bansal, Mehran Kazemi, Aviral Kumar, and Rishabh Agar- wal. Generative verifiers: Reward modeling as next-token prediction. In Proceedings of the International Conference Learning Representations, 2025a.
Zhenru Zhang, Chujie Zheng, Yangzhen Wu, Beichen Zhang. Runji Lin, Bowen Yu, Dayiheng Liu, Jingren Zhou, and Junyang Lin. The lessons of developing process reward models in mathematical reasoning. Findings of the Association for Compulational Linguistics: ACL 2025, pp. 10495- 10516, July 2025b.
Xuandong Zhao, Zhewei Kang, Aosong Feng. Sergey Levine, and Dawn Song. Learning to reason without external rewards. arXiv preprint arXiv:2505. 19590, 2025.
Denny Zhou, Nathanael Schärli, Le Hou, Jason Wei, Nathan Scales, Xuezhi Wang, Dale Schuur- mans, Claire Cui, Olivier Bousquet, Quoe V. Le, and H. Chi. Least-to-mosi prompting enables complex reasoning in large language models. In Proceedings of the International Conference on Learning Representations, 2023.
15

---

Publiced as conference paper at ICLR 2026
APPENDIX INDEX
This supplementary material includes the following sections:
Clarification on the Use of Large Language Models (ef. A
Ethics Statement (cf. B
Reproducibility Statement (ef.
Detailed Description of Datasets and Benchmarks (cf.
C.1
Details Description of Baseline Setup (ef. D
Detailed Training Setting (cf. (E)
Extended Experimental Results (ef. F
Detailed LogicReward Algorithm (cf. G
Detailed Prompt (cf.
H
A CLARIFICATION ON THE USE OF LARGE LANGUAGE MODELS
This work utilizes large language models both research subjects and auxiliary tools through- out various stages of the research process. As research subjects, we employ Qwen3-8B and GPT- 4o as the primary models for generating candidate reasoning responses in dataset construction pipeline, where Qwen3-8B produces 5 candidate responses and GPT-4o produces 3 responses per question instance, resulting in 8 total responses per question across approximately 6,000 instances from natural language inference and logical reasoning datasets. These models serve as the founda- tion for our LogicReward system, where their generated reasoning chains undergo formal logical validity assessment through our Autoformalization with Soft Unification mechanism. Additionally, we utilize LLMs as integral components within our methodology, specifically for the autoformal- ization process that translates natural language reasoning into symbolic logic by parsing into neo- davidsonian event semantics form and converting to Isabelle/HOL. theory format, as well as for supplementing valid but implicit assumptions within reasoning steps reduce ambiguity during formal verification. Besides, we trained models Llama3.1 1-8B- 1-8B--nstruct and Qwen3-8B based on the constructed data. The baseline models in our evaluation framework represent srate-of-the-are LLMs that serve as comparison benchmarks for assessing the effectiveness of our LogicReward-reet -raandd- models. Beyond their role as research subjects and methodological components, LLMs have been employed as auxiliary tools for code development assistance and writing support throughout the re- search process. All LLM usage in this work adheres the respective terms of service and ethical guidelines.
B ETHICS STATEMENT
This research was conducted in accordance with ethical guidelines for computational research and involves the development and evaluation of LogicReward, a novel reward system that evaluates the formal logical validity of reasoning chains in large language models. All datasets used this study, including Multi-LogicEval. ProofWriter, FOLIO, ProntoQA. ProverQA. LogiQA. E-SNLI, QASC, BBH, GSMSK, and CommonsenseQA, are publicly available and widely used in natural language inference and logical reasoning research, with no new human subject data collected and all usage complying with original licensing terms and ethical guidelines. The study utilizes existing large language models (Qwen3-8B and GPT-4o) for candidate answer generation and evaluation, following respective terms of service and ethical guidelines provided by model developers. While this research aims to improve reasoning capabilities in Al systems for beneficial applications in education, scientific research, and decision support systems, acknowledge the potential dual-use nature of advanced AI capabilities and encourage responsible deployment and further research into AI safety and alignment.
16

---

Publiced as conference paper at ICLR 2026
C REPRODICIBILITY STATEMENT
To ensure reproducibility, provide all necessary details and resources. We introduce the details of the LogicReward system in Section 3.2 with pseudocode in Appendix[Gaame anonymized source code as supplementary material. We also report data construction procedures in Section 3. and Appendix C.1 baseline model settings in Appendix [D] training parameters in Appendix E and prompts in Appendix H
We will also make all code and data publicly available upon acceptance.
C.I DATASET DETAILS
We provide details of each dataset used in our experiments. The training sets are used for model training. and the test sets for evaluation; for datasets without predefined splits, we perform our random split.
Mogii-LogiEEvl (Patel al. 2024 is comprehensive logical reasoning dataset with various in- ference rules and depths. It covers three logic types, propositional, first-order, and non-monotonic, consisting of more than 30 inference rules and more than 60 of their combinations.
ProofWriter (Tafjord et al. 2021) is synthetic natural language reasoning over rule sets that pairs questions with formal proof's and abductive steps; used proof generation and QA increasing depths.
FOLIO (Han al. 2024) is human-annotatee logically complex, and diverse dataset for rea- soning in natural language (NL), equipped with first-order logic (FOL) annotations, sourced from real-world knowledge like Wikipedia.
ProntoQA (Saparov & He 2023 is synthetic QA built from first-order-logic "worlds," enabling formal parsing chain-of thought into symbolic proofs for analysis.
ProverQA (Qi et al. 2025) is created via ProverGen, which synergizes the generative strengths of Large Language Models (L.LMs) with the rigor and precision of symbolic provers, enabling the creation of a scalable, diverse, and high-quality FOL reasoning dataset.
LogiQA (Liu al. 2020) multiple-choice
compreensommi question requiring deductive reasoning, sourced from Chinese civil-service exams and translated to English.
e-SNLI (Camburu et al. 2018 a large-scale dataset for natural language inference (NLI). It con- tains about 570k sentence pairs gremise-hypothesisy each annotated with one of three labels: en- tailment, contradiction, or neutral.
QASC (Khot et al., 2020) is a multiple-choice science QA dataset requiring multi-hop reasoning by combining two supporting facts from a large corpus. It emphasizes compositional reasoning and retrieval.
We perform additional experiments using the same test set employed in the main study. addi- tion. evaluate the out-of-distribution (OOD) generalization of our method, introduce several datasets that are unseen during training and randomly sample 500 instances from each. Specifically, include:
BIG-Bench Hard (Suzgun et al. 2023), a challenging benchmark designed to probe reasoning ability across diverse tasks. We use the BoarderGameeAA specifically.
GSM8K (Cobbe et al. 2021), a collection of grade- school math word problems that require multi- step arithmetic reasoning.
Commonsense Talmoor et al. 2019), which evaluates models' ability to perform commonsense reasoning everyday scenarios.
D BASELINE DETAILS
We describe the details of baselines and how them up in this section.
17

---

Publiced as conference paper at ICLR 2026
D.1
MAIN EXPERIMENTS BASELINES
In Table
we introduce the detailed setting of the baseline models.
Model
Model_II
Temperature
GPT-4o A 2024
gpt-4o-20024-08-16 gpt-4.1-2025-04--
GPT-4.1 OpenAA
2025a
L.aMAA3T 2024
metz--lama//Lama-3---883
04-mini O 2025b)
04-mini-2025-04-16
default
DeepSeek-KI-SB (Guo al.
2025
0.6
Qwen3-8B Yang ct al. 2025
Qwen/Qwen3-8B
0.6
MiniCPM-8B (OpenBMB 2024
openbmb/MinniCCM4...M
0.6
Nemotron-88 (Nvidia 2025
0.6
Skywork-ol 2025
2025
0.6
QwQ-32B Qwen Team 2025
Qwen/QwQ-32B
0.6
Table 3: Baseline models, their official IDs, and decoding temperatures.
D.2 STRICT COMPARISONS BASELINES
To ensure strict and fair comparison, we compare different reward functions under the identical settings. For all baselines, trained with the same SFT plus DPO pipeline as LogicReward. For training data, we use the same We explain how we set up each baselines as follows:
Llama-3.1-8B-Inste as basemodel, and all baselines
source dataset D explained in Section 3.1
Token Probability. For response {s1, 92m A A, compute the average token probability of each step denoted as
P(s:)
Σ p(t),
84
BE
where p(t) is the model's probability for token t. The reasoning score is then obtained by averaging across all steps:
S(r) Σ P(s.).
Finally, the overall reward also incorporates outcome correctness Acc(A), giving the reward func- tion:
R(r) = S(r) + Acc(A).
In Section 5.4
evaluate the effectiveness of the reward functions in the absence of ground truth, we remove Ac)(A) and use S(r) as the final reward.
assign reward to each response in R {r1, . Tn We first use the highest-rewarded response + to construct the SFT dataset. We then form the DPO pair (rt.r=) by selecting ++ as the chosen instance and the lowest-rewarded response
the rejected instance.
LLM-as-Judee Judge. For the rollout the L.M (GPT-4o with temperature 0) and prompt it to select the best response + and the worst response r- For Section[5.4] we exclude that ground-truth answer from the prompt. We use r+ to construct the SFT dataset, and the pair (r+ +rr to construct the DPO dataset.
(r1, 72, -..
}, provide the ground-truth answer to
Process Reward Model. For each generation r = {81, $2...., 9m) A A, we use NEMOTRON- NOB-REWARD to compute the reward for each step and take the average across steps as the reasoning reward:
1
Rrenson (r) =
Reward(s;)..
m
18

---

Publiced as conference paper at ICLR 2026
We also compute outcome reward based the correctness of the final answer A, denoted as Routcome( (AuucoomeAA... Since these two rewards may differ in scale, we normalize both to the interval [0, using min-mat normalization:
x - min(x) max( min(x)
R(x)
Finally, the overall reward is defined as the average of the normalized reasoning and outcome re- wards:
Rina(()) = (R(Rresson))) (r)) + R Routcome (A)))
For Section 5.4 where ground-truth answers are unavailable, we exclude Routcome (A) and use only Preason (r) as the reward.
We then use the highest-rewarded response y+ to construct the SFT dataset, and form the DPO dataset using the pair (r* ,r r, where r is the chosen instance and r is the rejected instance.
addition to the above baselines, we also evaluate a baseline that uses outcome correctness the reward signal for dataset construction. Specifically, for SFT, we ran- domly select a rollout response r E R from such that r contains the correct answer. For DPO, randomly choose correct response the positive instance + and an incorrect response the negative instance r
Outcome Correctness.
E TRAINING PATAMETER
For all training conducted in this paper, we adopt the Low-Rank Adaptation (LoRA (Hu et al. 2022)
) technique. All training was conducted using two H100 GPUs.
SFT Training. For all supervised fine-tuning (SFT), gradient accumulation over 16 steps, yielding an effective batch size of 64. Training employs a linear learning-rate scheduler with initial learning rate of 3 10-5 and warmup phase of 150 steps. To improve stability, we apply gradient clipping with a maximum norm of 0.3 and enable gradient checkpointing to reduce memory overhead. Optimization is performed with RMSprop, and trained with epoch.
batch size of 4 per device with
DPO Training. For direct preference optimization (DPO), training conducted for epochs with a batch size of 2 per device and gradient accumulation over 32 steps, giving effective batch size of 64. The learning rate remains x 10-5, but we switch cosine scheduler for smoother convergence. We continue use RMSprop and apply gradient checkpointing. To regulate policy updates, we set the DPO regularisation parameter = 0.1, ensuring stability while maintaining alignment with human preferences.
F EXTENDED EXPERIMENTAL RESULTS
COMPARISON OF DIFFERENT TRAINING PARADIGMS
We conduct additional experiments on the same test set the main experiments to compare different training paradigms, including SFT, SFT DPO, and SFT + SimPO (Meng et al.) 2024). For the baselines, we use outcome correctness as the sole reward to construct the SFT and DPO training sets.
As shown in Figure 7A LogicReward consistently outperforms outcome-only supervision across all settings. Furthermore, beyond the experiments presented in the main results, also evaluate SimPO as an alternative preference-leaminn paradigm. While SimPO provides further gains over SFT, the improvements smaller than those achieved with DPO.
19

---

Publiced as conference paper at ICLR 2026
A
Outcome only LogicReward
71.4
72
Accuracy (%)
70
Accuracy (%)
66.7
65.5
60.8
60.5
60
68
SFT
SimPO
Max-Min
Dual-Threshold
Random
Figure 7: Panel A presents comparison across training paradigms, while Panel B reports results for different data selection strategies.
F.2 DIFFERENT DATA CONSTRUCTION STRATEGIES
We evaluate three strategies for constructing DPO pairs with responses scored by reward model.
Top vs. Bottom (Max-Min). For each question, we select the highest-rewarded response as the chosen sample r and the lowest-rewarded response as the rejected sample r", yielding a single DPO pair (r+,r") ,r
Dual-Threshold (2 0.75 vs. < 0.25). For each question, all responses with reward 2 0.75 are treated as chosen and all responses with reward < 0.25 are treated as rejected; this results in multiple DPO pairs for each question.
Random Above/Below 0.5 (> 0.5 vs. < 0.5). For each question, we uniformly sample response with reward 0.5 as r and one with reward < 0.5 r- to form single DPO pair.
As shown in Figure 78, Max-Min yields the highest accuracy (71.43%), as selecting the globally best and worst responses maximizes the reward margin per pair and produces a strong learning signal. Dual-Threshold attains lower performance (67.67%) while it generates inclusion of near-threshold and redundant pairs dilutes pair quality and reduces the effective mar- gin relative Max-Min. Random Above/Below 0.5 performs the worst (67.03%), since random sampling around a mid threshold introduces label noise (e.g., mediocre "chosen" responses) and typically yields small reward margins, limiting gains.
pairs, the
Practical Takeaway. When reward estimates are reliable, prefer Max-Min pairing for the strongest signal. Use Dual-Threshold to expand the preference dataset when broader coverage desired, but expect smaller gains. Avoid Random Above/Below unless necessary, its noisier signal and weaker margins hinder performance.
G ALGORITHM
We introduce the full LogicReward algorithm, following its components Premise Validity and Logic Validity.
Algorithm LogicReward
Require: Question (P,Q) Q) with premises P (p1,... .., pm and question Q: Large Language Model; rollout size n=8 1: Responses <- Rollout(Large Language Model, (P, Q). n))
// Generate n==8 formatted responses, each as list of reasoning steps and final answer.
2: for all response E Responses do
3: sumPremise +- 0: sumLogic +
4: for all step E response do
5: sumPremise + sumPremise + PremiseValidityy Validitty(tepppremiss/. PP) suml agic suml.ogic - LogieValidiyy Validity (step( P)
6:
// PremiseValiditt checks grounding in P; LogicValidity checks formal soundness.
20

---

10: end for Publiced as conference paper at ICLR 2026
7:
end for
8: numSteps + #1 e response)
sumPremise sumLogic
9:
return numSteps
Average over steps gives the response- level Logic Score in [0, 1].
Algorithm 2 Premise Validity
Require: Premises { Pm) J:
a step text step containing the referenced premise(s)
1: similarityList +
2: for all E SplittyyPrriod((see)) do
3: for all p P' do
4:
similartyList.Appendd p))
Use cosine similarity between sentence and premise p (embedding space).
5: end for
6: end for
7: return max(similarityList)
Highest match across premises discourages hallucinated references.
Algorithm Logic Validity with Theorem Prover and Soft Unification
Require: Premises P;
step with one or more inferences; a Theorem Prover; a LLM;; a Prompt auto- formalization with soft unification
1: for all inference step do
2: symbolic logic <- LLM(inference, soft unification Prompt)
Transform inference into symbolic logic with soft unification to reduce ambiguity.
3:
(syntaxOK, logicOK) <- (ThooeemProver((ifeeneee))
4: if syntaxOK True then
5:
return 1 if logicOK = True else 0
// Syntactically valid formulas receive hinary semantic validation.
6:
else
7:
Validialidityy <- AygTokeeProbabiityyLnnne (Large Language Model, inference P))
8:
return token Validity
// Fallback: average token probability in [0, 1] when syntax is invalid.
9: end if end for
H PROMPT
We use the following prompt to roll out responses:
Rollout Prompt
System
You are a careful reasoner. Read the premise(s) and the question, then reason step-by-step using numbered steps.
For each step, write exactly three lines in this order and wording: Premi se: Soft Unification: Conclusion:
Formatting rules:
Title each step as Step N:, where N starts at I and increments by 1,
The Premi se must either (i) one given premises, or (ii) Conclusion from previous step.
The Soft Unification must be a commonsense, assumption, or implicit in- formation that is contextually reasonable.
The Conclusion must be new information that logically follows from the Premi se and the Assumption.
21

---

Publiced as conference paper at ICLR 2026
After all steps, output final line in the format: Final answer: [xxx]
If the question has choices (A), (B), (C), write only the option letter in the brackets (e.g., [A]).
Otherwise, write only the required label (e.g., [True], [False], [enta 1ment], (contradiction) [neutral]).
Do not use XML tags. Do not add extra commentary before or after the steps or the final line.
Example:
Premise: Harry read a book. People who read books will be smart.
Question: Will Harry be smart? Answer with tnee/falseunknnown.
Reasoning: Step 1: Premise: Harry read a book. People who read books will be smart.
Assumption: Harry is person. A person is people. Conclusion: Harry will be smart.
Final answer: [True]
Answer the question below: Premises: [PREMISES]
Question: [QUESTION]
22


Reviews:
[{"review_id": "1ISW6OiQH8", "reviewer": "Reviewer_PCn6", "summary": "This paper introduces LogicReward, a reward system that enforces logical correctness of the reasoning traces of LLMs with a theorem prover. It also comes with \"autoformalization with soft unification\", which is a technique that prompts the LLM to provide implicit assumptions in the reasoning steps to reduce ambiguity in the statements. The resulting LogicScore is used to train LLMs under SFT and DPO settings. The overall method demonstrates solid performance increase on a variety of logical reasoning benchmarks, allowing small 8B models to outperform larger reasoning models. Furthermore, LogicReward performs better than several alternative reward systems such as LLM-as-judge.", "questions": "- Why specifically using the pipeline of SFT followed by DPO? A few more sentences of justifications/intuitions would be good.\n- It would be good to clearly label or state how many test problems are used for each benchmark (wrt Sec 4.1).\n- Minor: on Line 190, there is a typo. It should be \"neo-davidsonia[n]\".", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "- This paper tackles a good problem in LLM research, and the contribution is timely and generally principled.\n- LogicReward achieves strong empirical performance. I appreciate that the authors evaluate the models/methods on a pretty large set of logical reasoning benchmarks.\n- The study includes fair ablation studies and comparisons (e.g., Table 2 and Figure 4), corroborating the advantage of LogicReward.\n- The generalizability analysis is interesting and encouraging (Sec. 5.3): LogicReward does not only help with strictly logical reasoning tasks—it may help with other kinds of reasoning too (e.g. grade school math).", "weaknesses": "- The related work section (Sec. 2) is incomplete. Much prior work has done on LLM logical reasoning using a range of different techniques, from earlier work like [1] to neurosymbolic approaches like [2, 3]. I think a dedicated paragraph is needed (could be in between \"general reasoning\" and \"reward models\") given the topic of this paper.\n- While LogicReward seems a good fit for logical reasoning tasks, many kinds of reasoning are harder to (auto)formalize. Do the authors expect their method to work on harder mathematical problems like AIME or code generation tasks? It is not necessary to evaluate on other benchmarks here, but some more thorough discussion would be ideal. In other words, what are the soft and hard limitations of this approach?\n\n[1] Kazemi, M., Kim, N., Bhatia, D., Xu, X., & Ramachandran, D. (2022). Lambada: Backward chaining for automated reasoning in natural language. arXiv preprint arXiv:2212.13894.\n[1] Olausson, T. X., Gu, A., Lipkin, B., Zhang, C. E., Solar-Lezama, A., Tenenbaum, J. B., & Levy, R. (2023). LINC: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. arXiv preprint arXiv:2310.15164.\n[2] Pan, L., Albalak, A., Wang, X., & Wang, W. Y. (2023). Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning. arXiv preprint arXiv:2305.12295.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "9u1LZ2vVjp", "reviewer": "Reviewer_HUW3", "summary": "The paper targets the flaw of outcome-based training that can yield correct answers with incorrect reasoning, proposing LogicReward, which enforces step-level logical correctness via a theorem prover, plus Autoformalization with Soft Unification to reduce ambiguity and improve formalization. An 8B model trained on LogicReward data surpasses GPT-4o and o4-mini by 11.6% and 2% on natural language inference and logical reasoning, improves reasoning faithfulness, generalizes to math and commonsense, and provides a reliable reward signal without ground-truth labels. The authors plan to release data and code upon acceptance.", "questions": "please refer to weaknesses", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "1. The use of symbolic methods for process supervision is well motivated and directly addresses limitations of outcome rewards. By enforcing step level logical validity, the approach reduces reward hacking and aligns training with faithful reasoning.\n2. Incorporating theorem prover feedback in multiple iterations expands the exploration space and yields a more informative training signal. Iterative prover guided refinement improves coverage of candidate solutions, lowers variance, and encourages discovery of alternative valid derivations rather than overfitting to a single trace.\n3. The manuscript is clearly written with well easy to follow and transparent evidence.", "weaknesses": "1. The paper omits several studies that combine LLMs with provers, for example Quan et al., “Verification and Refinement of Natural Language Explanations through LLM and Symbolic Theorem Proving,” EMNLP 2024. The task focus is closely related. Please situate LogicReward within this line of work and add direct comparisons where possible.\n2. It is unclear how much the method’s gains depend on the chosen prover and logic. If a different proof assistant or formal language is used, does LogicReward retain its advantages and stability. Experiments that swap the prover or vary the logic and encoding would strengthen the generality claim.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "jBzhOlMANK", "reviewer": "Reviewer_x5nR", "summary": "This paper introduces LogicReward, a novel reward system designed to train LLMs to produce reasoning that is not only correct in its final outcome but also \"faithful\" and \"logically rigorous\" at each intermediate step. The authors think that in existing training methods, rewarding only correct final answers can lead to models arriving at the right solution through \"flawed reasoning\", and supervising intermediate steps often relies on probabilistic signals, still \"lacks guarantees of logical soundness\".\n\nTo address these, the paper proposes LogicReward, which evaluates the logical validity of each reasoning step using a theorem prover. The method translates ambiguous natural language reasoning steps into the formal symbolic logic required by a theorem prover (specifically, Isabelle). Then, the paper gets the LogicScore by the following steps:\n1. Checks if the reasoning step is \"grounded in the given context\". It measures the cosine similarity between the premises used in a step and the original premises provided in the problem.\n2. Uses the theorem prover to check if the inference made in the step is logically sound. If the step cannot be parsed (i.e., has invalid syntax), the system falls back to using the \"average token probability\" as the score.\n3. The average of the Premise Validity and Logic Validity scores across all steps in the reasoning chain.\n4. A binary score (1 or 0) for whether the final answer matches the ground truth.\n5. The final LogicScore is an equal-weighted average of the Reasoning Validity and the Outcome Validity.\n\nAfter getting the LogicReward, the signal could be used to construct datasets and used to train models via SFT and DPO.", "questions": "Refer to Weaknesses.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "1. The primary strength is the integration of a symbolic theorem prover into the reward loop. This moves beyond the limitations of purely outcome-based or probabilistic process-based rewards, providing a more rigorous \"formal and symbolic assessment of logical validity\".\n2. The method directly targets and improves reasoning faithfulness, a critical need for high-stakes domains like medicine and law. The paper's manual evaluation found that the LogicReward-trained model could produce more faithful reasoning processes.\n3. The model shows strong generalization to out-of-distribution tasks, including BBH, GSM8K, and CommonsenseQA.\n4. LogicReward excels in scenarios without ground-truth labels. By removing the \"Outcome Validity\" component, the reward signal relies only on Premise and Logic Validity. In this setting, it still outperformed other reward systems (LLM-as-judge, PRM, Confidence), demonstrating its value in real-world situations where labels are scarce.", "weaknesses": "1. The authors explicitly acknowledge that the LogicReward labeling process, which involves running a theorem prover, is \"relatively slower than approaches that only compare final outcomes\".\n2. This speed limitation presents a significant challenge for scalability, particularly for \"on-policy reinforcement learning scenarios\"  (like PPO or GRPO) that require fast, in-the-loop reward generation. The paper's use of SFT and DPO  cleverly sidesteps this by being offline methods, but it leaves the system's viability for on-policy RL as an open question.\n3. The auto-formalization process is \"still imperfect\". Even with soft unification and refinement, ambiguities in natural language remain difficult to formalize. The results show that even after refinement, the logic success rate was 50.8%, meaning nearly half of the steps were still not validated as logically sound by the prover.\n4. When a reasoning step fails the syntactic check and cannot be evaluated by the theorem prover, the system \"falls back to the confidence of the inference $I$, defined as the average token probability of the reasoning step\". This pragmatic choice means that for a large portion of reasoning steps (those that fail to parse), LogicReward does not actually provide a symbolic logical guarantee.\n5. The method was primarily trained and evaluated on NLI and logical reasoning datasets. While it showed some generalization, the paper notes that \"gains on GSM8K are smaller\". The authors suggest this is because mathematical reasoning relies \"more on domain-specific reasoning\"  than on the commonsense assumptions that Soft Unification is good at handling. This suggests the current pipeline may be less effective for highly specialized domains without further adaptation.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "syiVEcQtYD", "reviewer": "Reviewer_L2rG", "summary": "The paper proposes LogicReward: a step‑level reward for reasoning that averages (i) Premise Validity—a cosine‑similarity grounding check against the provided premises—and (ii) Logic Validity—a deterministic check with Isabelle/HOL. The combined LogicScore selects SFT targets and DPO pairs. On eight NLI/logic benchmarks, LogicReward yields notable gains and higher human‑audited faithfulness; it also transfers to BBH/GSM8K/CSQA and remains competitive without outcome labels.", "questions": "* Your method generates training data with an automated pipeline. Could errors/noise slip in, and where in the pipeline are they most likely (e.g., premise-grounding, auto-formalization/parsing, soft-unification, prover-guided refinement, fallback scoring)? Did you perform any human auditing, and at what scale?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 4, "strengths": "* Substantial performance improvements across diverse NLI/logic datasets; the 8B backbones show consistent average gains (+11.0 for Llama3.1‑8B; +3.2 for Qwen3‑8B).\n* Faithfulness improves and is human‑verified: on a manual audit of 100 correct cases, the LogicReward‑trained model achieves 68% faithful traces vs. 43%/57% for baselines. I think reasoning faithfulness is critical for transparency/trust in the era of thinking LLMs.", "weaknesses": "* The training data are constructed automatically (LLM rollouts + theorem‑provers), and the paper does not report end‑to‑end human auditing of that data. This raises the risk that intermediate steps/premises or injected “soft‑unification” assumptions contain errors. Though the final positive performance gain from the proposed method's training compensates for some.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)