LogicTrack: Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solvers

Jingyu Hu; Shu Yang; Weiru Liu; Di Wang

cs.AISep 18, 2026

LogicTrack: Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solvers

Authors: Jingyu Hu, Shu Yang, Weiru Liu, Di Wang

Organizations: University of Bristol · King Abdullah University of Science and Technology

Abstract

Chain-of-Thought (CoT) reasoning has been shown to improve the performance of large language models (LLMs), yet existing optimization methods largely rely on outcome-based feedback, leaving the logical validity of intermediate reasoning steps largely unverified. To address the gap whereby LLMs arrive at correct final answers through logically flawed intermediate reasoning chains, we propose LogicTrack, a neuro-symbolic framework that audits reasoning trajectories by auto-formalizing each reasoning step into symbolic representations and verifying it with automated theorem provers. LogicTrack introduces Solver-Based Backtracking Reward (SBR), a step-wise scoring mechanism that quantifies logical soundness and guides backtracking tree search at inference time. We further extend LogicTrack to construct supervised fine-tuning (SFT) data with backtracking traces from its trajectories, enabling fine-tuned models to internalize step-wise auditing as an intrinsic capability. Extensive experiments across 8 reasoning benchmarks and 7 LLMs demonstrate that LogicTrack effectively improves both the verifiability of reasoning chains and final answer pass rate, thereby enhancing overall CoT quality and trustworthiness in high-stakes domains.

Figures & tables

Figure 1: Overview of the LogicTrack workflow. Each NL reasoning step is decomposed, formalized into a solver-executable specification, verified, assigned an SBR score, and either forwarded [FW] to the next step or backtracked [BT] for regeneration. These generated trajectories can be used for backtracking fine-tuning.

Figure 2: An example of LogicTrack-SFT training data construction with backtracking trajectories.

Dataset	Metric	Gemini-2.5		GPT-4o-mini		GPT-5-nano		Llama-3.1-8B		Mistral-7B		Qwen2.5-7B		Qwen2.5-14B
		BASE	Ours	BASE	Ours	BASE	Ours	BASE	Ours	BASE	Ours	BASE	Ours	BASE	Ours
FOLIO	VWA $\Uparrow$	21.17	56.37	46.35	59.91	46.35	51.36	27.76	39.40	32.87	43.82	31.90	48.97	45.14	57.53
	OA $\Uparrow$	79.31	77.59	68.97	74.14	71.70	73.28	48.28	45.69	48.28	54.31	59.48	65.52	75.00	75.00
	UR $\Downarrow$	75.63	27.79	34.74	19.76	38.75	31.90	41.85	17.45	33.75	26.72	47.65	28.41	42.09	28.00
ESNLI	VWA $\Uparrow$	31.09	39.08	46.38	87.21	30.10	44.32	11.89	19.07	16.12	22.74	35.25	50.52	39.50	53.89
	OA $\Uparrow$	66.67	66.67	86.05	100.00	65.12	63.57	22.48	21.71	31.01	31.01	60.47	64.34	68.22	65.89

Table 1: Benchmark-level Performance Comparison of VWA%, OA%, and UR% between BASE and LogicTrack (Ours) across Eight Reasoning Data Benchmarks and Seven Models.

Figure 3: Overall OA and VU for all models averaged across eight benchmarks under BASE and LogicTrack settings. Here $\bullet$ indicates closed source models, and $\blacktriangle$ indicates locally deployed models. Dashed arrows connect each model’s BASE and LogicTrack results.

Model	Method	VWA $\Uparrow$	$\Delta$ VWA $\Uparrow$	OA $\Uparrow$	$\Delta$ OA $\Uparrow$	UR $\Downarrow$
gpt- 4o mini	Fidelity Only	45.80	5.3	70.96	10.7	37.19
	Solver Only	63.96	23.4	73.16	12.9	15.78
	SBR (Both)	65.90	25.4	73.16	12.9	10.81
Llama- 3.1 8B	Fidelity Only	32.49	0.4	63.97	11.0	48.83
	Solver Only	57.55	25.4	62.50	9.6	7.89
	SBR (Both)	57.98	25.9	63.60	10.7	9.89

Table 2: Ablation Study of LogicTrack. (a) SBR reward component ablation. (b) Backtracking search strategy variants. The

\Delta

values report the absolute improvement (%) over the BASE model.

Figure 4: OA $\Uparrow$ and VWA $\Uparrow$ under BASE, LogicTrack, and LogicTrack-SFT averaged over all datasets. LogicTrack-SFT refers to the model fine-tuned on LogicTrack-generated train data.

Metric	LogicReward ( Xu et al. 2025b )	LogicTrack	LogicTrack-SFT
OA $\uparrow$	0.4338	0.5765	0.6808
VWA $\uparrow$	0.2656	0.4782	0.3924

Table 3: Performance comparison among LogicReward and LogicTrack. Full comparisons are in Table 6 of Appendix C.

Figure 5: Effectiveness of backtracking supervision in LogicTrack-SFT on Qwen2.5-7B. The VWA $\uparrow$ and UR $\downarrow$ comparison across inference-time LogicTrack, LogicTrack-SFT-BT, and LogicTrack-SFT-NoBT.

Appendix figures & tables3 assets

Supplementary material from the paper’s appendix.

Appendix

Metric	Gemini-2.5		GPT-4o-mini		GPT-5-nano		Llama-3.1-8B		Mistral-7B		Qwen2.5-7B		Qwen2.5-14B
Metric	Base	LogicTrack	Base	LogicTrack	Base	LogicTrack	Base	LogicTrack	Base	LogicTrack	Base	LogicTrack	Base	LogicTrack
OA $\Uparrow$	0.8096	0.8112	0.7068	0.7849	0.6850	0.7044	0.5506	0.5681	0.4964	0.5275	0.6629	0.7060	0.7402	0.7506
VU $\Uparrow$	0.1936	0.2725	0.2151	0.4661	0.2607	0.3968	0.0924	0.3275	0.1841	0.2980	0.1633	0.3554	0.2382	0.4143
VWA $\Uparrow$	0.3071	0.3693	0.4578	0.6436	0.4527	0.5394	0.3212	0.4717	0.3186	0.4025	0.3507	0.4942	0.4484	0.5573
UR $\Downarrow$	0.6273	0.5477	0.3727	0.1898	0.3832	0.2570	0.4171	0.1871	0.3793	0.2476	0.4737	0.3068	0.4213	0.2687

Appendix

Table 4: Overall performance for all models averaged across eight benchmarks under BASE and LogicTrack. Here OA and VU correspond to the coordinates used in Figure 3

Model	Metric	ESNLI	FOLIO	LogiQA	ProntoQA	ProofWriter	QASC	SARA	SemEval
SFT Llama-3.1-8B	OA	0.6047	0.6121	0.5170	0.9900	0.6548	0.8767	0.6324	0.7842
	VWA	0.3366	0.3412	0.2922	0.8069	0.3654	0.5194	0.4029	0.3004
	UR	0.4012	0.4735	0.4413	0.1856	0.5069	0.4463	0.3836	0.6207
SFT Qwen2.5-7B	OA	0.7984	0.6552	0.6136	0.9700	0.6131	0.8767	0.6360	0.7895
	VWA	0.4180	0.3329	0.3428	0.6183	0.3302	0.4840	0.4053	0.2982
	UR	0.4554	0.4825	0.4313	0.3587	0.5335	0.4589	0.3580	0.6433

Appendix

Table 5: Performance of LogicTrack-SFT across different models and datasets. We report OA

\uparrow

, VWA

\uparrow

, and UR

\downarrow

Dataset	OA $\uparrow$			VWA $\uparrow$			UR $\downarrow$
Dataset	LogicReward	LogicTrack	LogicTrack-SFT	LogicReward	LogicTrack	LogicTrack-SFT	LogicReward	LogicTrack	LogicTrack-SFT
FOLIO	0.3103	0.4569	0.6121	0.1841	0.3940	0.3412	0.4490	0.1745	0.4735
ESNLI	0.0155	0.2171	0.6047	0.0052	0.1907	0.3366	0.2605	0.1118	0.4012
LogiQA	0.3920	0.5000	0.5170	0.2408	0.4472	0.2922	0.3655	0.1247	0.4413
ProntoQA	0.6100	0.8700	0.9900	0.4457	0.7152	0.8069	0.3085	0.2046	0.1856
ProofWriter	0.4121	0.5729	0.6548	0.2130	0.4291	0.3654	0.5150	0.2910	0.5069

Appendix

Table 6: Dataset-level comparison among LogicReward, LogicTrack, and LogicTrack-SFT on Llama-3.1-8B. We report OA

\uparrow

, VWA

\uparrow

, and UR

\downarrow

Explore similar work

The Tell-Tale Trace: Detecting Reasoning Failures in LLMs Using Chain-of-Thought Dynamics
Aug 4, 2026Shashwat Sourav, Aishwarya BalwaniLLM Reliability Reasoning Trace Analysis
Department of Physics, Washington University in St. Louis · Department of Developmental Neurobiology, St. Jude Children’s Research Hospital
Imbuing Large Language Models with Bidirectional Logic for Robust Chain Repair
Jun 3, 2026Zehua Cheng, Wei Dai, Jiahao Sun +1LLM Self-Correction Symbolic Reasoning
Department of Computer Science, University of Oxford, UK · Institute of Logic and Computation, TU Wien, Austria
Making LLMs Say What They Think: Measuring and Improving CoT-Interpretability Alignment
Sep 30, 2026Yihuai Hong, Shauli Ravfogel, Chen Zhao +1CoT Faithfulness Faithfulness of Language Model Explanations
New York University · NYU Shanghai

Aug 4, 2026J/K move · Enter open · S save

The Tell-Tale Trace: Detecting Reasoning Failures in LLMs Using Chain-of-Thought Dynamics

Shashwat Sourav, Aishwarya Balwani

Department of Physics, Washington University in St. Louis · Department of Developmental Neurobiology, St. Jude Children’s Research Hospital

LLM Reliability Reasoning Trace Analysis

Open paper AskPDF arXiv

Chain-of-thought (CoT) reasoning improves large language model (LLM) performance while also providing an observable interface to the model's reasoning process. Existing approaches that leverage verbalized CoTs to monitor reasoning correctness, however, largely evaluate the semantic correctness or consistency of individual intermediate steps, rather than how the reasoning process evolves across the trace. As a result, failures distributed across the reasoning trajectory, rather than those localized to a single incorrect step, remain comparatively underexplored. Furthermore, verbalized CoTs need not faithfully reflect the model's internal reasoning, motivating analyses that do not treat individual statements as literal accounts of internal computation. In this work, we therefore ask whether the dynamics of visible CoT can be leveraged to systematically distinguish successful from failed reasoning without assuming such semantic faithfulness. We study a range of LLMs on verifiable Boolean satisfiability tasks with variable complexity, enabling controlled comparisons near each model's capability frontier. Tagging CoT sentences by reasoning function reveals premature verification collapse on SAT problems: incorrect traces enter clause checking earlier, repeat similar operations, and finalize sooner. On UNSAT problems, models presumptuously move towards incorrect SAT conclusions, checking candidate assignments rather than deriving contradictions across constructed cases. Subsequently, a targeted proof-search prompt intervention raises Llama3-70B accuracy from 13.3% to 85%, correcting 84.6% of these errors. These results show that capability failures can manifest as distributed, task-dependent changes in the structure of visible reasoning, and that CoT dynamics agnostic to whether the verbalized trace reflects the model's internal computations can help diagnose and correct failures.

Abstract

Explore similar work

The Tell-Tale Trace: Detecting Reasoning Failures in LLMs Using Chain-of-Thought Dynamics

Imbuing Large Language Models with Bidirectional Logic for Robust Chain Repair

Making LLMs Say What They Think: Measuring and Improving CoT-Interpretability Alignment