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

نوع مقاله : مقاله علمی- پژوهشی

نویسندگان

1 گروه مهندسی کنترل، دانشگاه تبریز، تبریز، ایران.

2 استادیار گروه مهندسی کنترل، دانشگاه تبریز، تبریز، ایران

چکیده

“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.

کلیدواژه‌ها

عنوان مقاله [English]

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

نویسندگان [English]

  • Arian Esmailinasab 1
  • Amir Aminzadeh Ghavifekr 2
1 Department of Control Engineering, University of Tabriz, Tabriz, Iran
2 Assistant Professor of Control Engineering Department, University of Tabriz, Tabriz
چکیده [English]

“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.

کلیدواژه‌ها [English]

  • Argument Reconstruction
  • Enthymemes
  • First-order Logic
  • Large Language Models
  • Neuro-Symbolic Systems
  • Z3 SMT solver

مراجع

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
ارسال نظر در مورد این مقاله
CAPTCHA Image
مجله پژوهش های فلسفی
دوره 20، شماره 56 - شماره پیاپی 56
مقالات
شماره 56 پاییز 1405
مهر 1405
صفحه 845-856

فایل ها

هم رسانی

ارجاع به این مقاله

آمار