NeuroProlog: Multi-Task Fine-Tuning for Neurosymbolic Mathematical Reasoning via the Cocktail Effect

Pratibha Zunjare; Michael Hsiao

cs.AIMar 3, 2026

NeuroProlog: Multi-Task Fine-Tuning for Neurosymbolic Mathematical Reasoning via the Cocktail Effect

Authors: Pratibha Zunjare, Michael Hsiao

Organizations: Electrical and Computer Engineering, Virginia Tech, Blacksburg, USA

Abstract

Large Language Models (LLMs) achieve strong performance on natural language tasks but remain unreliable in mathematical reasoning, frequently generating fluent yet logically inconsistent solutions. We present NeuroProlog, a neurosymbolic framework that ensures verifiable reasoning by compiling math word problems into executable Prolog programs with formal verification guarantees. We propose a multi-task Cocktail training strategy that jointly optimizes three synergistic objectives in a unified symbolic representation space: (i) mathematical formula-to-rule translation (KB), (ii) natural language-to-program synthesis (SOLVE), and (iii) program-answer alignment. This joint supervision enables positive transfer, where symbolic grounding in formula translation directly improves compositional reasoning capabilities. At inference, we introduce an execution-guided decoding pipeline with fine-grained error taxonomy that enables iterative program repair and quantifies model self-debugging capacity. Evaluation on GSM8K across multiple model scales demonstrates that cocktail training improves accuracy over single-task baselines, with statistically significant gains for most evaluated models. Error analysis reveals scale-associated differences in repair behavior: larger models exhibit more readily correctable errors, whereas smaller models show reduced syntactic errors but persistent semantic failures. These findings suggest that model capacity influences the acquisition of reliable symbolic reasoning and self-correction capabilities.

Figures & tables

Panel of Figure 1 — Fig. 1: Comparison of traditional LLM fine-tuning with NeuroProlog .

Dimension	PAL/PoT	GSM8K-P	LogicLM	LINC	Self-Dbg	Reflexion	ProSLM	Ours
KB grounding (train)	$\times$	$\times$	$\times$	$\times$	$\times$	$\times$	P	✓
Cross-task transfer	$\times$	$\times$	$\times$	$\times$	$\times$	$\times$	$\times$	✓
5-class error taxonomy	$\times$	$\times$	$\times$	$\times$	$\times$	$\times$	$\times$	✓
Execution feedback	$\times$	$\times$	P	$\times$	✓	✓	$\times$	✓
Scale-dependent analysis	$\times$	$\times$	$\times$	$\times$	$\times$	$\times$	$\times$	✓

TABLE I: Comparison of neurosymbolic reasoning systems across five design dimensions. ✓ = fully supported; P = partial;

\times

= absent.

Panel of Figure 3 — Fig. 2: NeuroProlog execution-guided decoding pipeline with error feedback.

Large-Scale Code Model (32B)
Model	Config	Acc. (%)	Exec. (%)	Initial Exec (%)	Corr. (%)	Avg Iter	Sig.
Qwen2.5-Coder-32B	Base	80.29	97.04	96.4	17.0	1.07	—
	Prolog FT	85.14	99.24	98.7	41.2	1.02	$\ddagger$
	Cocktail FT	85.52	99.32	90.7	92.7	1.11	$\ddagger$
	$\Delta_{\text{Prolog}}$	+4.85	+2.20	+2.3	+24.2	$-$ 0.05
	$\Delta_{\text{Cocktail}}$	+5.23	+2.28	$-$ 5.7	+75.7	+0.04

TABLE II: GSM8K evaluation with Prolog-based code generation. Bold = best per model; underline = overall best.

\Delta

rows show absolute change from the base model.

\dagger

p<0.05

;

\ddagger

p<0.01

by McNemar’s test against the same-model base configuration.

Fig. 3: GSM8K accuracy across four models and three configurations. Annotations show Cocktail FT improvement over the base model. Qwen3-8B is the only model where fine-tuning decreases accuracy, revealing a generation–correction trade-off.

Model	Base	Cocktail FT	$\Delta$
Qwen2.5-Coder-32B	40.17	42.68	+2.51
GPT-OSS-20B	49.37	51.46	+2.09
Llama-3B-Instruct	9.10	10.04	+0.94
Qwen3-8B	30.96	21.34	$-9.62$

TABLE III: Cocktail FT accuracy (%) on MATH-500 subset (239 problems).

\Delta

denotes change from Base.

Fig. 4: Initial success vs. correction rate across all 12 configurations, revealing four distinct behavioral regimes.

Fig. 5: Final error distribution after

k{=}3

correction attempts, by Prolog error type.

Fig. 6: Accuracy vs. Efficiency tradeoff across all configurations.

Model	Prolog FT	Cocktail FT	$\Delta$ Acc.	$\Delta$ Exec.
Qwen-32B	85.14	85.52	+0.38	+0.08
GPT-OSS-20B	86.12	88.34	+2.22	+2.00
Qwen3-8B	63.15	64.51	+1.36	+1.14
Llama-3B	21.83	27.07	+5.24	+15.84
Mean	64.06	66.36	+2.30	+4.77

TABLE IV: Effect of Additional Symbolic Supervision

	Initial success(%)	Final accuracy(%)	$\Delta$
Prolog FT	98.7	85.14	$-13.6$
Cocktail FT	90.7	85.52	$-5.2$
$\Delta$ (KB)	$-8.0$	+0.38	—

TABLE V: Effect of execution-guided repair on Qwen-32B performance.

LLM Mathematical Reasoning

Large language model mathematical reasoning studies how AI systems solve, explain, verify, and generalize across mathematical problems and proofs.

See all 270 papers

Aug 26, 2026

Neuro-symbolic PRM: Enhancing Scientific Reasoning via Structured Traces and Symbolic Verification

While tool-augmented Large Language Models have significantly improved multi-step reasoning in quantitative STEM tasks, a critical residual failure mode remains: intermediate reasoning steps that are syntactically well-formed, mathematically executable, and unit-consistent, yet contextually ungrounded. Current approaches either rely on formal verifiers that cannot assess semantic intent, or burden Process Reward Models (PRMs) with the dual task of checking both arithmetic and logic. In this paper, we propose a neuro-symbolic framework that cleanly decouples reasoning into two formal dimensions: Symbolic Validity (

V

) and Semantic Groundedness (

G

). We guarantee

V

by construction using a deterministic symbolic verifier acting as a hard filter. To assess

G

, we train a PRM conditionally on the verifier-accepted manifold. To train this PRM efficiently, we introduce Counterfactual Symbolic Perturbation (CSP), a novel data synthesis strategy that algorithmically generates constraint-preserving hard negatives (steps that perfectly pass the verifier but are logically flawed). At inference, we deploy a verifier-first constrained search that guarantees execution consistency for verifier-covered operations while relying on the PRM solely to rank semantic grounding. By targeting the exact residual error class of strong tool-using LLMs, our method significantly improves reasoning reliability without the sprawling heuristics of prior frameworks.

Yuxin Zi, Cong Xu, Suparna Bhattacharya +2

AI Institute of South Carolina · HPE Labs · Indian AI Research Organisation

Scientific Reasoning in Language Models Neuro-Symbolic Reasoning Process Reward Models Numerical Reasoning in Language Models

Ask PDF

Aug 9, 2026

SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification

Large language models (LLMs) increasingly serve as data-driven reasoners, yet their chains-of-thought (CoT) can be unfaithful even when final answers are correct. Most existing

verification'' signals are not diagnostic: answer matching observes only the outcome, LLM-as-judge provides subjective and non-verifiable critiques, and scalar rewards (e.g., PRMs/RMs) offer little insight into where a multi-step derivation fails.We propose **SymDiag**, a neuro-symbolic framework that **reframes reasoning verification as structured failure diagnosis**. SymDiag translates natural-language CoT into symbolic constraints and performs step-level satisfiability/entailment checks to (i) localize failing steps and (ii) produce verifiable diagnostic evidence, including counterexamples, inconsistency witnesses, and missing-premise indicators. A central challenge is that apparent

logic violations'' can be caused either by genuine reasoning defects or by neural-to-symbolic translation noise. SymDiag therefore incorporates a Self-Auditor that disentangles TranslationError from ReasoningError via dual symbolic encodings consistency checks, enabling robust diagnosis under partial observability. Across diverse mathematical, logical, scientific, and general reasoning benchmarks, SymDiag improves detection of unfaithful reasoning and provides substantially more effective feedback for multi-round reasoning repair than outcome-only verification and LLM-based judging, offering a principled foundation for trustworthy and scalable reasoning diagnosis.

Wenyao Cui, Huaping Zhang, Yongyi Huang +6

Beijing Institute of Technology Beijing, China · Zhongguancun Academy Beijing, China · Xinjiang Future Enterprise Incubator Co., Ltd. Xinjiang, China +1

CoT Faithfulness LLM Answer Verification Symbolic Reasoning Neuro-Symbolic Reasoning

Ask PDF

Oct 1, 2026

The Missing Primitive: Diagnosing and Repairing Mathematical Reasoning in Large Language Models

While Large Language Models (LLMs) have demonstrated striking capabilities on frontier mathematical problems, it remains unclear whether they possess the structural mathematical understanding underlying their solutions. In this paper, we take a first step toward systematically studying mathematical understanding in LLMs, from diagnosing its distinct capabilities to leveraging these findings to improve post-training. First, we introduce the notion of Mathematical Primitive to probe structural mathematical understanding and propose \hlei{}, a novel benchmark that evaluates mathematical reasoning along four distinct dimensions: Discovery, Generation, Digestion, and Execution. Second, our systematic diagnosis shows that solution accuracy masks distinct capability profiles, primitives unlock substantial latent execution capacity, and Discovery is the dominant bottleneck in mathematical reasoning. Our post-training analysis further shows that discovery-limited failures are particularly amenable to repair. Finally, building on these findings, we introduce \abs{}, a primitive-privileged self-distillation framework that selectively transfers primitive-guided reasoning into the student model. Extensive experiments demonstrate that \abs{} consistently improves mathematical reasoning over baselines across model scales and challenging benchmarks.

Shuo Xing, Zilin Dai, Chengyuan Qian +7

Texas A&M University · Harvard University · Vanderbilt University +3

Mathematical Reasoning Benchmarks Self-Distillation LLM Post-Training LLM Mathematical Reasoning

Ask PDF

Abstract

LLM Mathematical Reasoning

Explore similar work

Neuro-symbolic PRM: Enhancing Scientific Reasoning via Structured Traces and Symbolic Verification

SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification

The Missing Primitive: Diagnosing and Repairing Mathematical Reasoning in Large Language Models