Neuro-Symbolic Reconstruction of Philosophical and Formal Arguments: Automated Propositional Mapping and Verdict Verification via LLMs and SMT Solvers

Document Type : Research Paper

Authors

1 Department of Control Engineering, University of Tabriz, Tabriz, Iran

2 Assistant Professor of Control Engineering Department, University of Tabriz, Tabriz

Abstract

“To test whether an end-to-end neuro-symbolic pipeline (deterministic segmentation, LLM formalisation into SMT-LIB2, automated symbolic repair, and three-way Z3 SMT verification with countermodel generation) can reconstruct classical philosophical arguments, and to quantify where scaling changes the character of formalisation failures.” Five-stage pipeline evaluated on 31 curated philosophical and explicit-logic arguments plus the full 204-item FOLIO validation split under a three-way protocol, replicated across three independently pinned backends (Qwen3-4B-Instruct; Gemini 3.8 Flash; Nemotron-3-Ultra-550B). An independent audit script re-derives every reported number from the archived raw records. Explicit logic vs. philosophical prose: 68.8%/27.3% (Qwen) and 93.8%/63.6% (Gemini); replicated effect sizes of −41.5 and −30.2 percentage points (Fisher p = 0.054/0.125, not significant for the larger model). Enthymemes: 0.0% vs 50.0%; a warrant-eliciting prompt repairs the barrier only for the larger model (7/11 to 10/11) at a cost on explicit items (8/8 to 6/8). FOLIO: a refutation asymmetry replicates in all three families and decided-item refutation never exceeds 58.1% (36/62); the direct no-solver baseline is 66.7% for the small model. LLMs transcribe fluently but reconstruct poorly; the deficit on classical prose is necessary rather than technical. The pipeline's value is inspectable judgment — solver-checked verdicts, per-stage diagnosis, and countermodels as automated thought experiments.

Keywords

References

de Moura, L., & Bjørner, N. (2008). Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 337–340). Springer. https://doi.org/10.1007/978-3-540-78800-3_24
Dziri, N., Lu, X., Sclar, M., Li, X. L., Jiang, L., Lin, B. Y., West, P., Bhagavatula, C., Le Bras, R., Hwang, J. D., Sanyal, S., Welleck, S., Ren, X., Ettinger, A., Harchaoui, Z., & Choi, Y. (2023). Faith and fate: Limits of transformers on compositionality. Advances in Neural Information Processing Systems, 36. https://arxiv.org/abs/2305.18654
Frege, G. (1967). Begriffsschrift, a formula language, modeled upon that of arithmetic, for pure thought (S. Bauer-Mengelberg, Trans.). In J. van Heijenoort (Ed.), From Frege to Gödel: A source book in mathematical logic, 1879–1931 (pp. 1–82). Harvard University Press. (Original work published 1879)
Han, S., Schoelkopf, H., Zhao, Y., Qi, Z., Riddell, M., Zhou, W., Coady, J., Peng, D., Qiao, Y., Benson, L., Sun, L., Wardle-Solano, A., Szabó, H., Zubova, E., Burtell, M., Fan, J., Liu, Y., Wong, B., Sailor, M., … Radev, D. (2024). FOLIO: Natural language reasoning with first-order logic. In Proceedings of EMNLP 2024 (pp. 22017–22031). https://doi.org/10.18653/v1/2024.emnlp-main.1229
Nabavi, L., & Mirsanei, S. A. (2026). Paraconsistency, relevance and vagueness: A proof theoretic approach to fuzzy relevant logic FR. Journal of Philosophical Investigations, 20(55), 325–352. https://doi.org/10.22034/jpiut.2026.70950.4391
Olausson, T. X., Gu, A., Lipkin, B., Zhang, C., 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. In Proceedings of EMNLP 2023 (pp. 5153–5176). https://doi.org/10.18653/v1/2023.emnlp-main.313
Pan, L., Albalak, A., Wang, X., & Wang, W. Y. (2023). Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning. In Findings of EMNLP 2023 (pp. 3806–3824). https://doi.org/10.18653/v1/2023.findings-emnlp.248
Saparov, A., & He, H. (2023). Language models are greedy reasoners: A systematic formal analysis of chain-of-thought. In Proceedings of ICLR 2023. https://arxiv.org/abs/2210.01240
Tafjord, O., Dalvi, B., & Clark, P. (2021). ProofWriter: Generating implications, proofs, and abductive statements over natural language. In Findings of the Association for Computational Linguistics: ACL 2021 (pp. 3621–3634).
Toulmin, S. E. (2003). The uses of argument (Updated ed.). Cambridge University Press. (Original work published 1958)
Walton, D., Reed, C., & Macagno, F. (2008). Argumentation schemes. Cambridge University Press.
Ye, X., Chen, Q., Dillig, I., & Durrett, G. (2023). SatLM: Satisfiability-aided language models using declarative prompting. Advances in Neural Information Processing Systems, 36. https://arxiv.org/abs/2308.10457
Send comment about this article
CAPTCHA Image
Journal of Philosophical Investigations
Volume 20, Issue 56 - Serial Number 56
Articles
Issue 56, Autumn 2026
October 2026
Pages 845-856

Files

Share

How to cite

Statistics